By the same authors

Mechanised Theory Engineering in Isabelle

Research output: Chapter in Book/Report/Conference proceedingChapter

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationDependable Software Systems Engineering
DatePublished - 2015
Pages246-287
PublisherIOS Press
EditorsMaximilian Irlbeck, Doron Peled, Alexander Pretschner
Volume40
Original languageEnglish
ISBN (Print)978-1-61499-494-7

Publication series

NameNATO Science for Peace and Security Series, D: Information and Communication Security
PublisherIOS Press
Volume40

Abstract

This is an introduction to mechanised theory engineering in Isabelle, an LCF-style interactive theorem prover. We introduce an embedding of Hoare & He's Unifying Theories of Programming (UTP) in Isabelle (named Isabelle/UTP) and show how to mechanise two key theories: relations and designs. These theories are sufficient to give an account of the partial and total correctness of nondeterministic sequential programs and of networks of reactive processes. A tutorial introduction to each theory is interspersed with its formalisation and with mechanised proofs of relevant properties and theorems. The work described here underpins specification languages such as Circus, which combines state-rich imperative operations, communication and concurrency, object orientation, references and pointers, real time, and process mobility, all with denotational, axiomatic, algebraic, and operational semantics.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations