University of Limerick Institutional Repository

Saoithin : a theorem prover for UTP

DSpace Repository

Show simple item record Butterfield, Andrew 2011-02-02T20:55:41Z 2011-02-02T20:55:41Z 2010
dc.description peer-reviewed en_US
dc.description.abstract Saoithin is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order 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 user-de ned 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. en_US
dc.publisher Springer-Verlag en_US
dc.relation.ispartofseries Unifying Theories of Programming;6445,2010/ pp. 137-156
dc.subject unifying theories of programming en_US
dc.title Saoithin : a theorem prover for UTP en_US
dc.type Conference item en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.type.restriction none en
dc.contributor.sponsor SFI
dc.relation.projectid 03/CE2/I303_1
dc.relation.projectid 08/RFP/CMS1277
dc.relation.projectid 07/RFP/CMSF186

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account