Paper Info
Title
Boogie Meets Regions: A Verification Experience Report
Abstract
We use region logic specifications to verify several programs exhbiting the classic hard problem for object-oriented systems: the framing of heap updates. We use BoogiePL and its associated SMT solver, Z3, to prove both implementations and client code.
Year
DOI
Venue
2008
10.1007/978-3-540-87873-5_16
VSTTE
Keywords
Field
DocType
object-oriented system,region logic specification,boogie meets regions,associated smt solver,client code,classic hard problem,verification experience,heap updates
Framing (construction),Separation logic,Programming language,Computer science,Heap (data structure),Implementation,Proof obligation,Satisfiability modulo theories
Conference
Volume
ISSN
Citations 
5295
0302-9743
13
PageRank 
References 
Authors
0.76
14
3
Name
Order
Citations
PageRank
Anindya Banerjee1132470.68
Mike Barnett261329.03
David Naumann3110184.12