141 skills found · Page 1 of 5
pysmt / PysmtpySMT: A library for SMT formulae manipulation and solving
stp / StpSimple Theorem Prover, an efficient SMT solver for bitvectors
enzet / Symbolic ExecutionHistory of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
SRI-CSL / Yices2SRI Yices SMT Solver
Boolector / BoolectorA Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
bitwuzla / BitwuzlaBitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.
ufmg-smite / Lean SmtTactics for discharging Lean goals into SMT solvers.
LeventErkok / SbvSMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
sosy-lab / Java SmtJavaSMT - Unified Java API for SMT solvers.
testsmt / YinyangA fuzzing framework for SMT solvers
philzook58 / Z3 TutorialJupyter notebooks for tutorial on the Z3 SMT solver
smtcoq / SmtcoqCommunication between Coq and SAT/SMT solvers
muellerberndt / Scrooge McetherfaceScrooge McEtherface is an Ethereum auto-looter that was presented at DEFCON 2019. It uses symbolic execution & SMT solving to generically generate exploit sequences that extract ETH from vulnerable smart contracts.
cpitclaudel / Z3.wasmWASM builds of the Z3 SMT solver
mitchellh / Go Z3Go (golang) bindings to the Z3 SMT Solver
stanford-centaur / Smt SwitchA generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
epfl-lara / ScalaZ3DSL in Scala for Constraint Solving with Z3 SMT Solver
levjj / EsverifyECMAScript verification with SMT solvers
sambayless / MonosatMonoSAT - An SMT solver for Monotonic Theories
wenkokke / SchmittyAgda bindings to SMT-LIB2 compatible solvers.
