Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Shape Refinement through Explicit Heap Analysis
 
conference paper

Shape Refinement through Explicit Heap Analysis

Beyer, Dirk
•
Henzinger, Thomas A.  
•
Théoduloz, Grégory  
Show more
Rosenblum, D.S.
•
Taentzer, G.
2010
Fundamental Approaches to Software Engineering. FASE 2010
13th Internation Conference on Fundamental Approaches to Software Engineering (FASE)

Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-12029-9_19
Author(s)
Beyer, Dirk
Henzinger, Thomas A.  
Théoduloz, Grégory  
Zufferey, Damien
Editors
Rosenblum, D.S.
•
Taentzer, G.
Date Issued

2010

Publisher

Springer

Published in
Fundamental Approaches to Software Engineering. FASE 2010
Series title/Series vol.

Lecture Notes in Computer Science; 6013

Start page

263

End page

277

Subjects

Software Model Checking

•

Shape Analysis

URL

URL

http://www.mathematik.uni-marburg.de/~swt/fase2010/
Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
MTC  
Event nameEvent placeEvent date
13th Internation Conference on Fundamental Approaches to Software Engineering (FASE)

Paphos, Cyprus

March 22-26, 2010

Available on Infoscience
February 1, 2010
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/46344
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés