Stars
Chrobak normal form-based Exponential-Linear Integer Arithmetic Solver
Explyt Spring is a free, source-available plugin for IntelliJ IDEA Community Edition, designed to simplify and improve development with the Spring Framework.
Regular Invariant Generator and SMTLIB2 code transformer
fast and effective way to access and analyze java bytecode
A (concrete or symbolic) implementation of IEEE-754 / SMT-LIB floating-point
Bitwuzla 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 …
Pure Kotlin high performance implementation of Binary Decision Diagrams
grigoryfedyukovich / aeval
Forked from seahorn/seahornAE-solver and Skolemizer
History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
A survey by the SEASON lab on symbolic execution tools and techniques. The survey has appeared in ACM CSUR in 2018.
Statically typed embedding of miniKanren relational programming language into OCaml
Adds the soothing voice of Dmitri Komarov and other great chess masters to lichess.org (Google Chrome extension / Firefox Add-on)
A puzzle game inspired by functional programming
Set of roslyn-based analyzers for catching common C# errors (inspired by Google's error-prone)
Developer guide for the ReSharper Platform
Platform for parser generators and other grammarware research and development. GLL, RNGLR, graph parsing algorithms, and many others are included.
Modular and configurable OS for embedded applications
The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.