*To*: "Klaus Ostermann" <ostermann at informatik.tu-darmstadt.de>*Subject*: Re: [isabelle] Program verification and Isabelle?*From*: "Peter Homeier" <phomeier at gmail.com>*Date*: Sat, 30 Sep 2006 10:37:50 -0400*Cc*: isabelle-users at cl.cam.ac.uk, Peter Vincent Homeier <palantir at trustworthytools.com>*In-reply-to*: <451CDD6D.2050901@informatik.tu-darmstadt.de>*References*: <450EE44B.8010009@cs.utexas.edu> <450FAF70.5090508@in.tum.de> <4510D3C9.70205@cs.utexas.edu> <4511555A.4070804@in.tum.de> <451B1920.1070607@rsise.anu.edu.au> <Pine.LNX.4.63.0609281126240.7816@atbroy100.informatik.tu-muenchen.de> <451CDD6D.2050901@informatik.tu-darmstadt.de>

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)

**References**:**[isabelle] questions***From:*Jared Davis

**Re: [isabelle] questions***From:*Tobias Nipkow

**[isabelle] Simplifier questions***From:*Jared Davis

**Re: [isabelle] Simplifier questions***From:*Tobias Nipkow

**[isabelle] Theory loader: cannot update finished theory "Main"***From:*Jeremy Dawson

**Re: [isabelle] Theory loader: cannot update finished theory "Main"***From:*Makarius

**[isabelle] Program verification and Isabelle?***From:*Klaus Ostermann

- Previous by Date: Re: [isabelle] LaTeX conversion
- Previous by Thread: [isabelle] Program verification and Isabelle?
- Next by Thread: Re: [isabelle] questions
- Cl-isabelle-users September 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list