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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and