newsSeparation Logic in Coq - News: extraction of a certified verifier

 
 
Latest News
Upadte of Bigtoe posted by alalme, Wed 13 Dec 2006 01:48:39 AM UTC
Update to Coq v8.1 posted by alalme, Wed 13 Dec 2006 01:45:43 AM UTC
extraction of a certified verifier posted by alalme, Thu 21 Sep 2006 01:11:03 AM UTC
Completeness proof for Separation Logic posted by alalme, Thu 10 Aug 2006 08:58:53 AM UTC

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.13-02a9.
Corresponding source code