TY - GEN

T1 - Proofs that count

AU - Farzan, Azadeh

AU - Kincaid, Zachary

AU - Podelski, Andreas

PY - 2014/2/11

Y1 - 2014/2/11

N2 - 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.

AB - 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.

KW - concurrency

KW - static analysis

KW - verification

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

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

U2 - 10.1145/2535838.2535885

DO - 10.1145/2535838.2535885

M3 - Conference contribution

AN - SCOPUS:84893443562

SN - 9781450325448

T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SP - 151

EP - 164

BT - POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

T2 - 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014

Y2 - 22 January 2014 through 24 January 2014

ER -