Abstract
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. © 2008 Springer-Verlag.
Cite
CITATION STYLE
Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2008). FSHELL: Systematic test case generation for dynamic analysis and measurement - Tool paper. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 209–213). https://doi.org/10.1007/978-3-540-70545-1_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
