Model checking

Roscoe leads the development of FDR, a model-checker for refinement in CSP. Recent research has used FDR as a vehicle to tackle state explosion and the parameterised verification problem using techniques such as induction, compression, and data independence. Kwiatkowska's group pioneered quantitative probabilistic model checking techniques and their symbolic implementation, with Parker developing PRISM. Ouaknine and Worrell work on the decidability and complexity of checking classes of timed systems, and also software model checking. Kroening's research addresses both algorithms and applications, including SAT, abstraction refinement, bounded model-checking, decision procedures, and model-checking for C/C++, Verilog, and SystemC. Achievements include a series of papers by Ouaknine and Worrell that settled several outstanding decidability questions about Metric Temporal Logic, most notably the decidability of model-checking this logic on timed automata, a question open for over 15 years. PRISM became established as the internationally leading probabilistic model checker and attracted over £2M support from EPSRC, DTI and industry. FDR has hundreds of academic users and over 20 commercial ones. A Dutch start-up (Verum) has recently raised over £2M capital for a business model centred on FDR, and we have had research grants of nearly £1M to support this tool. Kroening developed the first symbolic software model checkers to reason about low-level programming artefacts such as bit-vector arithmetic and shared variable concurrency.