Akhilesh Srikanth
ABSTRACT
Determining if a given program satisfies a given bound on the amount of resources that it may use is a fundamental problem with critical practical applications. Conventional automatic verifiers for safety properties cannot be applied to address this problem directly because such verifiers target properties expressed in decidable theories; however, many practical bounds are expressed in nonlinear theories, which are undecidable.
In this work, we introduce an automatic verification algorithm, CAMPY, that determines if a given program P satisfies a given resource bound B, which may be expressed using polynomial, exponential, and logarithmic terms. The key technical contribution behind our verifier is an interpolating theorem prover for non-linear theories that lazily learns a sufficiently accurate approximation of non-linear theories by selectively grounding theorems of the nonlinear theory that are relevant to proving that P satisfies B. To evaluate CAMPY, we implemented it to target Java Virtual Machine bytecode. We applied CAMPY to verify that over 20 solutions submitted for programming problems hosted on popular online coding platforms satisfy or do not satisfy expected complexity bounds.
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci., 413(1), 2012. Google Scholar
Digital Library
- C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In SAS, 2010. Google ScholarDigital Library
- R. Alur and P. Madhusudan. Adding nesting structure to words. J. ACM, 56 (3), 2009. Google ScholarDigital Library
- R. Alur, R. Bodik, G. Juniwal, M. M. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In FMCAD, 2015.Google Scholar
- T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI, 2001. Google ScholarDigital Library
- C. Borralleras, S. Lucas, R. Navarro-Marset, E. Rodríguez-Carbonell, and A. Rubio. Solving non-linear polynomial arithmetic via sat modulo linear arithmetic. In CADE, 2009. Google ScholarDigital Library
- campy. campy. http://www.cc.gatech.edu/~wharris/campy.html, 2016. Accessed: 2016 Nov 6. Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao. End-to-end verification of stack-space bounds for C programs. In PLDI, 2014. Google ScholarDigital Library
- Q. Carbonneaux, J. Hoffmann, and Z. Shao. Compositional certified resource bounds. In PLDI, 2015. Google ScholarDigital Library
- codechef. Programming competition, programming contest, online computer programming. https://www.codechef.com/, 2016. Accessed: 2016 June 14. codeforces. Programming competitions and contests, programming community. https://www.codeforces.com/, 2016. Accessed: 2016 June 14. G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. Springer, 1998.Google Scholar
- cve-2011-3191. CVE - CVE-2011-3191. https://cve.mitre.org/cgibin/cvename.cgi?name=CVE-2011-3192, 2015.Google Scholar
- Accessed: 2015 July. L. Dai, B. Xia, and N. Zhan. Generating non-linear interpolants by semidefinite programming. In CAV, 2013.Google Scholar
- L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- framework. A framework for analyzing and transforming Java and Android applications. https://sable.github.io/soot/, 2016. Accessed: 2016.Google Scholar
- K. Gödel, S. C. Kleene, and J. B. Rosser. On undecidable propositions of formal mathematical systems. Institute for Advanced Study Princeton, NJ, 1934.Google Scholar
- B. S. Gulavani and S. Gulwani. A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In CAV, 2008. Google ScholarDigital Library
- S. Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL, 2011. Google ScholarDigital Library
- S. Gulwani and F. Zuleger. The reachability-bound problem. In PLDI, 2010. Google ScholarDigital Library
- S. Gulwani, S. Jain, and E. Koskinen. Control-flow refinement and progress invariants for bound analysis. In PLDI, 2009a. S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: precise and efficient static estimation of program computational complexity. In POPL, 2009b. S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In PLDI, 2011. Google ScholarDigital Library
- W. R. Harris and S. Gulwani. Spreadsheet table transformations from examples. In PLDI, 2011. Google ScholarDigital Library
- M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, 2010. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, 2004. Google ScholarDigital Library
- J. Hoffmann and M. Hofmann. Amortized resource analysis with polynomial potential. In ESOP, 2010. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. In POPL, 2011. Google ScholarDigital Library
- D. Jovanovi´c and L. De Moura. Solving non-linear arithmetic. In Automated Reasoning, 2012. Google ScholarDigital Library
- leetcode. LeetCode online judge. https://leetcode.com/, 2016. Accessed: 2016.Google Scholar
- LIS. Problem LIS on LeetCode. https://leetcode.com/problems/ longest-increasing-subsequence/, 2016. Accessed: 2016.Google Scholar
- K. L. McMillan. Lazy abstraction with interpolants. In CAV, 2006. Google ScholarDigital Library
- G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. TOPLAS, 1(2), 1979. Google ScholarDigital Library
- O. Olivo, I. Dillig, and C. Lin. Static detection of asymptotic performance bugs in collection traversals. In PLDI, 2015. Google ScholarDigital Library
- A. Reynolds, M. Deters, V. Kuncak, C. Tinelli, and C. Barrett. Counterexample-guided quantifier instantiation for synthesis in smt. In CAV, 2015.Google Scholar
- M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In CAV, 2014. Google ScholarDigital Library
- V. Sofronie-Stokkermans. Interpolation in local theory extensions. In Logical Methods in Computer Science, 2008.Google ScholarCross Ref
- A. Solar-Lezama, R. Rabbah, R. Bodík, and K. Ebcio˘glu. Programming by sketching for bit-streaming programs. In PLDI, 2005. Google ScholarDigital Library
- A. Tarski. A decision method for elementary algebra and geometry. Texts and Monogrpahs in Symbolic Computation, 1951.Google ScholarCross Ref
- N. Totla and T. Wies. Complete instantiation based interpolation. In POPL, 2013. Google ScholarDigital Library
- A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. Martin, and R. Alur. Transit: specifying protocols with concolic snippets. In PLDI, 2013. Google ScholarDigital Library
- R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. B. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. P. Puschner, J. Staschulat, and P. Stenström. The worst-case executiontime problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst., 7(3), 2008. Google ScholarDigital Library
- z3. Z3prover/z3 - github. https://github.com/Z3Prover/z3, 2015.Google Scholar
- Accessed: 2015 Nov 7. Introduction Overview An Iterative Implementation of Binary Search Inductive Step-Count Invariants Synthesizing Step-Count Invariants Background Target Language Program Structure Program Semantics Formal Logic Symbolic Representation of Program Semantics Interpolation Technical Approach Summaries Verification Algorithm Per-Path Bound Satisfaction as Tree-Interpolation Tree Interpolation by Theorem Enumeration The Theorem-Proving Algorithm Enumerating Quantifier-Free T-Theorems Properties Evaluation Benchmarks Results and Conclusions Related Work ConclusionGoogle Scholar
Index Terms
- Complexity verification using guided theorem enumeration
Recommendations
Complexity verification using guided theorem enumeration
POPL '17Determining if a given program satisfies a given bound on the amount of resources that it may use is a fundamental problem with critical practical applications. Conventional automatic verifiers for safety properties cannot be applied to address this ...
Interpolation guided compositional verification
ASE '15: Proceedings of the 30th IEEE/ACM International Conference on Automated Software EngineeringModel checking suffers from the state space explosion problem. Compositional verification techniques such as assume-guarantee reasoning (AGR) have been proposed to alleviate the problem. However, there are at least three challenges in applying AGR. ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Comments