dbueno Goto Github PK

ascent_simple

bitfunc

Library for building bit-vector and array constraints directly on top of a SAT solver

boolector

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

cclyzer-souffle

CClyzer port to souffle lang

certora-tutorials

Practical tutorials of Certora Prover

creduce

C-Reduce, a C program reducer

dbueno.github.io

ddsmt

A delta debugger for SMT benchmarks in SMT-LIB v2.

dotfiles

configuration files

dotvim

Vim configuration

espresso-ab-1.0

Reworked version of c espresso code that compiles with modern compilers

euforia

Software model checking with uninterpreted functions abstraction

fiblib

Fibonacci heap in ocaml

funsat

An efficient, embeddable DPLL SAT solver in Haskell

horn2vmt

Translation from (linear) Horn clauses into VMT, a logic-based transition system format

ic3ref

IC3 reference implementation: a short, simple, fairly competitive implementation of IC3. Read it, tune it, extend it, play with it.

immer

Postmodern immutable and persistent data structures for C++ — value semantics at scale

merjar

mini-mc

minimal symbolic model checker & fuzzer

minisat

A minimalistic and high-performance SAT solver (that compiles on OS X)

nix-bundle

Bundle Nix derivations to run anywhere!

nixpkgs

Nix Packages collection

ocaml-csv

CSV library for OCaml

outputcheck

A tool for checking tool output inspired by LLVM's FileCheck

parse-dimacs

puzzler

A puzzle assistant

qfgrep

a vim plugin to filter entries in Quickfix

rose

Developed at Lawrence Livermore National Laboratory (LLNL), ROSE is an open source compiler infrastructure to build source-to-source program transformation and analysis tools for large-scale C (C89 and C98), C++ (C++98 and C++11), UPC, Fortran (77/95/2003), OpenMP, Java, Python and PHP applications.

rusage

satyr

Automatically exported from code.google.com/p/satyr