Machine−Assisted Theorem−Proving for Software Engineering
Andrew Martin
Abstract
The thesis describes the production of a large prototype proof system for Z and a tactic language in which the proof tactics used in a wide range of systems (including the system described here) can be discussed.
Institution
OUCL
Month
July
Number
PRG121
Pages
137
Year
1996