TY - GEN
T1 - Boogie meets regions
T2 - 2nd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2008
AU - Banerjee, Anindya
AU - Barnett, Mike
AU - Naumann, David A.
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=69949152092&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=69949152092&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-87873-5_16
DO - 10.1007/978-3-540-87873-5_16
M3 - Conference contribution
AN - SCOPUS:69949152092
SN - 3540878726
SN - 9783540878728
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 177
EP - 191
BT - Verified Software
Y2 - 6 October 2008 through 9 October 2008
ER -