TY - GEN

T1 - Proof spaces for unbounded parallelism

AU - Farzan, Azadeh

AU - Kincaid, Zachary

AU - Podelski, Andreas

PY - 2015/1/14

Y1 - 2015/1/14

N2 - In this paper, we present a new approach to automatically verify multi-threaded programs which are executed by an unbounded number of threads running in parallel. The starting point for our work is the problem of how we can leverage existing automated verification technology for sequential programs (abstract interpretation, Craig interpolation, constraint solving, etc.) for multi-threaded programs. Suppose that we are given a correctness proof for a trace of a program (or for some other program fragment). We observe that the proof can always be decomposed into a finite set of Hoare triples, and we ask what can be proved from the finite set of Hoare triples using only simple combinatorial inference rules (without access to a theorem prover and without the possibility to infer genuinely new Hoare triples)? We introduce a proof system where one proves the correctness of a multi-threaded program by showing that for each trace of the program, there exists a correctness proof in the space of proofs that are derivable from a finite set of axioms using simple combinatorial inference rules. This proof system is complete with respect to the classical proof method of establishing an inductive invariant (which uses thread quantification and control predicates). Moreover, it is possible to algorithmically check whether a given set of axioms is sufficient to prove the correctness of a multi-threaded program, using ideas from well-structured transition systems.

AB - In this paper, we present a new approach to automatically verify multi-threaded programs which are executed by an unbounded number of threads running in parallel. The starting point for our work is the problem of how we can leverage existing automated verification technology for sequential programs (abstract interpretation, Craig interpolation, constraint solving, etc.) for multi-threaded programs. Suppose that we are given a correctness proof for a trace of a program (or for some other program fragment). We observe that the proof can always be decomposed into a finite set of Hoare triples, and we ask what can be proved from the finite set of Hoare triples using only simple combinatorial inference rules (without access to a theorem prover and without the possibility to infer genuinely new Hoare triples)? We introduce a proof system where one proves the correctness of a multi-threaded program by showing that for each trace of the program, there exists a correctness proof in the space of proofs that are derivable from a finite set of axioms using simple combinatorial inference rules. This proof system is complete with respect to the classical proof method of establishing an inductive invariant (which uses thread quantification and control predicates). Moreover, it is possible to algorithmically check whether a given set of axioms is sufficient to prove the correctness of a multi-threaded program, using ideas from well-structured transition systems.

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

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

U2 - 10.1145/2676726.2677012

DO - 10.1145/2676726.2677012

M3 - Conference contribution

AN - SCOPUS:84939498506

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

SP - 407

EP - 420

BT - POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

PB - Association for Computing Machinery

T2 - 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015

Y2 - 12 January 2015 through 18 January 2015

ER -