328 citations · 732 across the 43 of their papers we have counts for
Showing 2013 · cs.PLShow all
2 papers · 2 filters
cs.PL2013
Implementing hash-consed structures in Coq
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases includ…
cs.PL2013★ 3 cited
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
Alexis Fouilhé, David Monniaux, Michaël Périn
Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole st…