Using PVS for an assertional verification of the RPC-memory specification problem

J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review


The RPC-Memory Specification Problem has been specified and verified in an assertional method, supported by the verification system PVS. Properties of the components are expressed in the higher-order logic of PVS and all implementations have been verified by means of the interactive proof checker of PVS. A simplification of the memory specification — allowing multiple atomic reads — has been proved correct. Additionally, to increase the confidence in the specification, an implementation-oriented specification of the inner memory is shown to be equivalent to our original property-oriented formulation.
Original languageEnglish
Title of host publicationFormal Systems Specification: The RPC-Memory Specification Case Study
EditorsM. Broy, S. Merz, K. Spies
Place of PublicationBerlin
ISBN (Print)3-540-61984-4
Publication statusPublished - 1996

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Using PVS for an assertional verification of the RPC-memory specification problem'. Together they form a unique fingerprint.

Cite this