2026-08-16T16:18:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:512 2024-03-06T11:06:33Z ddc:004 open_access

On Algorithms and Complexity for Sets with Cardinality Constraints Kuncak, Viktor Rinard, Martin Marnette, Bruno Static analysis data structure consistency program verification decision procedures 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Viktor Kuncak and Martin Rinard and Bruno Marnette 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.05431.4 urn:nbn:de:0030-drops-5125 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.4 eng https://creativecommons.org/licenses/by/4.0/legalcode