Proof Techniques

In the ADVENT project, we have developed a number of custom verification techniques, such as decomposition principles, program logics, and coinductive definitions for reasoning about programs.

Decomposition techniques

Given the gigantic size of common systems software, the only way to verify it is by decomposing the verification of complex pieces of software into that of smaller and simpler ones. We have developed corresponding decomposition techniques in several domains:

• shared-memory concurrent libraries (representative paper)
• software transactional memory (representative paper)
• eventually consistent databases (representative paper)
• preemptive operating system kernels (representative paper)

Coinductive techniques

Coinduction is a general technique for reasoning about greatest fixpoints. These arise often in computer science, when reasoning about program equivalence (e.g., using bisimulations) or about programs operating on infinite data (e.g., streams).

• Stuttering parametric bisimulations: a technique for modular reasoning about the equivalence of programs with higher-order state and continuations.
• Parametric inter-language simulations: a technique for modular reasoning about the correctness of the compilation of programs with higher-order state and continuations.

Idiom-based reasoning techniques

Concurrent components in system software are highly-optimised designs. Developers manage the induced complexity using informal spatio-temporal arguments in which they make claims that concurrent threads access the shared data only where and when they are allowed to and idiomatic implementation practices. In the context of the ADVENT project, we have developed reasoning techniques that formalise these arguments and idioms.

• Extensions of separation logic which are specialised to capture particular forms of spatio-temporal synchronization (representative paper).
• Reductions of the verification of concurrent data structures into proving certain spatio-temporal architectural aspects of their implementation (representative paper).