Counterexample-guided focus

Andreas Podelski, Thomas Wies

Research output: Contribution to journalArticle

Abstract

The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right treatment of disjunction below and above the universal quantifier. In the closely related setting of shape analysis one uses the focus operator in order to adapt the treatment of disjunction (and thus the efficiency-precision tradeoff) to the individual program statement. One promising research direction is to design parameterized versions of the focus operator which allow the user to fine-tune the focus operator not only to the individual program statements but also to the specific verification task. We carry this research direction one step further. We fine-tune the focus operator to each individual step of the analysis (for a specific verification task). This fine-tuning must be done automatically. Our idea is to use counterexamples for this purpose. We realize this idea in a tool that automatically infers quantified invariants for the verification of a variety of heapmanipulating programs.

Original languageEnglish (US)
Pages (from-to)249-260
Number of pages12
JournalACM SIGPLAN Notices
Volume45
Issue number1
StatePublished - Jan 1 2010

    Fingerprint

Keywords

  • Abstraction Refinement
  • Data Structures
  • Predicate Abstraction
  • Quantified Invariants
  • Shape Analysis

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Podelski, A., & Wies, T. (2010). Counterexample-guided focus. ACM SIGPLAN Notices, 45(1), 249-260.