Re: [isabelle] L4.verified C-to-Isabelle parser release
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] L4.verified C-to-Isabelle parser release
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Wed, 04 Jan 2012 12:23:27 +0100
- In-reply-to: <5EF8996D-3632-4726-AC49-0AAD1692E6B3@nicta.com.au>
- References: <5EF8996D-3632-4726-AC49-0AAD1692E6B3@nicta.com.au>
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:188.8.131.52) Gecko/20111114 Icedove/3.1.16
On 14.12.2011 07:13, Gerwin Klein wrote:
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:
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.
Do you have any estimate when this is going to happen or how much of an
effort it will be to port this to a current Isabelle version?
This archive was generated by a fusion of
Pipermail (Mailman edition) and