Pietro Braione
Giovanni Denaro
Mauro Pezzè
ABSTRACT
Symbolic analysis is a core component of many automatic test generation and program verication approaches. To verify complex software systems, test and analysis techniques shall deal with the many aspects of the target systems at different granularity levels. In particular, testing software programs that make extensive use of heap data structures at unit and integration levels requires generating suitable input data structures in the heap. This is a main challenge for symbolic testing and analysis techniques that work well when dealing with numeric inputs, but do not satisfactorily cope with heap data structures yet. In this paper we propose a language HEX to specify invariants of partially initialized data structures, and a decision procedure that supports the incremental evaluation of structural properties in HEX. Used in combination with the symbolic execution of heap manipulating programs, HEX prevents the exploration of invalid states, thus improving the eefficiency of program testing and analysis, and avoiding false alarms that negatively impact on verication activities. The experimental data conrm that HEX is an effective and efficient solution to the problem of testing and analyzing heap manipulating programs, and outperforms the alternative approaches that have been proposed so far.
- A. Bouajjani, C. Drˇ agoi, C. Enea, and M. Sighireanu. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In S. Chakraborty and M. Mukund, editors, Automated Technology for Verification and Analysis, LNCS, pages 167–182. Springer, 2012. Google Scholar
Digital 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, and M. Pezzè. Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization. In Proc. of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pages 411–421, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- 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
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: automatically generating inputs of death. In ACM Conference on Computer and Communications Security. ACM, 2006. Google ScholarDigital Library
- L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Trans. on Soft. Eng., 2(3):215–222, Sept. 1976. Google ScholarDigital Library
- A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezzè. Using symbolic execution for verifying safety-critical systems. In Proceedings of the Joint European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2001. Google ScholarDigital Library
- 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):405–435, 2005. Google ScholarDigital Library
- C. Enea, V. Saveluc, and M. Sighireanu. Compositional invariant checking for overlaid and nested linked lists. In Proceedings of the European Conference on Programming Languages and Systems, ESOP’13, pages 129–148. Springer-Verlag, 2013. Google ScholarDigital Library
- J. P. Galeotti, N. Rosner, C. G. López Pombo, and M. F. Frias. Analysis of invariants for efficient bounded verification. In Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA ’10, pages 25–36, New York, NY, USA, 2010. ACM. Google ScholarDigital Library
- J. Geldenhuys, N. Aguirre, M. Frias, and W. Visser. Bounded lazy initialization. In G. Brat, N. Rungta, and A. Venet, editors, NASA Formal Methods, LNCS 7871. Springer Berlin Heidelberg, 2013.Google ScholarCross Ref
- 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
- J. G. Henriksen, J. L. Jensen, M. E. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Proc. of the Int. Workshop on Tools and Algorithms for Construction and Analysis of Systems, TACAS. Springer-Verlag, 1995. Google ScholarDigital Library
- D. Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2006. Google ScholarDigital Library
- R. Just, D. Jalali, and M. D. Ernst. Defects4J: A database of existing faults to enable controlled testing studies for Java programs. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pages 437–440, 2014. 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
- B. Liskov and J. Guttag. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1st edition, 2000. Google ScholarDigital Library
- P. Madhusudan and X. Qiu. Efficient decision procedures for heaps using strand. In Proc. of the 18th International Conference on Static Analysis, SAS’11, pages 43–59. Springer-Verlag, 2011. Google ScholarDigital Library
- P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 123–136, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- R. Majumdar and R.-G. Xu. Directed test generation using symbolic grammars. In Proc. of the Int. Conference on Automated Software Engineering, ASE ’07, New York, NY, USA, 2007. ACM. Google ScholarDigital Library
- S. McPeak and G. C. Necula. Data structure specifications via local equality axioms. In Proc. of the 17th International Conference on Computer Aided Verification, CAV’05. Springer-Verlag, 2005. Google ScholarDigital Library
- A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, PLDI ’01, pages 221–231, New York, NY, USA, 2001. ACM. Google ScholarDigital Library
- C. S. Pasareanu and W. Visser. A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transf., 11(4):339–353, Oct. 2009. Google ScholarDigital Library
- Z. Rakamari´ c, R. Bruttomesso, A. J. Hu, and A. Cimatti. Verifying heap-manipulating programs in an SMT framework. In Proc. of the 5th International Conference on Automated Technology for Verification and Analysis, ATVA’07, pages 237–252. Springer-Verlag, 2007. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS ’02, pages 55–74, Washington, DC, USA, 2002. IEEE Computer Society. 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
- W. Visser, C. S. Pˇ asˇ areanu, and S. Khurshid. Test input generation with Java PathFinder. In Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2004), pages 97–107. ACM, 2004. Google ScholarDigital Library
- G. Yorsh, A. Rabinovich, M. Sagiv, A. Meyer, and A. Bouajjani. A logic of reachable patterns in linked data-structures. In Proc. of the 9th European Joint Conference on Foundations of Software Science and Computation Structures, FOSSACS’06. Springer-Verlag, 2006. Google ScholarDigital Library
Index Terms
- Symbolic execution of programs with heap inputs
Recommendations
Combining symbolic execution and search-based testing for programs with complex heap inputs
ISSTA 2017: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and AnalysisDespite the recent improvements in automatic test case generation, handling complex data structures as test inputs is still an open problem. Search-based approaches can generate sequences of method calls that instantiate structured inputs to exercise a ...
JBSE: a symbolic executor for Java programs with complex heap inputs
FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software EngineeringWe present the Java Bytecode Symbolic Executor (JBSE), a symbolic executor for Java programs that operates on complex heap inputs. JBSE implements both the novel Heap EXploration Logic (HEX), a symbolic execution approach to deal with heap inputs, and ...
Runtime exception detection in Java programs using symbolic execution
Most of the runtime failures of a software system can be revealed during test execution only, which has a very high cost. In Java programs, runtime failures are manifested as unhandled runtime exceptions.
In this paper we present an approach and tool ...
Comments