Main Profile

At A Glance

Symbolic Execution and Model Checking for Testing

Google Tech TalksNovember, 16 2007This talk describes techniques that use model checking and symbolicexecution for test input generation. Abstract state matching is usedto avoid generation of redundant inputs. The techniques handle complexdata structures, arrays, as well as multithreading, and generateoptimized test suites that satisfy user-specified testing coveragecriteria. The techniques are applicable to both (executable) modelsand to code, and can be used in black box or white box fashion. Wehave applied the techniques to generate test sequences forobject-oriented code and to generate test vectors for NASA software.Speaker: Corina PasareanuCorina 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).
Length: 01:00:48


Questions about Symbolic Execution and Model Checking for Testing

Want more info about Symbolic Execution and Model Checking for Testing? Get free advice from education experts and Noodle community members.

  • Answer