Recent developments in FDR

Philip Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, and James Worrell

We describe and report upon various substantial extensions of the CSP refinement checker FDR including (i) the direct ability to handle real-time processes; (ii) the incorporation of bounded model checking technology; (iii) the development of conservative and highly efficient static analysis algorithms for guaranteeing livelock-freedom; and (iv) the development of automated CEGAR technology.

Proceedings of CAV 12, LNCS 7358, 2012. 6 pages.

PDF © 2012 Springer-Verlag.

Imprint / Data Protection