4 papers
The Complexity of Interference: When Rely/Guarantee Does Not Work
Nisansala P. Yatapanage
Rely/Guarantee is a well-known verification technique for reasoning about concurrent programs. However, for some algorithms, devising suitable rely and guarantee conditions is chal…
Rely/Guarantee, Refinement and the ABA Problem: Part 1
Nisansala P. Yatapanage
Rely/guarantee reasoning provides a compositional way of reasoning about concurrency. The ABA problem occurs in many non-blocking concurrent data structures, where a change made by…
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…
PFMC: a parallel symbolic model checker for security protocol verification
Alex James, Alwen Tiu, Nisansala Yatapanage
We present an investigation into the design and implementation of a parallel model checker for security protocol verification that is based on a symbolic model of the adversary, wh…