12 open source projects by uwplse

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

A CSS specification and reasoning engine

Certified Relational to Imperative

A framework for formally verifying distributed systems implementations in Coq

Optimize floating-point expressions for accuracy

Fun plugin to play with the Gallina AST.

A compiler for automatically re-targeting sequential Java code to Apache Spark.

A Valgrind tool for Herbie

Optimizing Synthesis with Metasketches, POPL 2016

An advanced automated reasoning tool for memory consistency model specifications.

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Rewrite Rule Inference Using Equality Saturation