| EPSRC Reference: |
EP/E012973/1 |
| Title: |
NOTOS: New algOrithm for LTL mOdel checking with Satisfiability |
| Principal Investigator: |
Fischer, Dr B |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Electronics and Computer Science |
| Organisation: |
University of Southampton |
| Scheme: |
First Grant Scheme |
| Starts: |
02 April 2007 |
Ends: |
01 April 2010 |
Value (£): |
208,613
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
| System on Chip |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Boolean Satisfiability (SAT) is the paradigmatic NP-complete decision problem. Besides its theoretical interest, SAT finds a vast number of applications in a large number of areas, including system validation by model checking. Over the last decade the area of SAT algorithms has witnessed a remarkable evolution. From an essentially academic curiosity in the early 90s, SAT technology has made great strides, and is now extensively used in a large number of practical applications. The evolution of SAT technology has been marked by a number of key ideas, which have shaped the organisation of current state of the art SAT solvers.Model checking is an essential technique for system validation and, arguably, it is one of the most successful applications of SAT solver technology. The improvements made to SAT solvers motivated their usage in model checking. The first uses of SAT were for Bounded Model Checking (BMC), a potentially incomplete form of model checking. More recent work has addressed completeness issues, in the form of Unbounded Model Checking (UMC). The use of SAT in model checking has yielded remarkable performance gains in different settings, having motivated the widespread offering, by most Electronic Design Automation (EDA) vendors, of commercial tools using SAT-based model checking.Nevertheless, the utilisation of SAT in publicly available robust model checkers is still scarce, the most well-known example being NuSMV. However, in NuSMV SAT is solely used for incomplete forms of bounded model checking. The dissemination of a publicly available SAT-based model checker will enable further research work on SAT-based model checking, and will provide a comparison framework for alternative model checking strategies. Moreover, model checking is a hard computational problem, and the ever increasing complexity of the systems to be verified motivates the development of new effective techniques.The NOTOS project will conduct innovative research on a number of topics in SAT-based model checking, including novel uses of a number of key concepts: resolution proofs and a supporting resolution engine, incremental SAT and incremental model checking, and new uses of interpolants. In addition to the research contributions, the project also entails the development of NOTOS, a fully SAT-based model checker. NOTOS will integrate the most effective techniques for SAT-based model checking, and will seek to compete with the most widely used model checkers, NuSMV and SPIN. Finally, the project will assess the utilisation of the NOTOS model checker in a number of different contexts, including hardware and software systems, and security protocols.The NOTOS project fits with EPSRC's mission and objectives, namely by conducting strategic and applied research in SAT-based model checking, by developing a model checking tool suitable for postgraduate training, and by advancing knowledge and technology in systems verification.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.soton.ac.uk |