Fast Infinite-State Model Checking in Integer-Based Systems

Опубликовано 6 сентября 2016, 5:11

In this talk we discuss the use of logic for reachability analysis for infinite-state systems. Infinite-state systems are formalised using transition systems over a first-order structure. We establish a common ground relating a large class of algorithms by analysing the connections between the symbolic representation of transition systems and formulas used in various reachability algorithms. We consider in detail the so-called guarded assignment systems and 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. (Joint work with Tatiana Rybina)