GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → BillHallahan → G2

BillHallahan / G2

Licence: other
No description or website provided.

Programming Languages

haskell
3896 projects
python
139335 projects - #7 most used programming language

Labels

symbolic-execution

Projects that are alternatives of or similar to G2

angr-antievasion
Final project for the M.Sc. in Engineering in Computer Science at Università degli Studi di Roma "La Sapienza" (A.Y. 2016/2017).
Stars: ✭ 35 (+45.83%)
Mutual labels:  symbolic-execution
seninja
symbolic execution plugin for binary ninja
Stars: ✭ 123 (+412.5%)
Mutual labels:  symbolic-execution
Rel
Binsec/Rel is an extension of Binsec that implements relational symbolic execution for constant-time verification and secret-erasure at binary-level.
Stars: ✭ 27 (+12.5%)
Mutual labels:  symbolic-execution
crete-dev
CRETE under development
Stars: ✭ 56 (+133.33%)
Mutual labels:  symbolic-execution
CFI-LB
Adaptive Callsite-sensitive Control Flow Integrity - EuroS&P'19
Stars: ✭ 13 (-45.83%)
Mutual labels:  symbolic-execution
TRACER
TRACER Symbolic Execution Tool
Stars: ✭ 23 (-4.17%)
Mutual labels:  symbolic-execution
Angryghidra
Use angr in Ghidra
Stars: ✭ 241 (+904.17%)
Mutual labels:  symbolic-execution
malware-s2e
Code for my blog post on using S2E for malware analysis
Stars: ✭ 21 (-12.5%)
Mutual labels:  symbolic-execution
surveyor
A symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
Stars: ✭ 14 (-41.67%)
Mutual labels:  symbolic-execution
Kirenenko
Super Fast Concolic Execution Engine based on Source Code Taint Tracing
Stars: ✭ 84 (+250%)
Mutual labels:  symbolic-execution
sai
Staged Abstract Interpreters
Stars: ✭ 58 (+141.67%)
Mutual labels:  symbolic-execution
vigor
Main repository of the Vigor NF verification project.
Stars: ✭ 40 (+66.67%)
Mutual labels:  symbolic-execution
SixtyPical
A 6502-oriented low-level programming language supporting advanced static analysis
Stars: ✭ 25 (+4.17%)
Mutual labels:  symbolic-execution
stevia
A simple (unfinished) SMT solver for QF_ABV.
Stars: ✭ 30 (+25%)
Mutual labels:  symbolic-execution
kleespectre
KLEESpectre is a symbolic execution engine with speculation semantic and cache modelling
Stars: ✭ 31 (+29.17%)
Mutual labels:  symbolic-execution
UTBotCpp
Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage
Stars: ✭ 59 (+145.83%)
Mutual labels:  symbolic-execution
symbooglix
Symbolic Execution Engine for Boogie
Stars: ✭ 24 (+0%)
Mutual labels:  symbolic-execution
smoosh
The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.
Stars: ✭ 86 (+258.33%)
Mutual labels:  symbolic-execution
crusher
No description or website provided.
Stars: ✭ 21 (-12.5%)
Mutual labels:  symbolic-execution
binary-decompilation
Extracting high level semantic information from binary code
Stars: ✭ 55 (+129.17%)
Mutual labels:  symbolic-execution
View All Similar Projects ➔

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)
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].