Trustworthy Systems

Extensible specifications for automatic re-use of specifications and proofs


Daniel Matichuk and Toby Murray




One way to reduce the cost of formally verifying a program is to perform proofs over a specification of its behaviour, which its implementation refines. However, interesting programs must often satisfy multiple properties. Ideally, each property should be proved against the most abstract specification for which it holds, to simplify reasoning and increase its robustness against later tweaks to the program's implementation.

In this short paper we introduce extensible specifications, a technique for writing specifications that allows properties to be proved at the highest levels of abstraction, while avoiding having to write and maintain a different specification for each property being proved. We explain how we applied this idea in the context of verifying confidentiality enforcement for the seL4 microkernel, saving us significant code and proof duplication.

BibTeX Entry

    address          = {Thessaloniki, Greece},
    author           = {Matichuk, Daniel and Murray, Toby},
    booktitle        = {10th International Conference on Software Engineering and Formal Methods},
    keywords         = {formal verification re-use refinement sel4 extensible specifications},
    month            = dec,
    pages            = {8},
    paperurl         = {},
    title            = {Extensible Specifications for Automatic Re-Use of Specifications and Proofs},
    year             = {2012}