Proofs that count

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

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

15 Scopus citations

Abstract

Counting arguments are among the most basic proof methods in mathematics. Within the field of formal verification, they are useful for reasoning about programs with infinite control, such as programs with an unbounded number of threads, or (concurrent) programs with recursive procedures. While counting arguments are common in informal, hand-written proofs of such programs, there are no fully automated techniques to construct counting arguments. The key questions involved in automating counting arguments are: how to decide what should be counted?, and how to decide when a counting argument is valid? In this paper, we present a technique for automatically constructing and checking counting arguments, which includes novel solutions to these questions.

Original languageEnglish (US)
Title of host publicationPOPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages151-164
Number of pages14
DOIs
StatePublished - Feb 11 2014
Externally publishedYes
Event41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 - San Diego, CA, United States
Duration: Jan 22 2014Jan 24 2014

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014
CountryUnited States
CitySan Diego, CA
Period1/22/141/24/14

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • concurrency
  • static analysis
  • verification

Fingerprint Dive into the research topics of 'Proofs that count'. Together they form a unique fingerprint.

Cite this