FSHELL: Systematic Test Case Generation for Dynamic Analysis and Measurement Tool Paper
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith · 2008
Although the principal analogy between counterexample generation and white box testing has been repeatedly addressed, the usage patterns and per- formance requirements for software testing are quite different from formal verifi- cation. 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 architec- tural modifications which support efficient test case generation.