Thread modularity at many levels: a pearl in compositional verification. (English) Zbl 1380.68274
Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 473-485 (2017).
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Mart´ın Abadi and Leslie Lamport. Conjoining specifications. Transactions on Programming Languages and Systems, 17(3), 1995. 10.1145/203095.201069 |
| [2] | P. A. Abdulla, K. ˇ Cerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1-2), 2000. 10.1006/inco.1999.2843 · Zbl 1046.68567 |
| [3] | Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, and Ahmed Rezine. Constrained monotonic abstraction: A CEGAR for parameterized verification. In CONCUR, 2010. · Zbl 1287.68117 |
| [4] | Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Hol´ık. All for the price of few. In VMCAI, 2013. 10.1007/978-3-642-35873-9_28 |
| [5] | Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Hol´ık. Parameterized verification through view abstraction. STTT, 18(5), 2016. 10.1007/s10009-015-0406-x |
| [6] | Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog. Verification of Sequential and Concurrent Programs. Springer, 2009. · Zbl 1183.68361 |
| [7] | Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, 2001. · Zbl 0991.68541 |
| [8] | Edward A. Ashcroft. Proving assertions about parallel programs. J. Comput. Syst. Sci., 10(1), 1975. 10.1016/S0022-0000(75)80018-3 · Zbl 0299.68013 |
| [9] | Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Boolean and cartesian abstraction for model checking C programs. STTT, 5(1), 2003. 10.1007/s10009-002-0095-0 · Zbl 0978.68540 |
| [10] | Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, and Shmuel Sagiv. Thread quantification for concurrent shape analysis. In CAV, 2008. 10.1007/978-3-540-70545-1_37 · Zbl 1155.68360 |
| [11] | Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, and Shmuel Sagiv. Thread quantification for concurrent shape analysis. In CAV, 2008. 10.1007/978-3-540-70545-1_37 · Zbl 1155.68360 |
| [12] | David L. Black. Personal communication., 2016. |
| [13] | David L. Black, Richard F. Rashid, David B. Golub, Charles R. Hill, and Robert V. Baron. Translation lookaside buffer consistency: A software approach. In ASPLOS-III, 1989. 10.1145/70082.68193 |
| [14] | Ariel Cohen and Kedar S. Namjoshi. Local proofs for global safety properties. Formal Methods in System Design, 34(2), 2009. 10.1007/s10703-008-0063-8 · Zbl 1135.68470 |
| [15] | Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977. 10.1145/512950.512973 · Zbl 1149.68389 |
| [16] | Patrick Cousot and Radhia Cousot. Reasoning about program invariance proof methods. Res. rep. CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980. · Zbl 1051.68624 |
| [17] | Patrick Cousot and Radhia Cousot. Invariance proof methods and analysis techniques for parallel programs. In Automatic program construction techniques. Macmillan, 1984. · Zbl 0586.68019 |
| [18] | Alastair Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In CAV, volume 6806, 2011. |
| [19] | Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods in System Design, 41(1), 2012. 10.1007/s10703-012-0155-3 · Zbl 1284.68179 |
| [20] | Klaus Dräger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. SLAB: A certifying model checker for infinite-state concurrent systems. In TACAS, 2010. |
| [21] | Michael Emmi, Rupak Majumdar, and Roman Manevich. Parameterized verification of transactional memories. In PLDI, 2010. 10.1145/1806596.1806613 |
| [22] | Azadeh Farzan and Zachary Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In POPL, 2012. 10.1145/2103656.2103693 · Zbl 1321.68192 |
| [23] | Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Inductive data flow graphs. In POPL, 2013. 10.1145/2429069.2429086 · Zbl 1301.68178 |
| [24] | Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proofs that count. In POPL, 2014. 10.1145/2535838.2535885 · Zbl 1284.68395 |
| [25] | Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proof spaces for unbounded parallelism. In POPL, 2015. 10.1145/2676726.2677012 · Zbl 1345.68102 |
| [26] | Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proving liveness of parameterized programs. In LICS, 2016. 10.1145/2933575.2935310 · Zbl 1401.68038 |
| [27] | Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer. Threadmodular verification for shared-memory programs. In ESOP, 2002. · Zbl 1077.68606 |
| [28] | Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, and Sanjit A. Seshia. Modular verification of multithreaded programs. Theoretical Computer Science, 338(1-3), 2005. 10.1016/j.tcs.2004.12.006 · Zbl 1108.68080 |
| [29] | Silvio Ghilardi and Silvio Ranise. Backward reachability of arraybased systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010. · Zbl 1213.68379 |
| [30] | Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, 2012. 10.1145/2254064.2254112 |
| [31] | Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. In CAV, 2011. · Zbl 1284.68427 |
| [32] | Arie Gurfinkel, Sharon Shoham, and Yuri Meshman. SMT-based verification of parameterized systems. In FSE, 2016. 10.1145/2950290.2950330 |
| [33] | Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In PLDI, 2004. 10.1145/996841.996844 |
| [34] | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In CAV, 2003. · Zbl 1278.68175 |
| [35] | Hossein Hojjat, Philipp Rümmer, Pavle Subotic, and Wang Yi. Horn clauses for communicating timed systems. In Workshop on Horn Clauses for Verification and Synthesis, 2014. |
| [36] | Joxan Jaffar and Andrew E. Santosa. Recursive abstractions for parameterized systems. In FM, 2009. 10.1007/978-3-642-05089-3_6 · Zbl 1165.68334 |
| [37] | Cliff B. Jones. Tentative steps toward a development method for interfering programs. Transactions on Programming Languages and Systems, 5(4), 1983. 10.1145/69575.69577 · Zbl 0517.68032 |
| [38] | Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Lost in abstraction: Monotonicity in multi-threaded programs. In CONCUR, 2014. |
| [39] | Shuvendu K. Lahiri, Alexander Malkis, and Shaz Qadeer. Abstract threads. In VMCAI, 2010. 10.1007/978-3-642-11319-2_18 · Zbl 1273.68087 |
| [40] | Leslie Lamport. Proving the correctness of multiprocess programs. Transactions on Software Engineering, 3(2), 1977. 10.1109/TSE.1977.229904 · Zbl 0349.68006 |
| [41] | R. Lipton. The reachability problem is exponential-space hard. Technical Report 62, Department of Computer Science, Yale University, 1976. |
| [42] | Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular verification is Cartesian abstract interpretation. In ICTAC, 2006. 10.1007/11921240_13 · Zbl 1168.68423 |
| [43] | Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Precise thread-modular verification. In SAS, 2007. · Zbl 1211.68095 |
| [44] | David Monniaux and Laure Gonnord. Cell morphing: From array programs to array-free horn clauses. In SAS, 2016. |
| [45] | Kedar S. Namjoshi. Symmetry and completeness in the analysis of parameterized systems. In VMCAI, 2007. · Zbl 1132.68476 |
| [46] | Leonor Prensa Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In IPDPS, 2001. |
| [47] | Susan S. Owicki. Axiomatic proof techniques for parallel programs. PhD thesis, Cornell University, 1975. · Zbl 0395.68015 |
| [48] | Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, 2001. · Zbl 0978.68539 |
| [49] | Hartley Rogers, Jr. Theory of recursive functions and effective computability. MIT Press, 1987. |
| [50] | Alejandro Sánchez and César Sánchez. Parametrized invariance for infinite state processes. Acta Inf., 52(6), 2015. 10.1007/s00236-015-0222-5 · Zbl 1329.68171 |
| [51] | Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, and Bor-Yuh Evan Chang. Invariant generation for parametrized systems using self-reflection. In SAS, 2012. |
| [52] | Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv. Abstract transformers for thread correlation analysis. In APLAS, 2009. 10.1007/978-3-642-10672-9_5 |
| [53] | Natarajan Shankar. Combining theorem proving and model checking through symbolic analysis. In CONCUR, 2000. · Zbl 0999.68523 |
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.
