1 citations · 1 across the 1 of their papers we have counts for
4 papers · 1 filter
Reasoning about concurrent loops and recursion with rely-guarantee rules
Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones
The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. We…
Reasoning about expression evaluation under interference
Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke
Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for…
Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols
Nisansala P. Yatapanage, Cliff B. Jones
The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptio…
Data reification in a concurrent rely-guarantee algebra
Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones
Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of program…