Flat Acceleration in Symbolic Model Checking

Abstract. Symbolic model checking provides partially effective verification procedures that can handle systems with an infinite state space. So-called “acceleration techniques” enhance the convergence of fixpoint computations by computing the transitive closure of some transitions. In this paper we develop a new framework for symbolic model checking with accelerations. We also propose and analyze new symbolic algorithms using accelerations to compute reachability sets. Key words: verification of infinite-state systems, symbolic model checking, acceleration.

• Type: Conference
• Year: 2005
• Where: ATVA
• Authors: Sébastien Bardin, Alain Finkel, Jérôme Leroux, Ph. Schnoebelen
• Keywords: ATVA 2005, Effective Verification Procedures, Model Checking, Symbolic Model