Symbolic execution for testing Java programs with complex heap inputs
Faculty of Informatics at Universita della Svizzera italiana (Lugano, Switzerland) and,
Software Engineering at the University of Milano-Bicocca (Milano, Italy)
COM1 Level 2
SR9, COM1-02-09
Abstract:
In this talk, I will address the main hurdles that still hinder the automatic generation of test cases for programs that make extensive use of heap data structures by means of symbolic execution.
I will present a technique for generating suitable symbolic path conditions that predicate on heap data structures, which avoids false alarms by enriching symbolic execution with 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.
I will propose an approach to automatically convert symbolic path conditions into sequences of method calls that properly instantiate the data structures in the heap to execute the corresponding paths, by converting the path conditions to optimisation problems that are solved with search-based techniques to produce sequences of method calls that instantiate those inputs.
I will propose an approach to reuse solutions across formulas that share at least one solution, regardless of their structural resemblance, thus reducing the impact of SMT solvers on complex executions.
Biodata:
Mauro Pezze is currently a visiting professor at the National University of Singapore; he is a professor of software engineering at the Universita della Svizzera italiana (Lugano, Switzerland) and at the University of Milano-Bicocca (Milano, Italy). He is associate editor of the Software Testing, Verification and Reliability Journal, and has served as associate editor of IEEE Transactions on Software Engineering and ACM Transactions on Software Engineering, as general chair or the ACM International Symposium on Software Testing and Analysis in 2013, program chair of the International Conference on Software Engineering in 2012 and of the ACM International Symposium on Software Testing and Analysis in 2006.
He is the co-author of the widely cited book 'Software Testing and Analysis: Process, Principles and Techniques', and is known for his work on software testing, program analysis, self-healing and self-adaptive software systems.