ABSTRACT
Symbolic execution suffers from problems when analyzing programs that handle complex data structures as their inputs and take decisions over non-linear expressions. For these programs, symbolic execution may incur invalid inputs or unidentified infeasible traces, and may raise large amounts of false alarms. Some symbolic executors tackle these problems by introducing executable preconditions to exclude invalid inputs, and some solvers exploit rewrite rules to address non linear problems. In this paper, we discuss the core limitations of executable preconditions, and address these limitations by proposing invariants specifically designed to harmonize with the lazy initialization algorithm. We exploit rewrite rules applied within the symbolic executor, to address simplifications of inverse relationships fostered from either program-specific calculations or the logic of the verification tasks. We present a symbolic executor that integrates the two techniques, and validate our approach against the verification of a relevant set of properties of the Tactical Separation Assisted Flight Environment. The empirical data show that the integrated approach can improve the effectiveness of symbolic execution.
- S. Anand, C. S. Pˇ asˇ areanu, and W. Visser. JPF-SE: A symbolic execution extension to Java PathFinder. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 4424. Springer, 2007. Google ScholarDigital Library
- A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic, 10(1), 2009. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN workshop on Model checking of software, LNCS 2057. Springer, 2001. Google ScholarDigital Library
- J. Belt, Robby, and X. Deng. Sireum/Topi LDP: A lightweight semi-decision procedure for optimizing symbolic execution-based analyses. In ACM SIGSOFT symposium on The foundations of software engineering. ACM, 2009. Google ScholarDigital Library
- C. Borralleras, S. Lucas, A. Oliveras, E. Rodr´ıguez-Carbonell, and A. Rubio. SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning, 48(1), 2012. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: automated testing based on java predicates. In International symposium on Software testing and analysis. ACM, 2002. Google ScholarDigital Library
- P. Braione, G. Denaro, B. Kˇ rena, and M. Pezzè. Verifying LTL properties of Bytecode with symbolic execution. In 2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformation, 2008.Google Scholar
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation, 2008. Google ScholarDigital Library
- E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2988. Springer, 2004.Google Scholar
- L. de Moura and N. Bjorner. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 4963. Springer, 2008.Google Scholar
- X. Deng, J. Lee, and Robby. Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In International Conference on Automated Software Engineering, 2006. Google ScholarDigital Library
- G. D. Dennis. TSAFE: Building a trusted computing base for air traffic control software. Master’s thesis, Massachusetts Institute of Technology, 2003.Google Scholar
- H. Do, S. G. Elbaum, and G. Rothermel. Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. Empirical Software Engineering: An International Journal, 10(4), 2005. Google ScholarDigital Library
- H. Erzberger. The automated airspace concept. In Air Traffic Management R&D Seminar, 2001.Google Scholar
- D. Giannakopoulou, D. H. Bushnell, J. Schumann, H. Erzberger, and K. Heere. Formal testing for separation assurance. Annals of Mathematics and Artificial Intelligence, 63(1):5–30, 2011. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In ACM Conference on Programming language design and implementation. ACM, 2005. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In ACM Symposium on Principles of Programming Languages, 2002. Google ScholarDigital Library
- D. Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2006. Google ScholarDigital Library
- S. Jha, R. Limaye, and S. A. Seshia. Beaver: Engineering an efficient smt solver for bit-vector arithmetic. In International Conference on Computer Aided Verification, LNCS 5643. Springer, 2009. Google ScholarDigital Library
- S. A. Khalek, G. Yang, L. Zhang, D. Marinov, and S. Khurshid. Testera: A tool for testing java programs using alloy specifications. In International Conference on Automated Software Engineering, 2011. Google ScholarDigital Library
- S. Khurshid, C. S. Pˇ asˇ areanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for Construction and Analysis of Systems, LNCS 2619. Springer, 2003. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385–394, 1976. Google ScholarDigital Library
- D. Marinov and S. Khurshid. Testera: A novel framework for automated testing of java programs. In International Conference on Automated Software Engineering, 2001. Google ScholarDigital Library
- A. V. Nori and S. K. Rajamani. An empirical study of optimizations in YOGI. In International Conference on Software Engineering. ACM, 2010. Google ScholarDigital Library
- C. S. Pˇ asˇ areanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In International Symposium on Software Testing and Analysis. ACM, 2008. Google ScholarDigital Library
- C. S. Pˇ asˇ areanu, N. Rungta, and W. Visser. Symbolic execution with mixed concrete-symbolic solving. In International Symposium on Software Testing and Analysis, 2011. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In European Software Engineering Conference and ACM Symposium on Foundations of Software Engineering, 2005. Google ScholarDigital Library
- J. H. Siddiqui and S. Khurshid. Staged symbolic execution. In ACM Symposium on Applied Computing, 2012. Google ScholarDigital Library
- N. Sinha. Symbolic program analysis using term rewriting and generalization. In International Conference on Formal Methods in Computer-Aided Design, pages 19:1–19:9. IEEE, 2008. Google ScholarDigital Library
- M. Souza, M. Borges, M. d’Amorim, and C. S. Pˇ asˇ areanu. Coral: Solving complex constraints for symbolic pathfinder. In NASA Formal Methods, 2011. Google ScholarDigital Library
- W. Visser, C. S. Pˇ asˇ areanu, and S. Khurshid. Test input generation with Java PathFinder. In International Symposium on Software Testing and Analysis. ACM, 2004. Google ScholarDigital Library
- H. Zankl and A. Middeldorp. Satisfiability of non-linear (ir)rational arithmetic. In International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 2010. Google ScholarDigital Library
Index Terms
- Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization
Recommendations
Lazy counterfactual symbolic execution
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present counterfactual symbolic execution, a new approach that produces counterexamples that localize the causes of failure of static verification. First, we develop a notion of symbolic weak head normal form and use it to define lazy symbolic ...
Enhancing symbolic execution with veritesting
ICSE 2014: Proceedings of the 36th International Conference on Software EngineeringWe present MergePoint, a new binary-only symbolic execution system for large-scale and fully unassisted testing of commodity off-the-shelf (COTS) software. MergePoint introduces veritesting, a new technique that employs static symbolic execution to ...
Verifying systems rules using rule-directed symbolic execution
ASPLOS '13Systems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is ...
Comments