An automated deductive program verifier based on concurrent separation logic.
Probabilistic separation logics for verifying higher-order probabilistic programs.
The MaPLe compiler: efficient and scalable parallel functional programming.
An automatic verifier for lock-free data structures.
A library of verified concurrent search structure algorithms.
An automated deductive program verifier.
An automated debugging tool for C programs.
A C assertion checker.
An automatic theorem prover for Satisfiability Modulo first-order Theories.
The fourth version in the Cooperating Validity Checker family of tools and the successor to CVC3.
A PVS implementation of a linear temporal logic verification system.
An interactive environment for symbolic model-checking and general BDD computation.