Email Gateway (Aug 18 2022 at 18:48): Email Gateway (Aug 18 2022 at 18:48):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Email Gateway (Aug 18 2022 at 18:54):From: Gerwin Klein <gerwin.klein@nicta.com.au>
We're looking at updating all our proofs in the next 2 months or so (optimistically). That includes the parser.
Effort: the C parser is usually one of the more painful parts, because it uses ML-level Isabelle APIs which tend to change a lot more than the user level. We might be pestering people with questions in a few weeks on new ways of doing things.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 18:58):From: Lars Noschinski <noschinl@in.tum.de>
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?
-- Lars
Last updated: Apr 18 2024 at 20:16 UTC