newsSeparation Logic in Coq - News


extraction of a certified verifier

Item posted by nicolas marti <alalme> on Thu 21 Sep 2006 01:11:03 AM UTC.

We implemented a decision procedure by reflection for Hoare triples using a fragment of separation logic (frag_hoare in frag.v).

Using the abstraction facility of Coq, we extracted the decision procedure in Ocaml, built a parser for Hoare triples with Ocaml-yacc, finally giving a certified verifier for Hoare triples. Its name is bigtoe (any similarity with an existing tool is not a coincidence).

Back to the top

Powered by Savane 3.12