Home | People | Research Projects | Publications | Techreports | Tools | Vacancies | Seminars
This is now an inactive research group it's members have moved on. You can find them at their new research groups:
Research Projects
Formal Methods Projects
Software Engineering Projects
EPSRC Funded

DSSE:Research Projects

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.

Homepage: http://www.ecs.soton.ac.uk/~mal/ISM.html
Type: Normal Research Project
Research Group: Dependable Systems & Software Engineering
Themes: Formal Methods, Software Engineering, E-Business Technologies
Dates: 1st August 2000 to 30th May 2002


  • EPSRC GR/N11667/01

Principal Investigators

  • [hidden]

Other Investigators

  • hel99r

Associated Publications

Welcome to ePrints Soton - ePrints Soton

Welcome to ePrints Soton

ePrints is no longer available to login or deposit outputs, although you can still use ePrints for searching.

All research outputs must now be deposited in Pure, the University's research information system - https://pure.soton.ac.uk

All records deposited in Pure will appear in ePrints.

For guidance on uploading your outputs to Pure, please consult the Pure support page http://library.soton.ac.uk/openaccess/Pure

For issues and queries on outputs and open access, please contact the ePrints team at eprints@soton.ac.uk or view the University's Pure support pages at: http://www.southampton.ac.uk/research/researcher-support/pure.page

Research outputs already deposited in ePrints will be automatically transferred to Pure.

Datasets will be transferred to Pure over the next few months, please email researchdata@soton.ac.uk with any queries.

Welcome to the University of Southampton Institutional Research Repository ePrints Soton.

Repository Policies & Help

University of Southampton policies regarding the ePrints Soton research repository.
Latest Additions

View items added to the repository in the past week.
Search Repository

Search the repository using a full range of fields. Use the search field at the top of the page for a quick search.
Browse Repository

Browse the items in the repository by subject.
© School of Electronics and Computer Science of the University of Southampton