[isabelle] Program verification and Isabelle?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and