UW PLSE

A framework for formally verifying distributed systems implementations in Coq

uwplse

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

uwplse

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

uwplse

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

uwplse

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

uwplse

A CSS specification and reasoning engine

uwplse

Formally verified Coq serialization library with support for extraction to OCaml

uwplse

Fun plugin to play with the Gallina AST.

uwplse

A compiler from Rust to C, and a checker for unsafe code

uwplse

a compiler for re-writing image processing functions in C++ to Halide

uwplse