Proofs that count

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Research output: Contribution to journalArticle

2 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)
Pages (from-to)151-164
Number of pages14
JournalACM SIGPLAN Notices
Volume49
Issue number1
StatePublished - Jan 13 2014
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Keywords

  • Concurrency
  • Static Analysis
  • Verification

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

  • Cite this

    Farzan, A., Kincaid, Z., & Podelski, A. (2014). Proofs that count. ACM SIGPLAN Notices, 49(1), 151-164.