@hackage g20.1.0.1

Haskell symbolic execution engine.

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 8.2.2 (other GHC 8 versions might also work)
  2. Install Z3
  3. Either:

a) Pull the Custom Haskell Standard Library into ~/.g2 by running bash base_setup.sh

b) Manually pull the base library. Add a file to the G2 folder, called g2.cfg that contains: base = /path/to/custom/library


Command line:

Reachability:

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

LiquidHaskell:

cabal run G2 -- --liquid ./tests/Liquid/Peano.hs --liquid-func 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

Authors

  • Bill Hallahan (Yale)
  • Anton Xue (Yale)
  • Maxwell Troy Bland (UCSD)
  • Ranjit Jhala (UCSD)
  • Ruzica Piskac (Yale)