Re: [isabelle] Program verification and Isabelle?



I work on the proof of properties of programs in SystemC (a c++ class library) and use the compilation approach (with shallow embedding). The work is quite preliminary and still has no external references to it.

But an overview of deep/shallow embeddings can be found in:

Azurat, A. & Prasetya, I.
A survey on Embedding Programming logics in a Theorem Prover
Inst. of Information and Comp. Science, Utrecht Univ., 2002
Tech report: UU-CS-2002-007

You can, in addition to extending Norberts sequential environment, also consider compiling towards an already existing java embedding (which might most likely need some extending too):
von Oheimb, D. 
Analyzing Java in Isabelle/HOL-Formalization, Type Safety and Hoare Logic
Ph.D. thesis, Technische Universität München, 2001

Regards,
Primrose
 
-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Klaus Ostermann
Sent: Friday, September 29, 2006 10:47 AM
To: isabelle-users at cl.cam.ac.uk
Subject: [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 been tried?

Regards,
Klaus





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