For the most recent entries see the Petri Nets Newsletter.

Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.

Lehmann, Helko; Leuschel, Michael

In: Maurice Bruynooghe (Ed.): Lecture Notes in Computer Science, Vol. 3018: Logic Based Program Synthesis and Transformation: 13th International Symposium, LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, pages 1-19. Springer-Verlag, 2004.

Abstract: In this paper we discuss the similarities between program specialisation and inductive theorem proving, and then show how program specialisation can be used to perform inductive theorem proving. We then study this relationship in more detail for a particular class of problems (verifying infinite state Petri nets) in order to establish a clear link between program specialisation and inductive theorem proving. In particular, we use the program specialiser ecce to generate specifications, hypotheses and proof scripts in the theory format of the proof assistant Isabelle. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of ecce's verification process and of the correspondence between program specialisation and inductive theorem proving.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography