Counterexample-guided focus

Andreas Podelski, Thomas Wies

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

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 heap-manipulating programs.

Original languageEnglish (US)
Title of host publicationPOPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages249-260
Number of pages12
DOIs
StatePublished - 2010
Event37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10 - Madrid, Spain
Duration: Jan 17 2010Jan 23 2010

Other

Other37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10
CountrySpain
CityMadrid
Period1/17/101/23/10

Fingerprint

Tuning

Keywords

  • Abstraction refinement
  • Data structures
  • Predicate abstraction
  • Quantified invariants
  • Shape analysis

ASJC Scopus subject areas

  • Software

Cite this

Podelski, A., & Wies, T. (2010). Counterexample-guided focus. In POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 249-260) https://doi.org/10.1145/1706299.1706330

Counterexample-guided focus. / Podelski, Andreas; Wies, Thomas.

POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. p. 249-260.

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

Podelski, A & Wies, T 2010, Counterexample-guided focus. in POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 249-260, 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10, Madrid, Spain, 1/17/10. https://doi.org/10.1145/1706299.1706330
Podelski A, Wies T. Counterexample-guided focus. In POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. p. 249-260 https://doi.org/10.1145/1706299.1706330
Podelski, Andreas ; Wies, Thomas. / Counterexample-guided focus. POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. pp. 249-260
@inproceedings{214714c2b0374073aab7ccfbd532400d,
title = "Counterexample-guided focus",
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 heap-manipulating programs.",
keywords = "Abstraction refinement, Data structures, Predicate abstraction, Quantified invariants, Shape analysis",
author = "Andreas Podelski and Thomas Wies",
year = "2010",
doi = "10.1145/1706299.1706330",
language = "English (US)",
isbn = "9781605584799",
pages = "249--260",
booktitle = "POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

TY - GEN

T1 - Counterexample-guided focus

AU - Podelski, Andreas

AU - Wies, Thomas

PY - 2010

Y1 - 2010

N2 - 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 heap-manipulating programs.

AB - 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 heap-manipulating programs.

KW - Abstraction refinement

KW - Data structures

KW - Predicate abstraction

KW - Quantified invariants

KW - Shape analysis

UR - http://www.scopus.com/inward/record.url?scp=77950892464&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77950892464&partnerID=8YFLogxK

U2 - 10.1145/1706299.1706330

DO - 10.1145/1706299.1706330

M3 - Conference contribution

SN - 9781605584799

SP - 249

EP - 260

BT - POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

ER -