Re: [isabelle] Program verification and Isabelle?
- To: Klaus Ostermann <ostermann at informatik.tu-darmstadt.de>
- Subject: Re: [isabelle] Program verification and Isabelle?
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Sun, 01 Oct 2006 10:44:00 +0200
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <451CDD6D.firstname.lastname@example.org>
- References: <450EE44B.email@example.com> <450FAF70.firstname.lastname@example.org> <4510D3C9.email@example.com> <4511555A.firstname.lastname@example.org> <451B1920.email@example.com> <Pine.LNX.firstname.lastname@example.org> <451CDD6D.email@example.com>
- User-agent: Thunderbird 22.214.171.124 (Macintosh/20060308)
The compilation approach (without partial evaluation) has been used in
at least two systems: the Loop tool by Huisman, Jacobs et al, and the
Jive system by Mueller, Poetzsch-Heffter and Rauch.
Klaus Ostermann schrieb:
I have seen many examples of proving properties of programming languages
(such as type soundness) in Isabelle.
I wonder whether it is also possible to prove properties of individual
programs written in some language, say Java or C#. It would of course be
tiresome to manually "translate" the program into Isabelle, but in
principle it should be possible to "compile" a Java program into an
Isabelle specification, e.g., by partially evaluating a Java semantics
written in Isabelle with an input program.
Has something like this been tried (maybe with another theorem prover)?
If yes, could you give me a reference? If no, are there specific reasons
why it has not been tried?
This archive was generated by a fusion of
Pipermail (Mailman edition) and