Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses

ABSTRACT

Automated theorem proving techniques such as Satisfiability Modulo Theory (SMT) solvers have seen significant advances in the past several years. These advancements, coupled with vast hardware improvements, have drastic impact on, for example, program verification techniques and tools. The general availability of robust general purpose solvers have reduced a significant engineering overhead when designing and developing program verifiers. However, most solver implementations are designed to be used as a black box, and due to their aim as general purpose solvers, they often miss optimization opportunities that can be done by leveraging domain-specific knowledge.

This paper presents our effort to leverage domain-specific knowledge for optimizing symbolic execution (SymExe)-based analyses; we present optimization techniques incorporated as a lightweight semi-decision procedure (LDP) that provides up to an order of magnitude faster analysis time when analyzing realistic programs and well-known algorithms. LDP sits in the middle between a SymExe-based analysis tool and an existing SMT solver; it aims to reduce the number of solver calls by intercepting them and attempting to solve constraints using its lightweight deductive engine.

REFERENCES

• 1: S. Anand, C. S. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to Java PathFinder. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 134--138, 2007.
• 2: L. Baresi, C. Ghezzi, and L. Mottola. On accurate automatic verification of publish-subscribe architectures. In Proceedings of the 29th International Conference on Software Engineering (ICSE), pages 199--208. IEEE Computer Society, 2007.
• 3: C. Barrett, S. Ranise, A. Stump, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2008.
• 4: C. Barrett and C. Tinelli. CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV), volume 4590 of Lecture Notes in Computer Science, pages 298--302. Springer-Verlag, 2007.
• 5: P. Baumgartner, A. Fuchs, and C. Tinelli. Lemma learning in the model evolution calculus. In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 4246 of Lecture Notes in Computer Science, pages 572--586. Springer, 2006.
• 6: J. Belt, Robby, and X. Deng. Sireum/Topi LDP: A lightweight semi-decision procedure for optimizing symbolic execution-based analyses. Technical Report SAnToS TR2009-03-16, Kansas State University, 2009.
• 7: C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224. USENIX Association, 2008.
• 8: E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Jan. 2000.
• 9: M. B. Cohen, M. B. Dwyer, and J. Shi. Exploiting constraint solving history to construct interaction test suites. In Proceedings of the Testing: Academic and Industrial Conference Practice and Research Techniques (TAIC PART), pages 121--132. IEEE Computer Society, 2007.
• 10: P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming, pages 106--130. Dunod, Paris, France, 1976.
• 11: L. de Moura. Personal communication, 2009.
• 12: L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer, 2008.
• 13: X. Deng, J. Lee, and Robby. Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 157--166, 2006.
• 14: X. Deng, Robby, and J. Hatcli. Kiasan/KUnit: Automatic test case generation and analysis feedback for open object-oriented systems. In Proceedings of the Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART), 2007.
• 15: X. Deng, Robby, and J. Hatcli. Towards a case-optimal symbolic execution algorithm for analyzing strong properties of ob ject-oriented programs. In Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pages 273--282. IEEE Computer Society, 2007.
• 16: N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pages 243--320, 1990.
• 17: B. Duterte. Personal communication, 2008.
• 18: B. Dutertre and L. de Moura. The Yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf, August 2006.
• 19: M. B. Dwyer, J. Hatcli, Robby, and V. P. Ranganath. Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Formal Methods in System Design (FMSD), 25(2-3):199--240, 2004.
• 20: J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.
• 21: D. Kroening, O. Strichman, and R. E. Bryant. Decision Procedures: An Algorithmic Point of Views. Springer, jul 2008.
• 22: G. T. Leavens, A. L. Baker, and C. Ruby. JML: a Java modeling language. In Formal Underpinnings of Java Workshop (at OOPSLA'98), 1998.
• 23: R. Moore. Interval Analysis. Prentice Hall, 1966.
• 24: F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999.
• 25: O. Rüthing, J. Knoop, and B. Steen. Detecting equalities of variables: Combining efficiency with precision. In Proceedings of the 6th International Symposium on Static Analysis (SAS), pages 232--247. Springer-Verlag, 1999.
• 26: K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for c. In Proceedings of the 10th European Software Engineering Conference (ESEC) held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pages 263--272. ACM, 2005.
• 27: S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In Proceedings of the 2006 International Symposium on Software Testing and Analysis (ISSTA), pages 157--168. ACM, 2006.
• 28: C. Tinelli. A DPLL-based calculus for ground satisfiability modulo theories. In Proceedings of the European Conference on Logics in Artificial Intelligence (JELIA), pages 308--319. Springer-Verlag, 2002.
• 29: K. Waldén and J.-M. Nerson. Seamless object-oriented software architecture: analysis and design of reliable systems. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1995.
• 30: Sireum website. http://www.sireum.org, 2009.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Programming by contract; Validation
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Inference engines

General Terms:
Algorithms, Performance, Theory, Verification

Keywords:
decision procedure, program analysis, symbolic execution