On the complexity of model checking counter automata

Theoretical and practical aspects of the verification of infinite-state systems have attracted a lot of interest in the verification community throughout the last 30 years. One goal is to identify classes of infinite-state systems that admit decidable decision problems on the one hand, and which are sufficiently general to model systems, programs or protocols with unbounded data or recursion depth on the other hand. The first part of this thesis is concerned with the computational complexity of verifying counter automata, which are a fundamental and widely studied class of infinite-state systems. Counter automata consist of a finite-state controller manipulating a finite number of counters ranging over the naturals. A classic result by Minsky states that reachability in counter automata is undecidable already for two counters. One restriction that makes reachability decidable and that this thesis primarily focuses on is the restriction to one counter. A main result of this thesis is to show that reachability in one-counter automata with counter updates encoded in binary is NP-complete, which solves a problem left open by Rosier and Yen in 1986. We also consider parametric one-counter automata, in which counter updates can be parameters ranging over the naturals. Reachability for this class asks whether there are values of the parameters such that a target configuration can be reached from an initial configuration. This problem is also shown to be NP-complete. Subsequently, we establish decidability and complexity results of model checking problems for one-counter automata with and without parameters for specifications written in EF, CTL and LTL. The second part of this thesis is about the verification of programs with pointers and linked lists in the framework of separation logic. We consider the fragment of separation logic introduced by Berdine, Calcagno and O'Hearn in 2004 and the problem of deciding entailment between formulae of this fragment. We improve the known coNP upper bound and show that this problem can actually be solved in polynomial time. This result is based on a novel approach in which we represent separation logic formulae as graphs and decide entailment between them by checking for the existence of a graph homomorphism. We complement this result by considering various natural extensions of this fragment which make entailment coNP-hard.