Azadeh Farzan
Andreas Podelski
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.
Supplemental Material
- P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parameterized system verification. In CAV, pages 134--145, 1999. Google Scholar
Digital Library
- P. A. Abdulla, Y.-F. Chen, G. Delzanno, F. Haziza, C.-D. Hong, and A. Rezine. Constrained monotonic abstraction: a cegar for parameterized verification. In CONCUR, pages 86--101, 2010. Google ScholarDigital Library
- P. A. Abdulla, F. Haziza, and L. Holík. All for the price of few. In VMCAI, pages 476--495, 2013.Google ScholarDigital Library
- K. R. Apt and D. Kozen. Limits for automatic verification of finitestate concurrent systems. Inf. Process. Lett., 22(6):307--309, 1986. Google ScholarDigital Library
- T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, pages 221--234, 2001. Google ScholarDigital Library
- T. Ball, S. Chaki, and S. K. Rajamani. Parameterized verification of multithreaded software libraries. In TACAS, pages 158--173, 2001. Google ScholarDigital Library
- S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf., 10(5): 401--424, Sept. 2008. Google ScholarDigital Library
- K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S systems to verify parameterized networks. In TACAS, pages 188--203, 2000. Google ScholarDigital Library
- K. Baukus, K. Stahl, S. Bensalem, and Y. Lakhnech. Networks of processes with parameterized state space. Electr. Notes Theor. Comput. Sci., 50(4):386--400, 2001.Google ScholarCross Ref
- J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and M. Sagiv. Thread quantification for concurrent shape analysis. In CAV, pages 399--413, 2008. Google ScholarDigital Library
- A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV, pages 403--418, 2000. Google ScholarDigital Library
- A. R. Bradley. Sat-based model checking without unrolling. In VMCAI, pages 70--87, 2011. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and M. C. Browne. Reasoning about networks with many identical finite-state processes. In PODC, pages 240--248, 1986. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and S. Jha. Veryfying parameterized networks using abstraction and regular languages. In CONCUR, pages 395--407, 1995. Google ScholarDigital Library
- M. A. Colón, S. Sankaranarayanan, and H. B. Sipma. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification, pages 420--432, 2003.Google ScholarCross Ref
- G. Delzanno, J.-F. Raskin, and L. V. Begin. Towards the automated verification of multithreaded java programs. In TACAS, pages 173--187, 2002. Google ScholarDigital Library
- T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. In POPL, pages 2--15, 2009. Google ScholarDigital Library
- A. Farzan and Z. Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In POPL, pages 297--308, 2012. Google ScholarDigital Library
- A. Farzan, Z. Kincaid, and A. Podelski. Inductive data flow graphs. In POPL, pages 129--142, 2013. Google ScholarDigital Library
- D. Fisman and A. Pnueli. Beyond regular model checking. In FSTTCS, pages 156--170, 2001. Google ScholarDigital Library
- P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. Formal Methods in System Design, 40(2):206--231, 2012. Google ScholarDigital Library
- S. M. German and A. P. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675--735, 1992. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, pages 331--344, 2011. Google ScholarDigital Library
- M. Hack. Decidability questions for Petri nets. PhD thesis, MIT, June 1976.Google Scholar
- M. Heizmann, J. Hoenicke, and A. Podelski. Refinement of trace abstraction. In SAS, pages 69--85, 2009. Google ScholarDigital Library
- L. E. Holloway, B. H. Krogh, and A. Giua. A survey of petri net methods for controlled discrete eventsystems. Discrete Event Dynamic Systems, 7(2):151--190, Apr. 1997. Google ScholarDigital Library
- C. N. Ip and D. L. Dill. Verifying systems with replicated components in mur'. Formal Methods in System Design, 14(3):273--310, 1999. Google ScholarDigital Library
- A. John, I. Konnov, U. Schmid, H. Veith, and J.Widder. Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In FMCAD, pages 201--209, 2013.Google ScholarCross Ref
- A. Kaiser, D. Kroening, and T. Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV, pages 645--659, 2010. Google ScholarDigital Library
- R. M. Karp and R. E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147--195, 1969. Google ScholarDigital Library
- Y. Kesten, A. Pnueli, E. Shahar, and L. D. Zuck. Network invariants in action. In CONCUR, pages 101--115, 2002. Google ScholarDigital Library
- S. R. Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC, pages 267--281, 1982. Google ScholarDigital Library
- R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. Inf. Comput., 117(1):1--11, 1995. Google ScholarDigital Library
- S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV, pages 629--644, 2010. Google ScholarDigital Library
- J. Leroux. Vector addition system reachability problem: a short selfcontained proof. In POPL, pages 307--316, 2011. Google ScholarDigital Library
- D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL, pages 346--357, 1997. Google ScholarDigital Library
- B. D. Lubachevsky. An approach to automating the verification of compact parallel coordination programs i. Acta Inf., 21:125--169, 1984.Google ScholarDigital Library
- M. Maidl. A unifying model checking approach for safety properties of parameterized systems. In CAV, pages 311--323, 2001. Google ScholarDigital Library
- K. L. McMillan. Lazy abstraction with interpolants. In CAV, pages 123--136, 2006. Google ScholarDigital Library
- L. P. Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In IPDPS, page 150, 2001. Google ScholarDigital Library
- S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM, 19:279--285, May 1976. ISSN 0001-0782. Google ScholarDigital Library
- E. Pelz. Closure properties of deterministic petri nets. In STACS, pages 371--382, 1987. Google ScholarDigital Library
- A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. In CAV, pages 328--343, 2000. Google ScholarDigital Library
- A. Pnueli, S. Ruah, and L. D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, pages 82--97, 2001. Google ScholarDigital Library
- A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, 1)-counter abstraction. In CAV, pages 107--122, 2002. Google ScholarDigital Library
- S. Qadeer and D. Wu. Kiss: keep it simple and sequential. In PLDI, pages 14--24, 2004. Google ScholarDigital Library
- M. Segalov, T. Lev-Ami, R. Manevich, R. Ganesan, and M. Sagiv. Abstract transformers for thread correlation analysis. In APLAS, pages 30--46, 2009. Google ScholarDigital Library
- P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In CAV, pages 88--97, 1998. Google ScholarDigital Library
- L. Zuck and A. Pnueli. Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct., 30 (3-4):139--169, Oct. 2004. Google ScholarDigital Library
Index Terms
- Proofs that count
Recommendations
Proofs that count
POPL '14Counting 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) ...
Soter: an automatic safety verifier for erlang
AGERE! 2012: Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractionsThis paper presents Soter, a fully-automatic program analyser and verifier for Erlang modules. The fragment of Erlang accepted by Soter includes the higher-order functional constructs and all the key features of actor concurrency, namely, dynamic and ...
An integrated specification and verification technique for highly concurrent data structures
AbstractWe present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free ...
Comments