Conference Paper (published)
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.
| Status | Published |
|---|---|
| Title of series | Lecture Notes in Computer Science |
| Number in series | 2767 |
| Publication date | 31/12/2003 |
| URL | http://hdl.handle.net/1893/10754 |
| Publisher | Springer |
| Publisher URL | http://link.springer.com/…3-540-39979-7_10 |
| Place of publication | Berlin Heidelberg |
| ISSN of series | 0302-9743 |
| ISBN | 978-3-540-20175-5 |
| Conference | Combating infinite state using ergo |
| Conference location | Berlin, Germany |
| Dates | – |