Yu-Fang Chen
Ondřej Lengál
ABSTRACT
In 2014, Heizmann et al. proposed a novel framework for program termination analysis. The analysis starts with a termination proof of a sample path. The path is generalized to a Büchi automaton (BA) whose language (by construction) represents a set of terminating paths. All these paths can be safely removed from the program. The removal of paths is done using automata difference, implemented via BA complementation and intersection. The analysis constructs in this way a set of BAs that jointly "cover" the behavior of the program, thus proving its termination. An implementation of the approach in Ultimate Automizer won the 1st place in the Termination category of SV-COMP 2017.
In this paper, we exploit advanced automata-based algorithms and propose several non-trivial improvements of the framework. To alleviate the complementation computation for BAs---one of the most expensive operations in the framework---, we propose a multi-stage generalization construction. We start with generalizations producing subclasses of BAs (such as deterministic BAs) for which efficient complementation algorithms are known, and proceed to more general classes only if necessary. Particularly, we focus on the quite expressive subclass of semideterministic BAs and provide an improved complementation algorithm for this class. Our experimental evaluation shows that the proposed approach significantly improves the power of termination checking within the Ultimate Automizer framework.
Supplemental Material
- Software Verification Competition (SV-Comp) Benchmarks. https://github.com/sosy-lab/sv-benchmarks. Accessed: 2017-11-01.Google Scholar
- Parosh Aziz Abdulla, Yu-Fang Chen, Luká? Holík, Richard Mayr, and Tomá? Vojnar. 2010. When Simulation Meets Antichains: On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata. In Proceedings of 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10). Springer-Verlag, Berlin, Heidelberg, 158-174.Google Scholar
- Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press. Google ScholarDigital Library
- Amir M. Ben-Amram. 2010. Size-Change Termination, Monotonicity Constraints and Ranking Functions. Logical Methods in Computer Science 6, 3 (2010). http://arxiv.org/abs/1005.0253Google Scholar
- Amir M. Ben-Amram. 2011. Monotonicity Constraints for Termination in the Integer Domain. Logical Methods in Computer Science 7, 3 (2011).Google Scholar
- Amir M. Ben-Amram and Samir Genaim. 2013. On the Linear Ranking Problem for Integer Linear-Constraint Loops. In Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13). ACM, New York, NY, USA, 51-62. Google ScholarDigital Library
- Amir M. Ben-Amram and Samir Genaim. 2014. Ranking Functions for Linear-Constraint Loops. J. ACM 61, 4 (2014), 26:1-26:55. Google ScholarDigital Library
- Amir M. Ben-Amram and Samir Genaim. 2015. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In Proceedings of 27th International Conference on Computer Aided Verification (CAV'15), Vol. 9207. Springer, Cham, 304-321.Google Scholar
- Amir M. Ben-Amram and Samir Genaim. 2017. On Multiphase-Linear Ranking Functions. In Proceedings of 29th International Conference on Computer Aided Verification (CAV'17), Vol. 10427. Springer, Cham, 601-620.Google Scholar
- Dirk Beyer. 2017. Software Verification with Validation of Results - (Report on SV-Comp 2017). In Proceedings of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17). Springer-Verlag New York, Inc., New York, NY, USA, 331-349. Google ScholarDigital Library
- Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Proceedings of 23rd International Conference on Computer Aided Verification (CAV'11). Springer-Verlag, Berlin, Heidelberg, 184-190. http://dl.acm.org/citation.cfm?id=2032305.2032321 Google ScholarDigital Library
- Franti?ek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, and Ming-Hsien Tsai. 2016. Complementing Semi-deterministic Büchi Automata. In Proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16). Springer Berlin Heidelberg, Berlin, Heidelberg, 770-787. Google ScholarDigital Library
- Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2017. Proving Termination Through Conditional Termination. In Proceedings of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Vol. 10205. Springer, Berlin, Heidelberg, 99-117.Google ScholarDigital Library
- Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear Ranking with Reachability. In Proceedings of 17th International Conference on Computer Aided Verification (CAV'05). Springer-Verlag, Berlin, Heidelberg, 491-504. Google ScholarDigital Library
- Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal Property Verification. In Proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), Vol. 9636. Springer, Berlin, Heidelberg, 387-393. Google ScholarDigital Library
- Byron Cook, Daniel Kroening, Philipp Rümmer, and Christoph M. Wintersteiger. 2013. Ranking function synthesis for bit-vector relations. Formal Methods in System Design 43, 1 (2013), 93-120.Google ScholarCross Ref
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination Proofs for Systems Code. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '06). ACM, New York, NY, USA, 415-426. Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving Program Termination. Commun. ACM 54, 5 (2011), 88-98. Google ScholarDigital Library
- Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. Lexicographic Termination Proving. In Proceedings of 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13). Springer-Verlag, Berlin, Heidelberg, 47-61. Google ScholarDigital Library
- Nathanaël Courant and Caterina Urban. 2017. Precise Widening Operators for Proving Termination by Abstract Interpretation. In Proceedings of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Vol. 10205. Springer, Berlin, Heidelberg, 136-152.Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 2012. An Abstract Interpretation Framework for Termination. In Proceedings of 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12). ACM, New York, NY, USA, 245-258. Google ScholarDigital Library
- Jean-Michel Couvreur. 1999. On-the-fly Verification of Linear Temporal Logic. In Proceedings of International Symposium on Formal Methods (FM'99). Springer-Verlag, London, UK, UK, 253-271. Google ScholarDigital Library
- Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. 2006. Antichains: A New Algorithm for Checking Universality of Finite Automata. In Proceedings of 18th International Conference on Computer Aided Verification (CAV'06), Vol. 4144. Springer, Berlin, Heidelberg, 17-30. Google ScholarDigital Library
- Seth Fogarty and Moshe Y. Vardi. 2012. Büchi Complementation and Size-Change Termination. Logical Methods in Computer Science 8, 1 (2012).Google Scholar
- Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke. 2009. Proving Termination of Integer Term Rewriting. In Proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA'09). Springer-Verlag, Berlin, Heidelberg, 32-47. Google ScholarDigital Library
- Andreas Gaiser and Stefan Schwoon. 2009. Comparison of Algorithms for Checking Emptiness of Büchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09), Vol. 13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. http://drops.dagstuhl.de/opus/volltexte/2009/2349Google Scholar
- Pierre Ganty and Samir Genaim. 2013. Proving Termination Starting from the End. In Proceedings of 25th International Conference on Computer Aided Verification (CAV'13), Vol. 8044. Springer-Verlag New York, Inc., New York, NY, USA, 397-412. Google ScholarDigital Library
- Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2017. Analyzing Program Termination and Complexity Automatically with AProVe. J. Autom. Reasoning 58, 1 (2017), 3-31. Google ScholarDigital Library
- Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. 2006. Mechanizing and Improving Dependency Pairs. J. Autom. Reasoning 37, 3 (2006), 155-203. Google ScholarDigital Library
- Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Springer.Google ScholarDigital Library
- William R. Harris, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani. 2010. Alternation for Termination. In Proceedings of 17th International Conference on Static Analysis (SAS'10). Springer-Verlag, Berlin, Heidelberg, 304-319. http://dl.acm.org/citation.cfm?id=1882094.1882113 Google ScholarDigital Library
- Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. 2013. Linear Ranking for Linear Lasso Programs. In Proceedings of 15th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), Vol. 8172. Springer, Cham, 365-380.Google ScholarCross Ref
- Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs. In Proceedings of 26th International Conference on Computer Aided Verification (CAV'14). Springer-Verlag New York, Inc., New York, NY, USA, 797-813. Google ScholarDigital Library
- Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, and Christoph M. Wintersteiger. 2010. Termination Analysis with Compositional Transition Invariants. In Proceedings of 22nd International Conference on Computer Aided Verification (CAV'10). Springer-Verlag, Berlin, Heidelberg, 89-103. Google ScholarDigital Library
- Robert P. Kurshan. 1987. Complementing Deterministic Büchi Automata in Polynomial Time. J. Comput. Syst. Sci. 35, 1 (1987), 59-71. Google ScholarDigital Library
- Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin. 2015. Termination and Non-termination Specification Inference. In Proceedings of 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '15). ACM, New York, NY, USA, 489-498. Google ScholarDigital Library
- Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The sizechange principle for program termination. In Proceedings of 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01). ACM, New York, NY, USA, 81-92. Google ScholarDigital Library
- Wonchan Lee, Bow-Yaw Wang, and Kwangkeun Yi. 2012. Termination Analysis with Algorithmic Learning. In Proceedings of 24th International Conference on Computer Aided Verification (CAV'12). Springer-Verlag, Berlin, Heidelberg, 88-104. Google ScholarDigital Library
- Jan Leike and Matthias Heizmann. 2015. Ranking Templates for Linear Loops. Logical Methods in Computer Science 11, 1 (2015).Google Scholar
- Max Michel. 1988. Complementation is more difficult with automata on infinite words. Technical Report. CNET, Paris.Google Scholar
- Sebastian Ott. 2016. Implementing a Termination Analysis using Configurable Software Analysis. Master's Thesis, University of Passau, Software Systems Lab.Google Scholar
- Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2018. Reducing Liveness to Safety in First-Order Logic. ACM Program. Lang. 2, POPL (2018), 26:1-26:33. Google ScholarDigital Library
- Doron Peled. 1993. All from One, One for All: on Model Checking Using Representatives. In Proceedings of 5th International Conference on Computer Aided Verification (CAV'93). Springer-Verlag, London, UK, 409-423. http://dl.acm.org/citation.cfm?id=647762.735490 Google ScholarDigital Library
- Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In Proceedings of 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), Vol. 2937. Springer, Berlin, Heidelberg, 239- 251.Google ScholarCross Ref
- Andreas Podelski and Andrey Rybalchenko. 2004. Transition Invariants. In Proceedings of 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04). IEEE Computer Society,Washington, DC, USA, 32-41. Google ScholarDigital Library
- Andreas Podelski, Andrey Rybalchenko, and Thomas Wies. 2008. Heap Assumptions on Demand. In Proceedings of 20th International Conference on Computer Aided Verification (CAV'08). Springer-Verlag, Berlin, Heidelberg, 314-327. Google ScholarDigital Library
- Corneliu Popeea and Andrey Rybalchenko. 2012. Compositional Termination Proofs for Multi-threaded Programs. In Proceedings of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12). Springer-Verlag, Berlin, Heidelberg, 237-251. Google ScholarDigital Library
- Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp, and Cornelius Aschermann. 2017. Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. J. Autom. Reasoning 58, 1 (2017), 33-65. Google ScholarDigital Library
- Caterina Urban. 2013. The Abstract Domain of Segmented Ranking Functions. In Proceedings of 24th International Symposium on Static Analysis (SAS'13), Vol. 7935. Springer, Berlin, Heidelberg, 43-62.Google ScholarCross Ref
- Caterina Urban. 2015. FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution). In Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15). Springer-Verlag New York, Inc., New York, NY, USA, 464-466. Google ScholarDigital Library
- Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing Ranking Functions from Bits and Pieces. In Proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16). Springer-Verlag New York, Inc., New York, NY, USA, 54-70. Google ScholarDigital Library
- Caterina Urban and Antoine Miné. 2014. An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In Proceedings of 23rd European Symposium on Programming Languages and Systems (ESOP'14). Springer-Verlag New York, Inc., New York, NY, USA, 412-431. Google ScholarDigital Library
- Caterina Urban and Antoine Miné. 2014. A Decision Tree Abstract Domain for Proving Conditional Termination. In Proceedings of 21st International Symposium on Static Analysis (SAS'14), Vol. 8723. Springer, Cham, 302-318.Google ScholarCross Ref
- Antti Valmari. 1991. Stubborn Sets for Reduced State Space Generation. In Proceedings of 10th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets (ICATPN'89). Springer, 491-515. Google ScholarDigital Library
Index Terms
- Advanced automata-based algorithms for program termination checking
Recommendations
Advanced automata-based algorithms for program termination checking
PLDI '18In 2014, Heizmann et al. proposed a novel framework for program termination analysis. The analysis starts with a termination proof of a sample path. The path is generalized to a Büchi automaton (BA) whose language (by construction) represents a set of ...
Ramsey-Based Inclusion Checking for Visibly Pushdown Automata
Checking whether one formal language is included in another is important in many verification tasks. In this article, we provide solutions for checking the inclusion of languages given by visibly pushdown automata over both finite and infinite words. ...
Advanced automata minimization
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present an efficient algorithm to reduce the size of nondeterministic Buchi word automata, while retaining their language. Additionally, we describe methods to solve PSPACE-complete automata problems like universality, equivalence and inclusion for ...
Comments