License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2012.34
URN: urn:nbn:de:0030-drops-38897
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3889/
Go to the corresponding LIPIcs Volume Portal

Parthasarathy, Madhusudan

Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures

pdf-format:
50.pdf (0.2 MB)

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.

BibTeX - Entry

@InProceedings{parthasarathy:LIPIcs:2012:3889,
  author =	{Madhusudan Parthasarathy},
  title =	{{Automated Reasoning and Natural Proofs for Programs Manipulating Data Structures}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) },
  pages =	{34--35},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2012/3889},
  URN =		{urn:nbn:de:0030-drops-38897},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.34},
  annote =	{Keywords: logic, heap structures, data structures, program verification}
}

Keywords: logic, heap structures, data structures, program verification
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Issue Date: 2012
Date of publication: 14.12.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI