# Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

## TL;DR

This paper introduces Isabelle/UTP, a framework that unifies semantic foundations for diverse formal methods, enabling integrated verification tools within Isabelle based on the Unifying Theories of Programming.

## Contribution

It provides a mechanised, extensible platform for formal semantics unification, supporting diverse paradigms and automating verification processes in Isabelle.

## Key findings

- Developed layered mathematical foundations including lenses and alphabetised predicates.
- Enabled formalisation of multiple computational paradigms within Isabelle.
- Supported automated verification using proof tools for Hoare logic and refinement calculus.

## Abstract

The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on 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 semantic models. 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, including algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms.