[isabelle] L4.verified C-to-Isabelle parser release



We're pleased to announce the release of the C-to-Isabelle/Simpl parser by Michael Norrish that was used in the L4.verified project.

It is available for download under BSD license from:
http://www.ertos.nicta.com.au/software/c-parser/

The parser reads .c files after preprocessing and translates them into the language Simpl by Norbert Schirmer embedded in Isabelle/HOL [http://afp.sf.net/entries/Simpl.shtml]. Programs in Simpl can then be verified using the VCG and other mechanisms of that package.

This release is still very much a research tool for experts and is based on Isabelle2009-1. We are aiming at porting the parser to the current Isabelle version in the future.

Cheers,
Gerwin




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.