English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Field Constraint Analysis

Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. C. (2006). Field Constraint Analysis. In Verification, Model Checking, and Abstract Interpretation: 7th International Conference, VMCAI 2006 (pp. 157-173). Berlin, Germany: Springer.

Item is

Files

show Files
hide Files
:
field-constraint-analysis.pdf (Any fulltext), 149KB
 
File Permalink:
-
Name:
field-constraint-analysis.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Wies, Thomas1, Author           
Kuncak, Viktor, Author
Lam, Patrick, Author
Podelski, Andreas1, Author           
Rinard, Martin C., Author
Emerson, E. Allen, Editor
Namjoshi, Kedar S., Editor
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We introduce \emph{field constraint analysis}, a new technique for verifying data structure invariants. A field constraint for a field is a formula specifying a set of objects to which the field can point. Field constraints enable the application of decidable logics to data structures which were originally beyond the scope of these logics, by verifying the backbone of the data structure and then verifying constraints on fields that cross-cut the backbone in arbitrary ways. Previously, such cross-cutting fields could only be verified when they were uniquely determined by the backbone, which significantly limits the range of analyzable data structures. Field constraint analysis permits \emph{non-deterministic} field constraints on cross-cutting fields, which allows the verificiation of invariants for data structures such as skip lists. Non-deterministic field constraints also enable the verification of invariants between data structures, yielding an expressive generalization of static type declarations. The generality of our field constraints requires new techniques, which are orthogonal to the traditional use of structure simulation. We present one such technique and prove its soundness. We have implemented this technique as part of a symbolic shape analysis deployed in the context of the Hob system for verifying data structure consistency. Using this implementation we were able to verify data structures that were previously beyond the reach of similar techniques.

Details

show
hide
Language(s): eng - English
 Dates: 2007-02-162006
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 314487
Other: Local-ID: C1256104005ECAFC-761CADE4F91377D6C12570B000587F60-WiesETAL06FieldConstraintAnalysis
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Charleston, SC, USA
Start-/End Date: 2006-01-08

Legal Case

show

Project information

show

Source 1

show
hide
Title: Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 157 - 173 Identifier: -

Source 2

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 3855 Sequence Number: - Start / End Page: - Identifier: -