Boogie meets regions: A verification experience report

Anindya Banerjee, Mike Barnett, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

14 Scopus citations

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.

Original languageEnglish
Title of host publicationVerified Software
Subtitle of host publicationTheories, Tools, Experiments - Second International Conference, VSTTE 2008, Proceedings
Pages177-191
Number of pages15
DOIs
StatePublished - 2008
Event2nd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2008 - Toronto, ON, Canada
Duration: 6 Oct 20089 Oct 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5295 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2008
Country/TerritoryCanada
CityToronto, ON
Period6/10/089/10/08

Fingerprint

Dive into the research topics of 'Boogie meets regions: A verification experience report'. Together they form a unique fingerprint.

Cite this