License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-5125
URL: http://drops.dagstuhl.de/opus/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:
Document 1.pdf (558 KB)


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:DSP:2006:512,
  author =	{Viktor Kuncak and Martin Rinard and Bruno Marnette},
  title =	{On Algorithms and Complexity for Sets with Cardinality Constraints},
  booktitle =	{Deduction and Applications},
  year =	{2006},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  number =	{05431},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2006/512},
  annote =	{Keywords: Static analysis, data structure consistency, program verification, decision procedures}
}

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


DROPS-Home | Fulltext Search | Imprint Published by LZI