Ort: Raum S2-02 / E302
Datum und Zeit: Dienstag, 13. Mai 2008, 16:25-18:00 Uhr

Michael Tautschnig

FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement

Although the principal analogy between counterexample generation and white
box testing has been repeatedly addressed, the usage patterns and
performance requirements for software testing are quite different from
formal verification. Our tool FShell provides a versatile testing
environment for C programs which supports both interactive explorative use
and a rich scripting language. More than a frontend for software model
checkers, FShell is designed as a database engine which dispatches queries
about the program to program analysis tools. We report on the integration of
CBMC into FShell and describe architectural modifications which support
efficient test case generation.