The University of Southampton

NOTOS: New algOrithm for LTL mOdel checking with Satisfiability

Date:
2007-2009
Themes:
Formal Methods, Design, Automation, Simulation and Optimisation
Funding:
EPSRC

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.

Primary investigator

  • Joao Marques-Silva

Secondary investigator

  • Florian Letombe

Associated research group

  • Dependable Systems & Software Engineering
Share this project FacebookGoogle+TwitterWeibo

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.

×