Computer Sciences Colloquium: Reasoning about Infinite-State Systems

Abstract: 

Computerized systems are becoming an integral part of many aspects of our lives. Their correctness is therefore crucial. Many such systems have an infinite state space, resulting from an unbounded domain of variables, an unbounded size of a heap, an unbounded number of components, and so on. This makes checking the correctness of such systems hard, and in many cases undecidable. This talk will focus on verification of safety properties in infinite-state systems. We will first present a novel semi-algorithm, called Universal Property Directed Reachability (UPDR), for proving safety properties of infinite-state systems. UPDR proves safety by inferring inductive invariants in a universal fragment of first-order logic. UPDR terminates when it either discovers a counterexample to the safety property, infers an inductive universal invariant strong enough to establish the desired safety property, or finds a proof that such an invariant does not exist. We implemented an analyzer based on UPDR, and applied it to a collection of list-manipulating programs, as well as several distributed protocols. Our analyzer was able to automatically infer universal invariants strong enough to establish various safety properties, show the absence of such invariants for certain systems, and detect bugs. All of this, without the need for user-supplied abstraction predicates. We then address the more fundamental question of decidability of inferring inductive invariants in restricted fragments of first-order logic. We prove several decidability and undecidability results. Finally, we propose to tackle the undecidable fragments by an interactive approach for inference of universal inductive invariants.