Abstract interpretation and model checking are two approaches to verifying or deriving properties of software and hardware systems. While model checking is applied to finite-state systems (typically hardware), abstract interpretation is usually aimed at infinite-state software systems. Indeed, the very notion of verification by abstraction starts from the assumption that the system under consideration is infinite or very large. Both abstract interpretation and model checking are the subject of major research efforts, both in academic and industrial laboratories, since they hold out the promise of an automatic, "push-button" approach to obtaining guarantees of system behaviour.
This proposal lies in the intersection of abstract interpretation and model checking, an area that has been the subject of active research in recent years, with a number of theoretical studies. Despite this there does not exist a set of well established practical techniques for systematically combining abstract interpretation with model checking, and what tools exist are not mature. On the other hand, there are many contributions, both theoretical and practical, in applying abstract interpretation for establishing safety properties, which are typical problems for model checkers. There are also a few well-developed tools and techniques for "abstract model checking" which apply a limited form of abstraction to model checking.
The main question for investigation in this project is how the framework and accumulated experience of abstract interpretation can be applied to model checking infinite state systems - in short, to define abstract model checking methods that exploit the generality and power of the framework of abstract interpretation. It is also clear that a greater understanding of the relationship between the two fields would be of benefit both in cross-fertilizing results from each area, and also in advancing the overall capabilities of tools in each field. Furthermore light will be shed on other static analyses, especially type-based analysis.
The project focusses on classes of abstraction that were developed in abstract interpretation, with a view to applying them to model checking problems. These are numeric and symbolic abstractions respectively, and combinations of them. Among numeric abstractions can be counted intervals, convex polyhedra and octagons, while symbolic abstractions include string and tree automata, Herbrand term lattices and congruences arising from equality theories. The use of powerful constraint solvers and satisfiability checkers in the implementation of these domains will be studied in the project. Recent breakthroughs in the speed and scalability of satisfiability checkers in particular offer great promise if they can be applied effectively for supporting abstractions.
The project involves several international collaborators and in particular the Madrid Institute for Advanced Studies in Software Development Technologies (IMDEA Software).