Hackage :: [Package]

g2: Haskell symbolic execution engine.

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

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

[Skip to Readme]

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

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1.0.0, 0.1.0.1, 0.2.0.0
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 && <0.6), 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 && <0.2), 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 && <2.3), parsec (>=3.1 && <3.2), process (>=1 && <1.7), reducers (>=3.12 && <3.13), regex-base (>=0.93 && <0.94), regex-compat (>=0.95 && <0.96), split (>=0.2.3 && <0.2.4), template-haskell (==2.12.0.0), temporary-rc (>=1.2 && <1.3), text (==1.2.3.1), time (>=1.6 && <=1.9.3), unordered-containers (>=0.2 && <0.3) [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 2019-06-29T00:12:25Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables QuasiQuote, G2
Downloads 986 total (4 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2019-06-29 [all 2 reports]

Readme for g2-0.1.0.0

[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)