Symbolic Execution and Model Checking for Testing
89Google Tech Talks
November, 16 2007
This talk describes techniques that use model checking and symbolic
execution for test input generation. Abstract state matching is used
to avoid generation of redundant inputs. The techniques handle complex
data structures, arrays, as well as multithreading, and generate
optimized test suites that satisfy user-specified testing coverage
criteria. The techniques are applicable to both (executable) models
and to code, and can be used in black box or white box fashion. We
have applied the techniques to generate test sequences for
object-oriented code and to generate test vectors for NASA software.
Speaker: Corina Pasareanu
Corina is a Research Scientist at NASA Ames Research Center, in the Robust Software Engineering Group, employed by Perot Systems Government Services. She received her Ph.D. in Computer Science from Kansas State University. She is currently investigating the use of abstraction and symbolic execution in the context of the Java PathFinder model checker, with applications in test input generation and error detection. She is also working on using learning techniques for automating assume-guarantee compositional verification. Her other research interests involve the design of a command execution language and the verification of the associated execution system (PLEXIL).