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

Simon David Foster; Chung-Kil Hur; Jim Woodcock

doi:10.1145/3702981

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

Simon David Foster, Chung-Kil Hur, Jim Woodcock

Computer Science

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Article number	108
Number of pages	40
Journal	ACM Transactions on Software Engineering and Methodology
Volume	34
Issue number	4
DOIs	https://doi.org/10.1145/3702981
Publication status	Published - 29 Apr 2025

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the University’s Research Publications and Open Access policy.

Access to Document

10.1145/3702981

Accepted manuscript
This is an author-produced version of the published paper. Uploaded in accordance with the University’s Research Publications and Open Access policy.
Accepted author manuscript, 1.18 MBLicence: CC BY

Cite this

@article{be9cd1aaa23245e78d0d12d7b40a762e,

title = "Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL",

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.",

author = "Foster, {Simon David} and Chung-Kil Hur and Jim Woodcock",

note = "This is an author-produced version of the published paper. Uploaded in accordance with the University{\textquoteright}s Research Publications and Open Access policy. ",

year = "2025",

month = apr,

day = "29",

doi = "10.1145/3702981",

language = "English",

volume = "34",

journal = "ACM Transactions on Software Engineering and Methodology",

issn = "1049-331X",

publisher = "ACM",

number = "4",

}

TY - JOUR

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

AU - Foster, Simon David

AU - Hur, Chung-Kil

AU - Woodcock, Jim

N1 - This is an author-produced version of the published paper. Uploaded in accordance with the University’s Research Publications and Open Access policy.

PY - 2025/4/29

Y1 - 2025/4/29

N2 - 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.

AB - 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.

U2 - 10.1145/3702981

DO - 10.1145/3702981

M3 - Article

SN - 1049-331X

VL - 34

JO - ACM Transactions on Software Engineering and Methodology

JF - ACM Transactions on Software Engineering and Methodology

IS - 4

M1 - 108

ER -