g2: Haskell symbolic execution engine.

[ bsd3, formal-methods, library, program, symbolic-computation ] [ Propose Tags ]

A Haskell symbolic execution engine. For details, please see: https://github.com/BillHallahan/G2


[Skip to Readme]
Versions [faq] 0.1.0.0, 0.1.0.1
Dependencies array (>=0.5.1.1 && <=0.5.3.0), base (>=4.8 && <5), bytestring (>=0.10.8.0 && <=0.10.8.2), Cabal (>=2.0.1.0 && <=2.0.1.1), concurrent-extra (>=0.7), containers (==0.5.*), directory (>=1.3.0.2 && <=1.3.3.2), extra (>=1.6.14 && <=1.6.17), filepath (==1.4.1.2), g2, ghc (==8.2.2), ghc-paths (==0.1.*), hashable (>=1.2.6.0 && <=1.3.0.0), hpc (>=0.6.0.0 && <0.6.1), HTTP (>=4000.3.0 && <4001.0), liquid-fixpoint (>=0.7.0.7), liquidhaskell (==0.8.2.2), MissingH (>=1.4.0.0 && <1.5), mtl (==2.2.*), parsec (==3.1.*), process (>=1 && <1.7), reducers (==3.12.*), regex-base (==0.93.*), regex-compat (==0.95.*), split (==0.2.3.*), template-haskell (==2.12.0.0), temporary-rc (==1.2.*), text (==1.2.3.1), time (>=1.6 && <=1.9.3), unordered-containers (==0.2.*) [details]
License BSD-3-Clause
Author William Hallahan, Anton Xue
Maintainer william.hallahan@yale.edu
Category Formal Methods, Symbolic Computation
Source repo head: git clone https://github.com/BillHallahan/G2.git
Uploaded by WilliamHallahan at Sun Jun 30 02:11:19 UTC 2019
Distributions NixOS:0.1.0.1
Executables QuasiQuote, G2
Downloads 98 total (23 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2019-06-30 [all 2 reports]

Modules

  • G2
    • G2.Config
    • G2.Execution
      • G2.Execution.Interface
      • G2.Execution.Memory
      • G2.Execution.NormalForms
      • G2.Execution.PrimitiveEval
      • G2.Execution.Reducer
      • G2.Execution.RuleTypes
      • G2.Execution.Rules
    • Initialization
      • G2.Initialization.DeepSeqWalks
      • G2.Initialization.ElimTicks
      • G2.Initialization.ElimTypeSynonyms
      • G2.Initialization.InitVarLocs
      • G2.Initialization.Interface
      • G2.Initialization.KnownValues
      • G2.Initialization.MkCurrExpr
      • G2.Initialization.StructuralEq
      • G2.Initialization.Types
    • G2.Interface
    • G2.Language
      • G2.Language.AST
      • G2.Language.AlgDataTy
      • G2.Language.ArbValueGen
      • G2.Language.Casts
      • G2.Language.CreateFuncs
      • G2.Language.Expr
      • G2.Language.ExprEnv
      • G2.Language.Ids
      • G2.Language.KnownValues
      • G2.Language.Located
      • G2.Language.Monad
        • G2.Language.Monad.AST
        • G2.Language.Monad.CreateFuncs
        • G2.Language.Monad.Expr
        • G2.Language.Monad.ExprEnv
        • G2.Language.Monad.Naming
        • G2.Language.Monad.Primitives
        • G2.Language.Monad.Support
        • G2.Language.Monad.TypeClasses
        • G2.Language.Monad.TypeEnv
        • G2.Language.Monad.Typing
      • G2.Language.Naming
      • G2.Language.PathConds
      • G2.Language.Primitives
      • G2.Language.Stack
      • G2.Language.Support
      • G2.Language.Syntax
      • G2.Language.TypeClasses
        • G2.Language.TypeClasses.Extra
        • G2.Language.TypeClasses.TypeClasses
      • G2.Language.TypeEnv
      • G2.Language.Typing
    • Lib
      • G2.Lib.Printers
    • Liquid
      • G2.Liquid.Interface
    • Postprocessing
      • G2.Postprocessing.Interface
    • Preprocessing
      • G2.Preprocessing.AdjustTypes
      • G2.Preprocessing.Interface
      • G2.Preprocessing.NameCleaner
    • QuasiQuotes
      • G2.QuasiQuotes.FloodConsts
      • G2.QuasiQuotes.G2Rep
      • Internals
        • G2.QuasiQuotes.Internals.G2Rep
      • G2.QuasiQuotes.Parser
      • G2.QuasiQuotes.QuasiQuotes
      • G2.QuasiQuotes.Support
    • G2.Solver
      • G2.Solver.Interface
      • G2.Solver.Solver
    • G2.Translation
      • Cabal
        • G2.Translation.Cabal.Cabal

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for g2-0.1.0.1

[back to package description]

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)