Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Program verification and Isabelle?


view this post on Zulip Email Gateway (Aug 18 2022 at 09:44):

From: Klaus Ostermann <ostermann@informatik.tu-darmstadt.de>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 09:44):

From: Peter Homeier <phomeier@gmail.com>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 09:45):

From: Tobias Nipkow <nipkow@in.tum.de>
The compilation approach (without partial evaluation) has been used in
at least two systems: the Loop tool by Huisman, Jacobs et al, and the
Jive system by Mueller, Poetzsch-Heffter and Rauch.

Tobias

Klaus Ostermann schrieb:

view this post on Zulip Email Gateway (Aug 18 2022 at 09:46):

From: Norbert Schirmer <norbert.schirmer@web.de>
Hello Klaus Ostermann,

as part of the Verisoft project (www.verisoft.de) I have developed a
verification environment for sequential imperative programs over the last few
years. It's a combination of a deep and shallow embedding and provides a
quite general core language that is suitable to express most common language
constructs of imperative programming languages. Allthough the focus in
Verisoft is on a subset of C, I believe it can also be customized to express
the object-oriented features of languages like Java or C#. I look forward to
someone heading in this direction. So if you are interested have a look at:

http://www4.in.tum.de/~schirmer/verification_environment.html

Norbert

view this post on Zulip Email Gateway (Aug 18 2022 at 09:50):

From: Primrose.Mbanefo@Infineon.com
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


Last updated: Nov 21 2024 at 12:39 UTC