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
theorem prover.

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.

Please see

http://www.trustworthytools.com/id13.html

Peter

On 9/29/06, Klaus Ostermann <ostermann at informatik.tu-darmstadt.de> wrote:

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?

Regards,
Klaus


--
"In Your majesty ride prosperously because of truth, humility, and
righteousness;
And Your right hand shall teach You awesome things." (Psalm 45:4)




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.