| Skip to main content | Skip to sub navigation |

This is now an inactive research group it's members have moved on. You can find them at their new research groups:

ECS Intranet:
NOTOS: New algOrithm for LTL mOdel checking with Satisfiability


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.

Homepage: http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/E012973/1
Type: Normal Research Project
Research Group: Dependable Systems & Software Engineering
Themes: Formal Methods, Design, Automation, Simulation and Optimisation
Dates: 2nd April 2007 to 1st October 2009

Funding

  • EPSRC

Principal Investigators

  • [hidden]

Other Investigators

  • [hidden]
URI: http://id.ecs.soton.ac.uk/project/407
RDF: http://rdf.ecs.soton.ac.uk/project/407

More information


Associated Publications

Number of items: 1.

Cordeiro, L., Fischer, B. and Marques-Silva, J. (2010) Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. In: 17th IEEE International Conference and Workshops on Engineering of Computer-Based Systems, 22-26 March, 2010, St. Anne's College, University of Oxford, UK.

This list was generated on Wed May 16 00:59:45 2012 BST.

Publications included from http://eprints.ecs.soton.ac.uk/view/projects/407.include.