By the same authors

Using PVS to Prove a Z Refinement: A Case Study

Research output: Contribution to conferencePaper



Publication details

DatePublished - 1997
Original languageUndefined/Unknown


The development of critical systems often places undue trust in the software tools used. This is especially true of compilers, which are a weak link between the source code produced and the object code which is executed. [Stepney, 1993] advocates a method for the production of trusted compilers (i.e. those which are guaranteed to produce object code that is a correct refinement of the source code) by developing a hand proof of a small, but non trivial, compiler by hand, in the Z specification language. This approach is quick, but the type system of Z is too weak to ensure that partial functions are correctly applied.

Here, we present a re-working of that development using the PVS specification and verification system. We describe the problems involved in translating from the partial set theory of Z to the total, higher order logic of the PVS system and the strengths and weaknesses of this approach.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations