PDF

URL

BibTeX

DOI

Abstract. Conventional software model-checking involves (i) creating an abstract model of a complex application; (ii) validating this model against the application; and (iii) checking safety properties against the abstract model. To non-experts, steps (i) and (ii) are often the most daunting. Firstly how does one decide which aspects of the application to include in the abstract model? Secondly, how does one determine whether the abstraction inadvertently “hides” critical bugs? Similarly, if a counter-example is found, how does one determine whether this is a genuine bug or just a modelling artifact?

Authors. Anil Madhavapeddy, Dave Scott and Richard Sharp

See Also. This publication was part of the Functional Internet Services project.

News Updates

Aug 2005. «» Workshop paper on temporal automata for protocol specifications at SPIN 2005.

Jun 2005. «» Blogged about the OpenBSD C2K5 hackathon trip in Canada.