An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
A framework for formally verifying distributed systems implementations in Coq
Synthesis for floating-point expressions
The collection synthesizer
Coq utility and tactic library.
compiler for fortran stencils using verified lifting,
Optimizing Synthesis with Metasketches, POPL 2016
A Valgrind tool for Herbie
A CSS synthesizer and reasoning engine
Use SpaceSearch to verify Conjunctive Query Rewrite Rules
Extracting Greg Morrisett x86 Semantics to SMT
A compiler for automatically re-targeting sequential Java code to Apache Spark.
A dummy implementation of the 2.5 Java Servlet designed for sound static analyses
Example application using the ACGLib for both good and evil
Library for AUDACIOUS
PL for 3D Printing
Ferrite, a toolkit for developing file system crash-consistency models
Parallel, incremental evaluation of attribute grammars through synthesis
Formally Verified Serialization Library
Phosphor forked and modified to work with Staccato
Stale Configuration and Consistency Analysis Tool
Batfish is a network configuration analysis tool developed jointly by researchers at University of California, Los Angeles; University of Southern California; and Microsoft Research. Though its individual modules have various applications, its primary purpose is to detect bugs in network configurations.
Peek: a verified peephole optimizer for CompCert
A proof assistant.
A compiler from Rust to C, and a checker for unsafe code
A genetic optimizer for the new PLSE logo
Certified Relational to Imperative
The STOKE stochastic super-optimizer