Mechanised Theory Engineering in Isabelle

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageEnglish
Title of host publicationDependable Software Systems Engineering
EditorsMaximilian Irlbeck, Doron Peled, Alexander Pretschner
PublisherIOS Press
ISBN (Print)978-1-61499-494-7
Publication statusPublished - 2015
EventMarktoberdorf Summer School - Marktoberdorf, Germany
Duration: 29 Jul 201410 Aug 2014

Publication series

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


ConferenceMarktoberdorf Summer School

Cite this