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
The University of Southampton

Welcome to ePrints Soton

Welcome to the University of Southampton Institutional Research Repository, ePrints Soton. This repository contains details and, if available, downloads of our research output.

Information on this website should be updated via PURE, our research management system. 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.

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.

Contact ePrints Soton: eprints@soton.ac.uk

ePrints Soton supports OAI 2.0 with a base URL of http://eprints.soton.ac.uk/cgi/oai2

This repository has been built using EPrints software, developed at the University of Southampton, but available to everyone to use.

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

© School of Electronics and Computer Science of the University of Southampton