Predicate abstraction and refinement for verifying multi-threaded programs. (English) Zbl 1284.68427
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’11, Austin, TX, USA, January 26–28, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0490-0). 331-344 (2011).
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68M20 | Performance evaluation, queueing, and scheduling in the context of computer systems |
| 68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |
Keywords:
(transition) predicate abstraction; abstraction refinement; environment transitions; Horn clauses; modular reasoning; multi-threaded programs; proof rule; safetyReferences:
| [1] | Y. Bar-David and G. Taubenfeld. Automatic discovery of mutual exclusion algorithms. In DISC, pages 136-150, 2003. |
| [2] | G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening. Symbolic counter abstraction for concurrent software. In CAV, pages 64-78, 2009. 10.1007/978-3-642-02658-4_9 · Zbl 1242.68055 |
| [3] | G. Basler, M. Hague, D. Kroening, C.-H. L. Ong, T. Wahl, and H. Zhao. Boom: Taking boolean program model checking one step further. In TACAS, pages 145-149, 2010. 10.1007/978-3-642-12002-2_11 |
| [4] | E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, pages 154-169, 2000. · Zbl 0974.68517 |
| [5] | A. Cohen and K. S. Namjoshi. Local proofs for global safety properties. FMSD, 34 (2): 104-125, 2009. 10.1007/s10703-008-0063-8 · Zbl 1176.68118 |
| [6] | J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers, 3rd Edition. O’Reilly Media, Inc., 2005. |
| [7] | P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238-252, 1977. 10.1145/512950.512973 |
| [8] | C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL, pages 110-121, 2005. 10.1145/1040305.1040315 · Zbl 1369.68135 |
| [9] | C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, pages 213-224, 2003. · Zbl 1023.68529 |
| [10] | C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In ESOP, pages 262-277, 2002. · Zbl 1077.68606 |
| [11] | P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis, University of Liege, Computer Science Department, 1994. |
| [12] | S. Graf and H. Saıdi. Construction of abstract state graphs with PVS. In CAV, pages 72-83, 1997. |
| [13] | A. Gupta, C. Popeea, and A. Rybalchenko. Non-monotonic refinement of control abstraction for concurrent programs. In phATVA, pages 188-202, 2010. · Zbl 1305.68057 |
| [14] | T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58-70, 2002. 10.1145/503272.503279 · Zbl 1323.68374 |
| [15] | T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In PLDI, pages 1-13, 2004. 10.1145/996841.996844 |
| [16] | C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5 (4): 596-619, 1983. 10.1145/69575.69577 · Zbl 0517.68032 |
| [17] | C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321-332, 1983. |
| [18] | L. Lamport. A new solution of Dijkstra’s concurrent programming problem. Commun. ACM, 17 (8): 453-455, 1974. 10.1145/361082.361093 · Zbl 0281.68004 |
| [19] | L. Lamport. A fast mutual exclusion algorithm. ACM Trans. Comput. Syst., 5 (1): 1-11, 1987. 10.1145/7351.7352 |
| [20] | S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS, pages 329-339, 2008. 10.1145/1346281.1346323 |
| [21] | A. Malkis, A. Podelski, and A. Rybalchenko. Thread-modular verification is cartesian abstract interpretation. In ICTAC, pages 183-197, 2006. 10.1007/11921240_13 · Zbl 1168.68423 |
| [22] | Z. Manna and A. Pnueli. Temporal verification of reactive systems: safety. Springer-Verlag, 1995. |
| [23] | P. McKenney. Using Promela and Spin to verify parallel algorithms. LWN.net weekly edition, 2007. |
| [24] | M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In OSDI, pages 267-280, 2008. |
| [25] | G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In CC, pages 213-228, 2002. · Zbl 1051.68756 |
| [26] | S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6: 319-340, 1976. · Zbl 0312.68011 |
| [27] | A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, infty)-counter abstraction. In CAV, pages 107-122, 2002. · Zbl 1010.68095 |
| [28] | A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. In POPL, pages 132-144, 2005. 10.1145/1040305.1040317 · Zbl 1369.68152 |
| [29] | A. Podelski and A. Rybalchenko. Armc: The logical choice for software model checking with abstraction refinement. In PADL, pages 245-259, 2007. 10.1007/978-3-540-69611-7_16 |
| [30] | S. Qadeer and D. Wu. KISS: keep it simple and sequential. In PLDI, pages 14-24, 2004. 10.1145/996841.996845 |
| [31] | A. Rybalchenko. The ARMC tool. Available from http://www7.in.tum.de/ rybal/armc/. |
| [32] | B. K. Szymanski. A simple solution to Lamport’s concurrent programming problem with linear wait. In ICS, pages 621-626, 1988. 10.1145/55364.55425 |
| [33] | The Intelligent Systems Laboratory. SICStus Prolog User’s Manual. Swedish Institute of Computer Science, 2001. Release 3.8.7. |
| [34] | C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In TACAS, pages 382-396, 2008. · Zbl 1134.68421 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
