Email Gateway (Aug 18 2022 at 20:17): Email Gateway (Aug 18 2022 at 20:17):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
What is the best approach for verifying the correctness of C programs in
Isabelle? I see that some people have done some work on this already, but
is there a current best approach? This is for a virtual machine/assembly
language that is implemented in C and will be used as the target language
for a compiler that will need to be verified in Isabelle as well. I
would like to verify the implementation of the virtual machine.
Email Gateway (Aug 18 2022 at 20:20):From: "C. Diekmann" <diekmann@in.tum.de>
Maybe this mail is helpful:
Email Gateway (Aug 18 2022 at 20:20):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Maybe a bit more background on that:
Our C-Parser at http://www.ertos.nicta.com.au/software/c-parser/ will translate a large subset of C into the Isabelle/Simpl language, which comes with various semantics formalisations, verification condition generator, etc.
The version on the website above runs on Isabelle2009-1, we should be able to release the Isabelle2011-1 version shortly, and we're working on the Isabelle2012 update.
The Simpl language is described in Norbert Schirmer's PhD thesis. The C memory model in Harvey Tuch's thesis and a few papers from our web site.
Although the language subset and tool chain are quite powerful and have been applied to large verifications, it is not a very polished tool set at moment, definitely more on the research software side. We'd be happy to help with questions, though.
Cheers,
Gerwin
Last updated: Apr 16 2024 at 01:05 UTC