26 citations · 70 across the 17 of their papers we have counts for
Showing 2013Show all
2 papers · 1 filter
cs.PL2013★ 1 cited
MirrorShard: Proof by Computational Reflection with Verified Hints
Gregory Malecha, Adam Chlipala, Thomas Braibant +2
We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and…
cs.PL2013★ 25 cited
Formal Verification of Hardware Synthesis
Thomas Braibant, Adam Chlipala
We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version o…