rainoftime Goto Github PK

az3

A solver for All-solution Satisfiabiiity Modulo Theories

bayes-to-cnf

Encode Bayesian Networks into Conjunctive Normal Form

bigdatalog

bvcount

canary

cclyzer

A tool for analyzing LLVM bitcode using Datalog.

cpbenchmark

This repo contains the bc and source files of C/C++ projects used for value-flow analysis. The LLVM IR is in the version of 3.6.2.

csrankings

A web app for ranking computer science departments according to their research output in selective venues, and for finding active faculty across a wide range of areas.

cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

depthk

K-Induction adopting program invariants

dg

[LLVM Static Slicer] Dependence graph for programs. A set of generic program analyses and a static slicer for LLVM bitcode.

dr_checker

DR.CHECKER : A Soundy Vulnerability Detection Tool for Linux Kernel Drivers

dryadsynth

A SyGuS Solver

eldarica

The Eldarica model checker

fastsmt

Learning to Solve SMT Formulas Fast

fpsolve

FPsolve: solver for polynomial equations over omega-continuous semirings

gpusat

graspan-cpp

This is a C++ implementation of Graspan.

hello-abduction

Test of abduction using the MISTRAL SMT solver.

klee

KLEE Symbolic Execution Engine

llvm-cbe

resurrected LLVM "C Backend", with improvements

mba-solver

neongobyport

Port the neonGoby project (https://github.com/columbia/neongoby) to work with the latest version of LLVM

neurosat

NeuroSAT: Learning a SAT Solver from Single-Bit Supervision

opensmt

The opensmt solver

pda

The PDA loop summarization algorithm.

pfad

Pearls of Functional Algorithm Design

plfm-bib

Reference about PL and FM

pysat

A toolkit for SAT-based prototyping in Python

q3b