Willem Visser
Jaco Geldenhuys
Matthew B. Dwyer
ABSTRACT
The analysis of constraints plays an important role in many aspects of software engineering, for example constraint satisfiability checking is central to symbolic execution. However, the norm is to recompute results in each analysis. We propose a different approach where every call to the solver is wrapped in a check to see if the result is not already available. While many tools use some form of results caching, the novelty of our approach is the persistence of results across runs, across programs being analyzed, across different analyses and even across physical location. Achieving such reuse requires that constraints be distilled into their essential parts and represented in a canonical form.
In this paper, we describe the key ideas of our approach and its implementation, the Green solver interface, which reduces constraints to a simple form, allows for reuse of constraint solutions within an analysis run, and allows for recycling constraint solutions produced in one analysis run for use in other analysis runs. We describe how we integrated Green into two existing symbolic execution tools and demonstrate the reuse we achieve in the different settings.
- C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07), volume 4590 of Lecture Notes in Computer Science, pages 298--302. Springer-Verlag, July 2007. Berlin, Germany. Google Scholar
Digital Library
- A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM, 53(2), Feb. 2010. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI'08, pages 209--224, Berkeley, CA, USA, 2008. USENIX Association. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. Exe: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur., 12(2):10:1--10:38, Dec. 2008. Google ScholarDigital Library
- Choco. Choco Solver. http://www.emn.fr/z-info/choco-solver/.Google Scholar
- T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson. Introduction to Algorithms. McGraw-Hill Higher Education, 2001. Google ScholarDigital Library
- L. de Moura, S. Owre, H. Rueç, J. Rushby, and N. Shankar. The ICS decision procedures for embedded deduction. In Automated Reasoning, volume 3097, pages 218--222. Springer, 2004.Google Scholar
- L. de Moura, H. Rueß, and N. Shankar. Justifying equality. Electron. Notes Theor. Comput. Sci., 125(3):69--85, July 2005. Google ScholarDigital Library
- R. A. DeMillo and A. J. Offutt. Constraint-based automatic test data generation. IEEE Trans. Software Eng., 17(9):900--910, 1991. Google ScholarDigital Library
- J. Geldenhuys, W. Visser, and M. B. Dwyer. Probabilistic symbolic execution. In Proceedings of the 21st International Symposium on Software Testing and Analysis, 2012. To appear. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. Molnar. Sage: whitebox fuzzing for security testing. Commun. ACM, 55(3):40--44, Mar. 2012. Google ScholarDigital Library
- R. Iosif. Symmetry reductions for model checking of concurrent dynamic software. International Journal on Software Tools for Technology Transfer (STTT), 6:302--319, 2004.Google Scholar
- Jedis. Redis Java Interface. http://code.google.com/p/jedis/.Google Scholar
- Y. Jia and M. Harman. An analysis and survey of the development of mutation testing. IEEE Transactions on Software Engineering, 2008(5):1--32, 2011. Google ScholarDigital Library
- Jumble. Jumble mutation testing tool. http://jumble.sourceforge.net/.Google Scholar
- LattE. LattE Integrale, UC Davis, Mathematics. http://www.math.ucdavis.edu/~latte.Google Scholar
- G. J. Myers. Art of Software Testing. John Wiley & Sons, Inc., 1979. Google ScholarDigital Library
- G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1(2):245--257, Oct. 1979. Google ScholarDigital Library
- S. Person, M. B. Dwyer, S. Elbaum, and C. S. Păsăreanu. Differential symbolic execution. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, pages 226--237, 2008. Google ScholarDigital Library
- S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. In Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation, pages 504--515, 2011. Google ScholarDigital Library
- C. S. Păsăreanu and N. Rungta. Symbolic PathFinder: symbolic execution of Java bytecode. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ASE '10, pages 179--180, New York, NY, USA, 2010. ACM. Google ScholarDigital Library
- D. Ramos and D. Engler. Practical, low-effort equivalence verification of real code. In Computer Aided Verification, pages 669--685. 2011. Google ScholarDigital Library
- Redis. Redis NoSQL Database. http://redis.io.Google Scholar
- T. Sang, F. Bacchus, P. Beame, H. A. Kautz, and T. Pitassi. Combining component caching and clause learning for effective model counting. In Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing, 2004.Google Scholar
- 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, pages 157--168, 2006. Google ScholarDigital Library
- SIR. SIR Repository. http://sir.unl.edu.Google Scholar
- N. Tillmann and J. De Halleux. Pex: white box test generation for .net. In Proceedings of the 2nd international conference on Tests and proofs, TAP'08, pages 134--153, Berlin, Heidelberg, 2008. Springer-Verlag. Google ScholarDigital Library
- W. Visser, C. S. Păsăreanu, and R. Pelánek. Test input generation for Java containers using state matching. In L. L. Pollock and M. Pezzè, editors, ISSTA, pages 37--48. ACM, 2006. Google ScholarDigital Library
- G. Yang, C. Păsăreanu, and S. Khurshid. Memoized symbolic execution. In Proceedings of the 21st International Symposium on Software Testing and Analysis, 2012. to appear. Google ScholarDigital Library
- Yikes. Yices SMT Solver. http://yices.csl.sri.com/.Google Scholar
- zChaff. SAT Research Group, Princeton University. http://www.princeton.edu/~chaff/zchaff.html.Google Scholar
Index Terms
- Green: reducing, reusing and recycling constraints in program analysis
Recommendations
Enhancing reuse of constraint solutions to improve symbolic execution
ISSTA 2015: Proceedings of the 2015 International Symposium on Software Testing and AnalysisConstraint solution reuse is an effective approach to save the time of constraint solving in symbolic execution. Most of the existing reuse approaches are based on syntactic or semantic equivalence of constraints. For example, the Green framework can ...
Symbolic Execution with Interval Solving and Meta-heuristic Search
ICST '12: Proceedings of the 2012 IEEE Fifth International Conference on Software Testing, Verification and ValidationA challenging problem in symbolic execution is to solve complex mathematical constraints such as constraints that include floating-point variables and transcendental functions. The inability to solve such constraints limit the application scope of ...
User-defined backtracking criteria for symbolic execution
Symbolic execution is a path-sensitive program analysis technique that aids users with program verification. To avoid exploring infeasible paths, symbolic execution checks the prefix of a current path for feasibility by adding a branch constraint to the ...
Comments