Location
Toggle navigation
HOME
INSTITUTE
Mission
Address
Executive Board
Scientific Members of MPG
Scientific Advisory Board
Board of Trustees
NEWS
Overview
Press Releases
Awards
Spotlights
Campus Event Calendar
25th Anniversary
Employment
DEPARTMENTS
Algorithms & Complexity
Computer Vision and Machine Learning
Internet Architecture
Computer Grapics
Databases and Information Systems
Visual Computing and Artificial Intelligence
Research Group Computational Biology
Automation of Logic
Network and Cloud Systems
PUBLICATIONS
Algorithms & Complexity
Computer Vision and Machine Learning
Internet Architecture
Computer Graphics
Databases and Information Systems
Visual Computing and Artificial Intelligence
Research Group Computational Biology
Automation of Logic
Network and Cloud Systems
Research Reports
Scientific Advisory Board
Curatorship Board
25th anniversary
IMPRS-CS
PEOPLE
SOFTWARE
SERVICES
Joint Central Services
Joint Administration
- Library
- International Office
Joint Scientific IT and Technical Services
- Building and Technical Support
Research Coordination
Representative for Equal Opportunities
- Equal Opportunities
Representative for Severely Disabled Persons
Representative for Safety
Ombudsperson for
Good Scientific Practice
and Doctoral Research
Company Physician
CS@MPG
CS@SAAR
Saarland Informatics Campus
Computer Science Department,
Saarland University
Max Planck Institute for
Software Systems (MPI-SWS)
German Center for
Artificial Intelligence (DFKI)
Center for Security, Privacy
and Accountability (CISPA)
VIA - Saarbrücken Center for
Visual Computing, Interaction
and Artificial Intelligence
Graduate School for
Computer Science
Cluster of Excellence (MMCI)
Max Planck Center for Visual
Computing and Communication
Kaiserslautern-Saarbrücken
Computer Science Cluster
IT Incubator
Publications
Home
Intranet
Server
halma.mpi-inf.mpg.de
Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Wies, Thomas
Kuncak, Viktor
Lam, Patrick
Podelski, Andreas
Rinard, Martin C.
dblp
dblp
dblp
dblp
dblp
Not MPG Author(s):
Kuncak, Viktor
Lam, Patrick
Rinard, Martin C.
Editor(s):
Emerson, E. Allen
Namjoshi, Kedar S.
dblp
dblp
Not MPII Editor(s):
Emerson, E. Allen
Namjoshi, Kedar S.
BibTeX cite key*:
WiesETAL06FieldConstraintAnalysis
Title, Booktitle
Title*:
Field Constraint Analysis
Attachment(s)
:
field-constraint-analysis.pdf (148.49 KB)
Booktitle*:
Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006
Event, URLs
Conference URL::
Downloading URL:
http://www.springerlink.com/content/731j75527670t635/fulltext.pdf
Event Address*:
Charleston, SC, USA
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
8 January 2006
Event End Date:
10 January 2006
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
3855
Number:
Month:
January
Pages:
157-173
Year*:
2006
VG Wort Pages:
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) 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.
URL for the Abstract:
http://dx.doi.org/10.1007/11609773_11
Download
Access Level:
Public
Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort
BibTeX Entry:
@INPROCEEDINGS
{
WiesETAL06FieldConstraintAnalysis
,
AUTHOR = {Wies, Thomas and Kuncak, Viktor and Lam, Patrick and Podelski, Andreas and Rinard, Martin C.},
EDITOR = {Emerson, E. Allen and Namjoshi, Kedar S.},
TITLE = {Field Constraint Analysis},
BOOKTITLE = {Verification, Model Checking, and Abstract Interpretation : 7th International Conference, VMCAI 2006},
PUBLISHER = {Springer},
YEAR = {2006},
VOLUME = {3855},
PAGES = {157--173},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Charleston, SC, USA},
MONTH = {January},
}
Entry last modified by Christine Kiesel, 01/28/2008
Edit History (please click the blue arrow to see the details)
Edit History (please click the blue arrow to see the details)
Editor(s)
Thomas Wies
Created
11/05/2005 05:06:37 PM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Thomas Wies
Thomas Wies
Thomas Wies
Thomas Wies
Edit Dates
16.02.2007 22:55:44
01/30/2006 05:24:23 PM
11/07/2005 03:29:43 PM
11/05/2005 05:09:40 PM
11/05/2005 05:06:37 PM
Attachment Section
Attachment Section
field-constraint-analysis.pdf
field-constraint-analysis.pdf