Automated reasoning and natural proofs for programs manipulating data structures

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication32nd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012
Pages34-35
Number of pages2
DOIs
StatePublished - 2012
Event32nd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012 - Hyderabad, India
Duration: Dec 15 2012Dec 17 2012

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume18
ISSN (Print)1868-8969

Other

Other32nd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012
Country/TerritoryIndia
CityHyderabad
Period12/15/1212/17/12

Keywords

  • Data structures
  • Heap structures
  • Logic
  • Program verification

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Automated reasoning and natural proofs for programs manipulating data structures'. Together they form a unique fingerprint.

Cite this