Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Automated Verification of Shape and Size Properties Via Separation Logic
verfasst von : Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses
user-definable
shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle
well-founded
inductive predicates using
unfold/fold
reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system.