2026-07-23T06:52:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3889 2024-03-06T10:34:30Z ddc:004 open_access

Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures Parthasarathy, Madhusudan logic heap structures data structures program verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Madhusudan Parthasarathy 2012 Is Part Of LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2012.34 urn:nbn:de:0030-drops-38897 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.34 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode