ABSTRACT
We show how a test suite for a sequential program can be profitably used to construct a termination proof. In particular, we describe an algorithm TpT for proving termination of a program based on information derived from testing it. TpT iteratively calls two phases: (a) an infer phase, and (b) a validate phase. In the infer phase, machine learning, in particular, linear regression is used to efficiently compute a candidate loop bound for every loop in the program. These loop bounds are verified for correctness by an off-the-shelf checker. If a loop bound is invalid, then the safety checker provides a test or a counterexample that is used to generate more data which is subsequently used by the next infer phase to compute better estimates for loop bounds. On the other hand, if all loop bounds are valid, then we have a proof of termination. We also describe a simple extension to our approach that allows us to infer polynomial loop bounds automatically. We have evaluated TpT on two benchmark sets, micro-benchmarks obtained from recent literature on program termination, and Windows device drivers. Our results are promising -- on the micro-benchmarks, we show that TpT is able to prove termination on 15% more benchmarks than any previously known technique, and our evaluation on Windows device drivers demonstrates TpT's ability to analyze and scale to real world applications.
- D. Babic, A. J. Hu, Z. Rakamaric, and B. Cook. Proving termination by divergence. In Software Engineering and Formal Methods (SEFM), pages 93–102, 2007. Google ScholarDigital Library
- M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO), pages 364–387, 2005. Google ScholarDigital Library
- N. E. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons. Proofs from tests. In International Symposium on Software Testing and Analysis (ISSTA), pages 3–14, 2008. Google ScholarDigital Library
- J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O’Hearn. Variance analyses from invariance analyses. In Principles of Programming Languages (POPL), pages 211–224, 2007. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In Computer Aided Verification (CAV), pages 491–504, 2005. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In International Colloquium on Automata, Logic and Programming (ICALP), pages 1349–1361, 2005. Google ScholarDigital Library
- A. Chawdhary, B. Cook, S. Gulwani, M. Sagiv, and H. Yang. Ranking abstractions. In European Symposium on Programming (ESOP), pages 148–162, 2008. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification (CAV), pages 154–169, 2000. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In Programming Language Design and Implementation (PLDI), pages 415–426, 2006. Google ScholarDigital Library
- P. Cousot. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In Verification, Model Checking and Abstract Interpretation (VMCAI), pages 1–24, 2005. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Principles of Programming Languages (POPL), pages 269–282, 1979. Google ScholarDigital Library
- V. Dallmeier, N. Knopp, C. Mallon, G. Fraser, S. Hack, and A. Zeller. Automatically generating test cases for specification mining. IEEE Transactions on Software Engineering, 38(2):243–257, 2012. Google ScholarDigital Library
- M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 69(1-3):35–45, 2007. Google ScholarDigital Library
- S. Goldsmith, A. Aiken, and D. S. Wilkerson. Measuring empirical computational complexity. In Foundations of Software Engineering (FSE), pages 395–404, 2007. Google ScholarDigital Library
- B. S. Gulavani and S. Gulwani. A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In Computer Aided Verification (CAV), pages 370–384, 2008. Google ScholarDigital Library
- B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. Synergy: a new algorithm for property checking. In Foundations of Software Engineering (FSE), pages 117–127, 2006. Google ScholarDigital Library
- S. Gulwani, S. Jain, and E. Koskinen. Control-flow refinement and progress invariants for bound analysis. In Programming Languages Design and Implementation (PLDI), pages 375–385, 2009. Google ScholarDigital Library
- S. Gulwani, K. K. Mehra, and T. M. Chilimbi. Speed: precise and efficient static estimation of program computational complexity. In Principles of Programming Languages (POPL), pages 127–139, 2009. Google ScholarDigital Library
- S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint solving. In Programming Language Design and Implementation (PLDI), pages 281–292, 2008. Google ScholarDigital Library
- A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu. Proving non-termination. In Principles of Programming Languages (POPL), pages 147–158, 2008. Google ScholarDigital Library
- A. Gupta, R. Majumdar, and A. Rybalchenko. From tests to proofs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 262–276, 2009. Google ScholarDigital Library
- W. R. Harris, A. Lal, A. V. Nori, and S. K. Rajamani. Alternation for termination. In Static Analysis Symposium (SAS), pages 304–319, 2010. Google ScholarDigital Library
- L. Huang, J. Jia, B. Yu, B.-G. Chun, P. Maniatis, and M. Naik. Predicting execution time of computer programs using sparse polynomial regression. In Neural Information Processing Systems (NIPS), pages 883–891, 2010.Google Scholar
- A. Komuravelli, C. S. Pasareanu, and E. M. Clarke. Learning probabilistic systems from tree samples. In Logic in Computer Science (LICS), pages 441–450, 2012. Google ScholarDigital Library
- D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination analysis with compositional transition invariants. In Computer Aided Verification (CAV), pages 89–103, 2010. Google ScholarDigital Library
- W. Lee, B.-Y. Wang, and K. Yi. Termination analysis with algorithmic learning. In Computer Aided Verification (CAV), pages 88–104, 2012. Google ScholarDigital Library
- T. M. Mitchell. Machine learning. McGraw-Hill, 1997. Google ScholarDigital Library
- T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. Using dynamic analysis to discover polynomial and array invariants. In International Conference on Software Engineering (ICSE), 2012. Google ScholarDigital Library
- C. H. Papadimitriou and K. Steiglitz. Combinatorial optimization: algorithms and complexity. Prentice-Hall, Inc., 1982. Google ScholarDigital Library
- C. S. Pasareanu and M. G. Bobaru. Learning techniques for software verification and validation. In International Symposium on Leaveraging Applications of Formal Methods, Verification and Validation (ISoLA), pages 505–507, 2012. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking and Abstract Interpretation (VMCAI), pages 239–251, 2004.Google ScholarCross Ref
- A. Podelski and A. Rybalchenko. Transition invariants. In Logic in Computer Science (LICS), pages 32–41, 2004. Google ScholarDigital Library
- C. P. Robert and G. Casella. Monte Carlo Statistical Methods (Springer Texts in Statistics). Springer-Verlag New York, Inc., 2005. Google ScholarDigital Library
- R. Sharma, I. Dillig, T. Dillig, and A. Aiken. Simplifying loop invariant generation using splitter predicates. In Computer Aided Verification (CAV), pages 703–719, 2011. Google ScholarDigital Library
- R. Sharma, S. Gupta, B. Hariharan, A. Aiken, P. Liang, and A. V. Nori. A data driven approach for algebraic loop invariants. In European Symposium on Programming (ESOP), pages 574–592, 2013. Google ScholarDigital Library
- R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V. Nori. Program verification as learning geometric concepts. In Static Analysis Symposium (SAS), 2013.Google ScholarCross Ref
- R. Sharma, A. Nori, and A. Aiken. Interpolants as classifiers. In Computer Aided Verification (CAV), pages 71–87, 2012. Google ScholarDigital Library
- O. Shkaravska, R. Kersten, and M. C. J. D. van Eekelen. Test-based inference of polynomial loop-bound functions. In Principles and Practice of Programming in Java (PPPJ), pages 99–108, 2010. Google ScholarDigital Library
- A. Tsitovich, N. Sharygina, C. M. Wintersteiger, and D. Kroening. Loop summarization and termination analysis. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 81–95, 2011. Google ScholarDigital Library
- D. Zaparanuks and M. Hauswirth. Algorithmic profiling. In Programming Language Design and Implementation (PLDI), pages 67–76, 2012. Google ScholarDigital Library
Index Terms
- Termination proofs from tests
Recommendations
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Special issue on POPL 2005Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Comments