Document Open Access Logo

Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures

Author Madhusudan Parthasarathy

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2012.34.pdf
  • Filesize: 234 kB
  • 2 pages

Document Identifiers

Subject Classification

Keywords
  • logic
  • heap structures
  • data structures
  • program verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We consider the problem of automatically verifying programs that manipulate a dynamic heap, maintaining complex and multiple data-structures, given modular pre-post conditions and loop invariants. We discuss specification logics for heaps, and discuss two classes of automatic procedures for reasoning with these logics. 
The first identifies fragments of logics that admit completely decidable reasoning. The second is a new approach called the natural proof method that builds proof procedures for very expressive logics that are automatic and sound (but incomplete), and that embody natural proof tactics learnt from manual verification.

Cite As Get BibTex

Madhusudan Parthasarathy. Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 34-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.FSTTCS.2012.34

Author Details

Madhusudan Parthasarathy
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact