我要吃瓜

Conference Paper (published)

Combating infinite state using ergo

Details

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
URL
PublisherSpringer
Publisher URL
Place of publicationBerlin Heidelberg
ISSN of series0302-9743
ISBN978-3-540-20175-5
ConferenceCombating infinite state using ergo
Conference locationBerlin, Germany
Dates