@hackage g20.2.0.0

Haskell symbolic execution engine.

  • Installation

  • Dependencies (38)

  • Dependents (1)

    @hackage/g2q
  • Package Flags

      support-lh
       (on by default)

      Build modules for reasoning about LiquidHaskell

G2 Haskell Symbolic Execution Engine


About

G2 performs lazy symbolic execution of Haskell programs to detect state reachability. It is capable of generating assertion failure counterexamples and solving for higher-order functions.


Dependencies


Setup:

  1. Install GHC.
  2. Install Z3. Ensure Z3 is in your system's path.
  3. Pull the Custom Haskell Standard Library into ~/.g2 by running bash base_setup.sh.

Command line:

Reachability:

cabal run G2 ./tests/Samples/Peano.hs add

LiquidHaskell:

cabal run G2LH ./tests/Liquid/Peano.hs add

Arguments:
  • --n number of reduction steps to run
  • --max-outputs number of inputs/results to display
  • --smt Pass "z3" or "cvc4" to select a solver [Default: Z3]
  • --time Set a timeout in seconds