Re: [isabelle] Program verification and Isabelle?

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 MHonArc.