Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL

TL;DR

This paper introduces Interaction Trees in Isabelle/HOL as a unified framework for executing and verifying models, enabling coherent analysis and proof of software behaviors across diverse semantics.

Contribution

It mechanises Interaction Trees in Isabelle/HOL, unifying execution and deductive verification for various models and semantics, with automation support.

Findings

ITrees can encode infinite transition systems and are inherently executable.

The framework supports verification of stateful, concurrent, and abstract models.

ITrees enable model animation through Isabelle's code generator.

Abstract

Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this paper, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and \Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.