UTP2
swMATH ID:  6342 
Software Authors:  Andrew BUTTERFIELD 
Description:  Unifying Theories of Programming Theorem Prover ( U·(TP)2, ”UTPsquared”, or UTP2 if stuck in ASCIIland ) is a theorem proving assistant for 2ndorder predicate calculus, designed to support foundational proof work in the Unifying Theories of Programming framework (UTP). Formerly known as Saoithín (pronounced ”Seeheen”) Saoithín is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higherorder logic, alphabets, equational reasoning and “programs as predicates” style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He [HH98] onwards. This paper describes the key features of the theorem prover, with an emphasis on the underlying foundations, and how these affect the design and implementation choices. These key features include: a formalisation of a UTP Theory; support for common proof strategies; sophisticated goal/law matching ; and userdefined language constructs. A simple theory of designs with some proof extracts is used to illustrate the above features. The theorem prover has been used with undergraduate students and we discuss some of those experiences. The paper then concludes with a discussion of current limitations and planned improvements to the tool 
Homepage:  https://www.scss.tcd.ie/andrew.butterfield/Saoithin/ 
Related Software:  Saoithin; Isabelle/HOL; Isabelle/UTP; ProofPower; PVS; Coq; Isabelle/Circus; Z; ArcAngel; Isar; UTPCalc; Maude; Haskell; Isabelle/Isar; Stratego; HOL; Sledgehammer; ML; Isabelle; CZT 
Cited in:  5 Publications 
Standard Articles
2 Publications describing the Software, including 2 Publications in zbMATH  Year 

The logic of \(U\cdot(TP)^{2}\). Zbl 1452.68261 Butterfield, Andrew 
2013

Saoithín: a theorem prover for UTP. Zbl 1309.68039 Butterfield, Andrew 
2010

all
top 5
Cited by 6 Authors
3  Butterfield, Andrew 
1  Cavalcanti, Ana 
1  Foster, Simon 
1  Freitas, Leo 
1  Ribeiro, Pedro 
1  Zeyda, Frank 
Cited in 1 Serial
1  Theoretical Computer Science 
Cited in 2 Fields
5  Computer science (68XX) 
1  Mathematical logic and foundations (03XX) 