Computer Science Logic and 8th Kurt Gödel Colloquium
Tatiana Rybina, Andrei Voronkov: Fast Infinite-State Model Checking in Integer-Based Systems
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
In this paper we discuss the use of logic for reachability analysis for infinite-state systems. Infinite-state systems are formalized using transition systems over a first-order structure. We establish a common ground relating a large class of algorithms by analyzing the connections between the symbolic representation of transition systems and formulas used in various reachability algorithms. We consider in detail the so-called \emph{guarded assignment systems} and \emph{local reachability algorithms}. We show how an implementation of local reachability algorithms and a new incremental algorithm for finding Hilbert's base in the system \Brain\ resulted in much faster reachability checking than in systems using constraint libraries and decision procedures for Presburger's arithmetic. Experimental results demonstrate that problems in protocol verification which are beyond the reach of other existing systems can be solved completely automatically.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-07-09 Valid HTML 4.01! Valid CSS! Debian