39 Open source projects that are alternatives of or similar to Yices2

Verification framework and tool for higher-order Scala programs

Automatic verification of LLVM optimizations

Symbolic execution tool

APALACHE: symbolic model checker for TLA+

A Proof-oriented Programming Language

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.

Triton is a Dynamic Binary Analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a dynamic taint engine, AST representations of the x86, x86-64, ARM32 and AArch64 Instructions Set Architecture (ISA), SMT simplification passes, an SMT solver interface and, the last but not least, Python bindings.

Precious Plastic Downloadpack

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

Better parametric search for components available for JLC PCB assembly

Update to Eustathios with a little bit of HercuLien Design Changes

mbed HDK - This repository is not being maintained. For the latest updates, please use: https://github.com/ARMmbed/mbed-HDK-Eagle-Projects

Deep Blockchains - reference implementation of Plasma, Stark, SMT and more

Collection of Eagle projects for targets, interfaces, shields and more

JavaSMT - Unified Java API for SMT solvers.

A blackbox mutational fuzzer for detecting critical bugs in SMT solvers

Automatic program repair and patch generation system for Java based on dynamic analysis and code synthesis with SMT, developed at University of Lille and Inria, France.

SMT Solver for Nonlinear Theories of Reals

Liquid Types For Haskell

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

CAD files for various boards, components and parts

pySMT: A library for SMT formulae manipulation and solving

Simple Theorem Prover, an efficient SMT solver for bitvectors

"SAT/SMT by example" free ebook

SMACK Software Verifier and Verification Toolchain

A Go library that implements a Sparse Merkle tree for a key-value map.

Kryptonite for Kafka is a client-side 🔒 field level 🔓 crypto library for Apache Kafka® currently focused on Kafka Connect scenarios. It's an ! UNOFFICIAL ! community project

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Jupyter notebooks for tutorial on the Z3 SMT solver

A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)

Synthesis of Heap-Manipulating Programs from Separation Logic

Haskell bindings to Microsoft's Z3 API (unofficial).

CLP(SMT) on top of miniKanren

Transpiler of Python to many other languages

This plugin allows you to configure email notifications for build results

Targoman SMT framework source code

This a type-checker plugin to rule all type checker plugins involving type-equality reasoning using smt solvers.

A simple (unfinished) SMT solver for QF_ABV.

prototyping logic programming in Scala