Block or report user

Pinned repositories

  1. sbv

    SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

    Haskell 162 32

  2. hArduino

    Control your Arduino board from Haskell, using the Firmata protocol

    Haskell 51 3

  3. sbvPlugin

    Formally prove properties of Haskell programs using SBV/SMT.

    Haskell 13 4

  4. conjugateGradient

    Sparse matrix linear equation solver, using the Conjugate Gradient algorithm

    Haskell 7 2

  5. crackNum

    Convert to/from IEEE-754 HP/SP/DP formats

    Haskell 4 2

  6. FloatingHex

    Hexadecimal Floats for Haskell

    Haskell 1

183 contributions in the last year

Mar Apr May Jun Jul Aug Sep Oct Nov Dec Jan Feb Mon Wed Fri

Contribution activity First pull request First issue First repository Joined GitHub

February 2017

Created an issue in Z3Prover/z3 that received 4 comments

Bug with recursive function models?

I'm trying recursive functions in z3, and I'm curious if there's a bug with model construction. Consider: (define-fun-rec f ((x Int)) Int (ite (> x…

Seeing something unexpected? Take a look at the GitHub profile guide.