Context-Bounded Verification of Liveness: Conclusion, Acknowledgment & References

Table of Links

• Introduction
• Dynamic Networks of Concurret Pushdown Systems (DCPS)
• Warm-up: Non-Termination
• Fair Non-Termination
• From Progressive Runs for VASSB to Reachability
• Starvation
• Conclusion, Acknowledgment & References
• A. Strengthening Fairness to Progressive Runs
• B. Proofs from Section 4.1
• C. Proofs for Section 5
• D. Proofs for Section 5.3
• E. Proofs for Section 6

7 CONCLUSION

ACKNOWLEDGMENTS

This research was sponsored in part by the Deutsche Forschungsgemeinschaft project 389792660 TRR 248–CPEC and by the European Research Council under the Grant Agreement 610150 (http://www.impact-erc.eu/) (ERC Synergy Grant ImPACT).

REFERENCES

Parosh Aziz Abdulla, Karlis Čer ¯ ans, Bengt Jonsson, and Yih-Kuen Tsay. 1996. General decidability theo ¯ rems for infinitestate systems. In Proceedings of the Eleventh Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 313–321.

Krzysztof R. Apt and Ernst-Rüdiger Olderog. 1991. Verification of Sequential and Concurrent Programs. Springer-Verlag.

Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, and Akash Lal. 2012a. Detecting Fair Non-termination in Multithreaded Programs. In Proceedings of CAV 2012. 210–226. https://doi.org/10.1007/978-3-642-31424-7_19

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. 2012b. Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. In Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings (Lecture Notes in Computer Science), Vol. 7561. Springer, 152–166.

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. 2017. Parity Games on Bounded Phase Multi-pushdown Systems. In Networked Systems - 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings (Lecture Notes in Computer Science), Vol. 10299. Springer, 272–287.

Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2009. Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In Proceedings of TACAS 2009. 107–123.

Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2011. Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads. Log. Methods Comput. Sci. 7, 4 (2011). https://doi.org/10.2168/LMCS-7(4:4)2011

Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund. 2015. Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity. In 9th International Conference on Language and Automata Theory and Applications, LATA 2015, Nice, France, March 2-6, 2015, Proceedings. Springer, 473–485.

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2020. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference) (LIPIcs), Vol. 168. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 111:1–111:16.

Julius Richard Büchi. 1964. Regular canonical systems. Archiv für mathematische Logik und Grundlagenforschung 6, 3-4 (1964), 91–111.

Heino Carstensen. 1987. Decidability questions for fairness in Petri nets. In Proceedings of STACS 1987. Springer, 396–407.

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2007. Proving thread termination. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007. ACM, 320–330.

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination. Commun. ACM 54, 5 (2011), 88–98. https://doi.org/10.1145/1941487.1941509

Bruno Courcelle. 1991. On construction obstruction sets of words. EATCS 44 (1991), 178–185.

Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. 2019. The reachability problem for Petri nets is not elementary. In Proceedings of STOC 2019. 24–33.

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. 2017. Model checking parameterized asynchronous shared-memory systems. Formal Methods Syst. Des. 50, 2-3 (2017), 140–167. https://doi.org/10.1007/s10703-016-0258-3

Paul Erdős and Richard Rado. 1952. Combinatorial Theorems on Classifications of Subsets of a Given Set. Proceedings of the London Mathematical Society s3-2, 1 (01 1952), 417–439. https://doi.org/10.1112/plms/s3-2.1.417

Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2016. Proving Liveness of Parameterized Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. ACM, 185–196.

Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 1-2 (2001), 63–92.

Marie Fortin, Anca Muscholl, and Igor Walukiewicz. 2017. Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Vol. 10427. Springer, 155– 175.

Pierre Ganty and Rupak Majumdar. 2012. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 34, 1 (2012), 6.

Leonard H Haines. 1969. On free monoids partially ordered by embedding. Journal of Combinatorial Theory 6, 1 (1969), 94–98.

David Harel. 1986. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM 33 (1986), 224–248.

Rodney R Howell, Louis E Rosier, and Hsu-Chun Yen. 1991. A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science 82, 2 (1991), 341–372.

Petr Jančar. 1990. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science 74, 1 (1990), 71–93.

Vineet Kahlon. 2008. Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs. IEEE Computer Society, 181–192.

Sambasiva Rao Kosaraju. 1982. Decidability of Reachability in Vector Addition Systems (Preliminary Version). In STOC ’82: Proc. of 14th ACM symp. on Theory of Computing. ACM, 267–281.

Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. 2020. Inductive sequentialization of asynchronous programs. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020. ACM, 227–242.

Akash Lal and Thomas W. Reps. 2009. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design 35, 1 (2009), 73–97. https://doi.org/10.1007/s10703-009-0078-9

Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas W. Reps. 2008. Interprocedural Analysis of Concurrent Programs Under a Context Bound. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science), Vol. 4963. Springer, 282–298.

Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. 2015. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP 2015, Vol. 9135. 324–336. https://doi.org/10.1007/978-3-662-47666-6_26

Irina A. Lomazova and Philippe Schnoebelen. 1999. Some Decidability Results for Nested Petri Nets. In Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI’99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999, Proceedings (Lecture Notes in Computer Science), Vol. 1755. Springer, 208–220.

Ernst W. Mayr. 1981. An Algorithm for the General Petri Net Reachability Problem. In Proceedings of STOC 1981. 238–246.

Anca Muscholl, Helmut Seidl, and Igor Walukiewicz. 2017. Reachability for Dynamic Parametric Processes. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings (Lecture Notes in Computer Science), Vol. 10145. Springer, 424–441.

Madanlal Musuvathi and Shaz Qadeer. 2007. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, PLDI 2007, San Diego, CA, USA, June 10-13, 2007. ACM, 446–455.

Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2018. Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2, POPL (2018), 26:1–26:33.

Rohit J. Parikh. 1966. On Context-Free Languages. J. ACM 13, 4 (1966), 570–581.

Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings (Lecture Notes in Computer Science), Vol. 3440. Springer, 93–107.

Charles Rackoff. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 2 (1978), 223–231.

Ganesan Ramalingam. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS 22(2) (2000), 416–430.

Frank Plumpton Ramsey. 1930. On a Problem of Formal Logic. Proceedings of the London Mathematical Society s2-30, 1 (1930), 264–286. https://doi.org/10.1112/plms/s2-30.1.264

Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. 2016. Scope-Bounded Pushdown Languages. Int. J. Found. Comput. Sci. 27, 2 (2016), 215–234. https://doi.org/10.1142/S0129054116400074

Moshe Y. Vardi. 1991. Verification of concurrent programs—the automata-theoretic framework. Annals of Pure and Applied Logic 51 (1991), 79–98.

Kumar Neeraj Verma and Jean Goubault-Larrecq. 2005. Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science Vol. 7 (2005).

Georg Zetzsche. 2013. Silent Transitions in Automata with Storage. (2013). arXiv:1302.3798 Full version of an article in Proceedings of ICALP 2013.