Conference Proceeding

Combating infinite state using ergo

Citation

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. http://link.springer.com/chapter/10.1007/978-3-540-39979-7_10; https://doi.org/10.1007/978-3-540-39979-7_10

Abstract
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.

StatusPublished
Title of seriesLecture Notes in Computer Science
Number in series2767
Publication date31/12/2003
URLhttp://hdl.handle.net/1893/10754
PublisherSpringer
Publisher URLhttp://link.springer.com/…3-540-39979-7_10
Place of publicationBerlin Heidelberg
ISSN of series0302-9743
ISBN978-3-540-20175-5
ConferenceCombating infinite state using ergo
Conference locationBerlin, Germany
Dates