Reverse Hoare Logic
File Type:
PDFItem Type:
Conference PaperDate:
2011Author:
Access:
OpenAccessCitation:
Vasileios Koutavas and Edsko de Vries, Reverse Hoare Logic, Lecture Notes in Computer Science, oftware Engineering and Formal Methods, Montevideo, Uruguay, 2011, Gilles Barth, Alberto Pardo, Gerardo Schneider, 7041, Springer Berlin Heidelberg, 2011, 155 - 171Download Item:
Abstract:
We present a novel Hoare-style logic, called Reverse Hoare Logic, which can be used to reason about state reachability of imperative programs. This enables us to give natural specifications to randomized (deterministic or nondeterministic) algorithms. We give a proof system for the logic and use this to give simple formal proofs for a number of illustrative examples. We define a weakest postcondition calculus and use this to show that the proof system is sound and complete.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
SFI 06 IN.1 1898
Author's Homepage:
http://people.tcd.ie/vkoutavDescription:
PUBLISHEDMontevideo, Uruguay
Author: KOUTAVAS, VASILEIOS
Other Titles:
Lecture Notes in Computer Scienceoftware Engineering and Formal Methods
Publisher:
Springer Berlin HeidelbergType of material:
Conference PaperCollections
Series/Report no:
7041Availability:
Full text availableKeywords:
Hoare-Logic, VerificationDOI:
http://dx.doi.org/10.1007/978-3-642-24690-6_12Metadata
Show full item recordLicences: