@inbook{a1c3798cac764b68acee119371bcb7cc,
title = "Using PVS for an assertional verification of the RPC-memory specification problem",
abstract = "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.",
author = "J.J.M. Hooman",
year = "1996",
doi = "10.1007/BFb0024433",
language = "English",
isbn = "3-540-61984-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "275--304",
editor = "M. Broy and S. Merz and K. Spies",
booktitle = "Formal Systems Specification: The RPC-Memory Specification Case Study",
address = "Germany",
}