Infinite State Model Checking using Partial Evaluation (this project has ended)
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.
Welcome to the University of Southampton Institutional Research Repository, ePrints Soton. This repository contains details and, if available, downloads of our research output.
