Symbolic (Java) PathFinder – Symbolic Execution of Java bytecodes

July 17, 2008
Corina Pasareanu | NASA Ames Research Center

We describe an approach to testing complex safety critical software that combines unit-level symbolic execution and system-level concrete execution for generating test cases that satisfy user-specified testing criteria. We have developed Symbolic (Java) PathFinder – a symbolic execution framework that implements a non-standard bytecode interpreter on top of the Java PathFinder model checking tool. The framework propagates the symbolic information via attributes associated with the program data. Furthermore, we describe two techniques that use system-level concrete program executions to gather information about a unit’s input to improve the precision of the unit-level test case generation. We applied our approach to testing a prototype NASA flight software component. Our analysis helped discover a serious bug that resulted in design changes to the software. Although we give our presentation in the context of a NASA project, we believe that our work is relevant for other critical systems that require thorough testing. (joint work with many people)

Speaker Details

Corina Pãsãreanu is a Research Scientist at the NASA Ames Research Center, Robust Software Engineering Group. Her research focuses on using abstraction and symbolic execution in the context of software model checking, with applications to test input generation and error detection. Her research interests also include automating assume-guarantee compositional verification and designing languages for commanding robots. She received her PhD degree from Kansas State University. She has served on program committees for many meetings in the formal analysis area, such as CAV, ISSTA, FSE, and ICSE. She is also an associate editor for the ACM TOSEM journal. More information can be found on her web-page at: http://ti.arc.nasa.gov/people/pcorina/