Conference Proceeding

Combating infinite state using ergo


Robinson P & Shankland C (2003) Combating infinite state using ergo. In: Konig H, Heiner M & Wolisz A (eds.) Formal Techniques for Networked and Distributed Systems - FORTE 2003. Lecture Notes in Computer Science, 2767. Combating infinite state using ergo, Berlin, Germany, 29.09.2003-02.10.2003. Berlin Heidelberg: Springer, pp. 144-159.;

Symbolic transition systems can be used to represent infinite state systems in a finite manner. The modal logic FULL, defined over symbolic transition systems, allows properties over infinite state to be expressed, establishing necessary constraints on data. We present here a theory and tactics for FULL, developed using Ergo, a generalised sequent calculus style theorem prover allowing interactive proofs. This allows exploitation of the underlying symbolic transition system and reasoning about symbolic values.

Title of seriesLecture Notes in Computer Science
Number in series2767
Publication date31/12/2003
Publisher URL…3-540-39979-7_10
Place of publicationBerlin Heidelberg
ISSN of series0302-9743
ConferenceCombating infinite state using ergo
Conference locationBerlin, Germany