| dc.contributor.author | KOUTAVAS, VASILEIOS | en |
| dc.contributor.editor | Gilles Barth, Alberto Pardo, Gerardo Schneider | en |
| dc.date.accessioned | 2014-01-23T14:52:16Z | |
| dc.date.available | 2014-01-23T14:52:16Z | |
| dc.date.created | 2011 | en |
| dc.date.issued | 2011 | en |
| dc.date.submitted | 2011 | en |
| dc.identifier.citation | 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 - 171 | en |
| dc.identifier.other | Y | en |
| dc.identifier.uri | http://hdl.handle.net/2262/67872 | |
| dc.description | PUBLISHED | en |
| dc.description | Montevideo, Uruguay | en |
| dc.description.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. | en |
| dc.description.sponsorship | SFI | en |
| dc.format.extent | 155 | en |
| dc.format.extent | 171 | en |
| dc.language.iso | en | en |
| dc.publisher | Springer Berlin Heidelberg | en |
| dc.relation.ispartofseries | 7041 | en |
| dc.rights | Y | en |
| dc.subject | Hoare-Logic | en |
| dc.subject | Verification | en |
| dc.title | Reverse Hoare Logic | en |
| dc.title.alternative | Lecture Notes in Computer Science | en |
| dc.title.alternative | oftware Engineering and Formal Methods | en |
| dc.type | Conference Paper | en |
| dc.type.supercollection | scholarly_publications | en |
| dc.type.supercollection | refereed_publications | en |
| dc.identifier.peoplefinderurl | http://people.tcd.ie/vkoutav | en |
| dc.identifier.rssinternalid | 91020 | en |
| dc.identifier.doi | http://dx.doi.org/10.1007/978-3-642-24690-6_12 | en |
| dc.rights.ecaccessrights | OpenAccess | |
| dc.contributor.sponsor | Science Foundation Ireland (SFI) | en |
| dc.contributor.sponsorGrantNumber | SFI 06 IN.1 1898 | en |
