Computer Science Logic and 8th Kurt Gödel Colloquium Ahmed Bouajjani: Verification of Infinite State System

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page The aim of this tutorial is to give an overview on the state-of-the-art in infinite-state model checking and its applications. We present a unified modeling framework based on word/term rewrite systems and show its relevance in reasoning about several important classes of systems (communication protocols, parametrized distributed algorithms, multithreaded programs, etc). Then, we address the verification problem of various classes of such models. We consider especially the basic problem of reachability analysis which consists in computing a (finite) representation of the (potentially infinite) set of reachable configurations. We show the main existing approaches to tackle this problem: Specialized constructions for several significant classes of models for which this problem is shown to be decidable, General principles to prove the termination and the completeness of the iterative computation of the reachability sets for classes of models, Generic constructions and fixpoint acceleration techniques, leading to powerful semi-algorithms applicable to general classes of models in order to compute exact/approximate reachability sets. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-07-09