Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

TY - JOUR

T1 - Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

AU - Foster, Simon David

AU - Baxter, James

AU - Cavalcanti, Ana Lucia Caneca

AU - Woodcock, Jim

AU - Zeyda, Frank

N1 - © 2020 Elsevier B.V. All rights reserved. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. 45 pages, submitted to Science of Computer Programming, March 2019

PY - 2020/6/26

Y1 - 2020/6/26

N2 - The growing complexity and diversity of models used for engineering dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration requires unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He’s Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantics. These can be further applied in the development of verification tools, harnessing Isabelle’s proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms.

AB - The growing complexity and diversity of models used for engineering dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration requires unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He’s Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantics. These can be further applied in the development of verification tools, harnessing Isabelle’s proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms.

KW - cs.LO

KW - cs.FL

U2 - 10.1016/j.scico.2020.102510

DO - 10.1016/j.scico.2020.102510

M3 - Article

SN - 0167-6423

VL - 197

JO - Science of Computer Programming

JF - Science of Computer Programming

M1 - 102510

ER -