Marc Brockschmidt
Jürgen Giesl
Skip Abstract Section
Abstract
We present a modular approach to automatic complexity analysis of integer programs. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer bounds on the absolute values of program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. The bounds computed by our method are polynomial or exponential expressions that depend on the absolute values of input parameters.
We show how to extend our approach to arbitrary cost measures, allowing the use of our technique to find upper bounds for other expended resources, such as network requests or memory consumption. Our contributions are implemented in the open-source tool KoAT, and extensive experiments show the performance and power of our implementation in comparison with other tools.
- Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, Germán Puebla, and Damiano Zanardini. 2008. Termination analysis of Java bytecode. In Proceedings of the 2008 FMOODS Conference (FMOODS’08). 2--18. Google Scholar
Digital Library
- Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. 2011a. Closed-form upper bounds in static cost analysis. Journal of Automated Reasoning 46, 2, 161--203. Google ScholarDigital Library
- Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. 2012. Cost analysis of object-oriented bytecode programs. Theoretical Computer Science 413, 1, 142--159. Google ScholarDigital Library
- Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez. 2011b. Verified resource guarantees using COSTA and KeY. In Proceedings of the 2011 PEPM Conference (PEPM’11). 73--76. Google ScholarDigital Library
- Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of the 2010 SAS Conference (SAS’10). 117--133. Google ScholarDigital Library
- Diego Esteban Alonso-Blas, Puri Arenas, and Samir Genaim. 2013. Precise cost analysis via local reasoning. In Proceedings of the 2013 ATVA Conference (ATVA’13). 319--333.Google ScholarCross Ref
- Martin Avanzini and Georg Moser. 2013. A combination framework for complexity. In Proceedings of the 2013 RTA Conference (RTA’13). 55--70.Google Scholar
- Roberto Bagnara, Fred Mesnard, Andrea Pescetti, and Enea Zaffanella. 2012. A new look at the automatic synthesis of linear ranking functions. Information and Computation 215, 47--67. Google ScholarDigital Library
- Amir M. Ben-Amram and Samir Genaim. 2013. On the linear ranking problem for integer linear-constraint loops. In Proceedings of the 2013 POPL Conference (POPL’13). 51--62. Google ScholarDigital Library
- Amir M. Ben-Amram, Neil D. Jones, and Lars Kristiansen. 2008. Linear, polynomial or exponential? Complexity inference in polynomial time. In Proceedings of the 2008 CiE Conference (CiE’08). 67--76. Google ScholarDigital Library
- Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko, and Valerio Senni (Eds.). 2014. Proceedings: First Workshop on Horn Clauses for Verification and Synthesis. EPTCS 169. Vienna, Austria.Google Scholar
- Régis Blanc, Thomas A. Henzinger, Thibaud Hottelier, and Laura Kovács. 2010. ABC: Algebraic bound computation for loops. In Proceedings of the 2010 LPAR Conference (LPAR’10). 103--118. Google ScholarDigital Library
- Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear ranking with reachability. In Proceedings of the 2005 CAV Conference (CAV’05). 491--504. Google ScholarDigital Library
- Marc Brockschmidt, Byron Cook, and Carsten Fuhs. 2013. Better termination proving through cooperation. In Proceedings of the 2013 CAV Conference (CAV’13). 413--429.Google ScholarCross Ref
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl. 2014. Alternating runtime and size complexity analysis of integer programs. In Proceedings of the 2014 TACAS Conference (TACAS’14). 140--155.Google ScholarCross Ref
- Marc Brockschmidt, Richard Musiol, Carsten Otto, and Jürgen Giesl. 2012. Automated termination proofs for Java programs with cyclic data. In Proceedings of the 2012 CAV Conference (CAV’12). 105--122. Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In Proceedings of the 2006 PLDI Conference (PLDI’06). 415--426. Google ScholarDigital Library
- Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In Proceedings of the 2013 TACAS Conference (TACAS’13). 47--61. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 1977 POPL Conference (POPL’77). 238--252. Google ScholarDigital Library
- Saumya Debray and Nai-Wei Lin. 1993. Cost analysis of logic programs. ACM Transactions on Programming Languages and Systems 15, 826--875. Google ScholarDigital Library
- Saumya Debray, Pedro López-García, Manuel V. Hermenegildo, and Nai-Wei Lin. 1997. Lower bound cost estimation for logic programs. In Proceedings of the 1997 ILPS Conference (ILPS’97). 291--305. Google ScholarDigital Library
- Stephan Falke, Deepak Kapur, and Carsten Sinz. 2011. Termination analysis of C programs using compiler intermediate languages. In Proceedings of the 2011 RTA Conference (RTA’11). 41--50.Google Scholar
- Antonio Flores-Montoya and Reiner Hähnle. 2014. Resource analysis of complex programs with cost equations. In Proceedings of the 2014 APLAS Conference (APLAS’14). 275--295.Google ScholarCross Ref
- Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl. 2007. SAT solving for termination analysis with polynomial interpretations. In Proceedings of the 2007 SAT Conference (SAT’07). 340--354. Google ScholarDigital Library
- Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke. 2009. Proving termination of integer term rewriting. In Proceedings of the 2009 RTA Conference (RTA’09). 32--47. Google ScholarDigital Library
- Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2014. Proving termination of programs automatically with AProVE. In Proceedings of the 2014 IJCAR Conference (IJCAR’14). 184--191.Google ScholarCross Ref
- Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes, and Carsten Fuhs. 2012. Symbolic evaluation graphs and term rewriting: A general methodology for analyzing logic programs. In Proceedings of the 2012 PPDP Conference (PPDP’12). 1--12. Google ScholarDigital Library
- Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. 2006. Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37, 3, 155--203. Google ScholarDigital Library
- Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. 2012. Synthesizing software verifiers from proof rules. In Proceedings of the 2012 PLDI Conference (PLDI’12). 405--416. Google ScholarDigital Library
- Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: Precise and efficient static estimation of program computational complexity. In Proceedings of the 2009 POPL Conference (POPL’09). 127--139. Google ScholarDigital Library
- William R. Harris, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani. 2010. Alternation for termination. In Proceedings of the 2010 SAS Conference (SAS’10). 304--319. Google ScholarDigital Library
- Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination analysis by learning terminating programs. In Proceedings of the 2014 CAV Conference (CAV’14). 797--813. Google ScholarDigital Library
- Manuel V. Hermenegildo, Francisco Bueno, Manuel Carro, Pedro López-García, Edison Mera, José F. Morales, and Germán Puebla. 2012. An overview of Ciao and its design philosophy. Theory and Practice of Logic Programming 12, 1--2, 219--252. Google ScholarDigital Library
- Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Multivariate amortized resource analysis. ACM Transactions on Programming Languages and Systems 34, 3, Article No. 14. Google ScholarDigital Library
- Jan Hoffmann and Zhong Shao. 2014. Type-based amortized resource analysis with integers and arrays. In Proceedings of the 2014 FLOPS Conference (FLOPS’14). 152--168.Google ScholarCross Ref
- Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, and Philipp Rümmer. 2012. A verification toolkit for numerical transition systems—tool paper. In Proceedings of the 2012 FM Conference (FM’12). 247--251.Google Scholar
- Bertrand Jeannet and Antoine Miné. 2009. Apron: A library of numerical abstract domains for static analysis. In Proceedings of the 2009 CAV Conference (CAV’09). 661--667. Google ScholarDigital Library
- Jens Knoop, Laura Kovács, and Jakob Zwirchmayr. 2012. r-TuBound: Loop bounds for WCET analysis. In Proceedings of the 2012 LPAR Conference (LPAR’12). 435--444. Google ScholarDigital Library
- Dallas Lankford. 1979. On Proving Term Rewriting Systems are Noetherian. Technical Report MTP-3. Louisiana Technical University, Ruston, LA.Google Scholar
- Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2013. Proving termination of imperative programs using Max-SMT. In Proceedings of the 2013 FMCAD Conference (FMCAD’13). 218--225.Google ScholarCross Ref
- Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In Proceedings of the 2001 POPL Conference (POPL’01). 81--92. Google ScholarDigital Library
- Jan Leike and Matthias Heizmann. 2014. Ranking templates for linear loops. In Proceedings of the 2014 TACAS Conference (TACAS’14). 172--186.Google ScholarCross Ref
- Stephen Magill, Ming-Hsien Tsai, Peter Lee, and Yih-Kuen Tsay. 2010. Automatic numeric abstractions for heap-manipulating programs. In Proceedings of the 2010 POPL Conference (POPL’10). 211--222. Google ScholarDigital Library
- Antoine Miné. 2006. The octagon abstract domain. Higher-Order and Symbolic Computation 19, 1, 31--100. Google ScholarDigital Library
- Leonardo M. de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the 2008 TACAS Conference (TACAS’08). 337--340. Google ScholarDigital Library
- Jorge A. Navas, Edison Mera, Pedro López-García, and Manuel V. Hermenegildo. 2007. User-definable resource bounds analysis for logic programs. In Proceedings of the 2007 ICLP Conference (ICLP’07). 348--363. Google ScholarDigital Library
- Lars Noschinski, Fabian Emmes, and Jürgen Giesl. 2013. Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning 51, 1, 27--56.Google ScholarCross Ref
- Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In Proceedings of the 2004 VMCAI Conference (VMCAI’04). 239--251.Google ScholarCross Ref
- Alejandro Serrano, Pedro López-García, and Manuel V. Hermenegildo. 2014. Resource usage analysis of logic programs via abstract interpretation using sized types. Theory and Practice of Logic Programming 14, 4--5, 739--754.Google ScholarCross Ref
- Moritz Sinn, Florian Zuleger, and Helmut Veith. 2014. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proceedings of the 2014 CAV Conference (CAV’14). 745--761. Google ScholarDigital Library
- Fausto Spoto, Fred Mesnard, and Étienne Payet. 2010. A termination analyser for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems 32, 3, Article No. 8. Google ScholarDigital Library
- Aliaksei Tsitovich, Natasha Sharygina, Christoph M. Wintersteiger, and Daniel Kroening. 2011. Loop summarization and termination analysis. In Proceedings of the 2011 TACAS Conference (TACAS’11). 81--95. Google ScholarDigital Library
- Tao Wei, Jian Mao, Wei Zou, and Yu Chen. 2007. A new algorithm for identifying loops in decompilation. In Proceedings of the 2007 SAS Conference (SAS’07). 170--183. Google ScholarDigital Library
- Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, et al. 2008. The worst-case execution-time problem: Overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems 7, 3, Article No. 36. Google ScholarDigital Library
- Florian Zuleger, Sumit Gulwani, Moritz Sinn, and Helmut Veith. 2011. Bound analysis of imperative programs with the size-change abstraction. In Proceedings of the 2011 SAS Conference (SAS’11). 280--297. Google ScholarDigital Library
Index Terms
- Analyzing Runtime and Size Complexity of Integer Programs
Recommendations
Inferring Lower Runtime Bounds for Integer Programs
We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program ...
One-Way Communication Complexity and the Nečiporuk Lower Bound on Formula Size
In this paper the Nečiporuk method for proving lower bounds on the size of Boolean formulas is reformulated in terms of one-way communication complexity. We investigate the settings of probabilistic formulas, nondeterministic formulas, and quantum ...
Comments