Infinite State Model Checking using Partial Evaluation (this project has ended)
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
and considerable human ingenuity is still required.
most software systems cannot be modelled directly by a
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.
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
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
for the validation of business-critical systems.