Re: [isabelle] Program verification and Isabelle?
You may be interested in the Sunrise project. Although not targeting Java
or C#, only a small imperative language similar to a subset of Pascal, it is
a genuine system for proving partial or total correctness of individual
programs written in the Sunrise language, using the Higher Order Logic
Rather than by translation, which could be considered a "shallow embedding,"
it is based on a "deep embedding" of Sunrise within HOL. Deep embeddings
are much more difficult to create, but once built, have significant
advantages over shallow embeddings.
On 9/29/06, Klaus Ostermann <ostermann at informatik.tu-darmstadt.de> wrote:
I have seen many examples of proving properties of programming languages
as type soundness) in Isabelle.
I wonder whether it is also possible to prove properties of individual
written in some language, say Java or C#. It would of course be tiresome
manually "translate" the program into Isabelle, but in principle it should
possible to "compile" a Java program into an Isabelle specification, e.g.,
partially evaluating a Java semantics written in Isabelle with an input
Has something like this been tried (maybe with another theorem prover)? If
could you give me a reference? If no, are there specific reasons why it
"In Your majesty ride prosperously because of truth, humility, and
And Your right hand shall teach You awesome things." (Psalm 45:4)
This archive was generated by a fusion of
Pipermail (Mailman edition) and