Motivation: The past years have seen dramatic growth in the application of model checking techniques to the validation and verification of hardware systems. However, despite the success of model checking, most systems must be substantially simplified (i.e., abstracted) and considerable human ingenuity is still required. Furthermore, most software systems cannot be modelled directly by a finite state system: as soon as some kind of recursion, dynamic or unbounded data structures come into play, an infinite number of states must be verified.
Description The main objective of the project is to study the potential of automatically deriving abstractions for infinite model checking through a combination of existing technology for the automatic control of partial evaluation and abstract interpretation. First successful experiments of this idea have been conducted using the ECCE and LOGEN tools.
The project consists of a theoretical study coupled with the implementation of a combined partial evaluation and abstract interpretation system (based upon ECCE). The practicality of the approach will be gauged on realistic examples, some of them coming from the EPSRC funded ABCD projet for the validation of business-critical systems.