License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05431.4
URN: urn:nbn:de:0030-drops-5125
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/512/
Go to the corresponding Portal

Kuncak, Viktor ; Rinard, Martin ; Marnette, Bruno

On Algorithms and Complexity for Sets with Cardinality Constraints

pdf-format:
05431.KuncakViktor.Paper.512.pdf (0.5 MB)

Abstract

Complexity of data structures in modern programs presents a
challenge for current analysis and verification tools,
forcing them to report false alarms or miss errors. I will
describe a new approach for verifying programs with complex
data structures. This approach builds on program analysis
techniques, as well as decision procedures and theorem
provers.

The approach is based on specifying interfaces of data
structures by writing procedure preconditions and
postconditions in terms of abstract sets and relations. Our
system then separately verifies that 1) each data structure
conforms to its interface, 2) each data structure interface
is used correctly, and 3) desired high-level
application-specific invariants hold. The system verifies
these conditions by combining decision procedures, theorem
provers, and static analyses, promising an unprecedented
tradeoff between precision and scalability. In the context
of this system, we have developed new decision procedures
for reasoning about sets and their cardinalities, approaches
for extending the applicability of existing decision
procedures, and techniques for modular analysis of
dynamically created data structure instances.

BibTeX - Entry

@InProceedings{kuncak_et_al:DagSemProc.05431.4,
  author =	{Kuncak, Viktor and Rinard, Martin and Marnette, Bruno},
  title =	{{On Algorithms and Complexity for Sets with Cardinality Constraints}},
  booktitle =	{Deduction and Applications},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/512},
  URN =		{urn:nbn:de:0030-drops-5125},
  doi =		{10.4230/DagSemProc.05431.4},
  annote =	{Keywords: Static analysis, data structure consistency, program verification, decision procedures}
}

Keywords: Static analysis, data structure consistency, program verification, decision procedures
Collection: 05431 - Deduction and Applications
Issue Date: 2006
Date of publication: 25.04.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI