No description or website provided.
Haskell
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
tests
.gitignore
G2.cabal
README.md
Setup.hs

README.md

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.0.2 (other GHC 8 versions might also work)
  2. Install Z3
  3. Pull the Custom Haskell Standard Library (optional)
  4. Add a file to the G2 folder, called g2.cfg that contains: base = /path/to/custom/library

Example g2.cfg file:

base = ../base-4.9.1.0/Control/Exception/Base.hs
     , ../base-4.9.1.0/Prelude.hs
     , ../base-4.9.1.0/Data/Map.hs

n = 1000
time = 300

Command line:

Reachability:

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

LiquidHaskell:

cabal run G2 ./tests/Liquid/ -- --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)
  • Ranjit Jhala (UCSD)
  • Ruzica Piskac (Yale)