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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Zolda, Michael; Kirner, Raimund: Calculating WCET estimates from timed traces (2016)
- Holzer, Andreas; Schallhart, Christian; Tautschnig, Michael; Veith, Helmut: Closure properties and complexity of rational sets of regular languages (2015)
- Beyer, Dirk; Holzer, Andreas; Tautschnig, Michael; Veith, Helmut: Information reuse for multi-goal reachability analyses (2013)
- Flanagan, Cormac (ed.); König, Barbara (ed.): Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24--April 1, 2012. Proceedings (2012)
- Holzer, Andreas; Kroening, Daniel; Schallhart, Christian; Tautschnig, Michael; Veith, Helmut: Proving reachability using FShell (competition contribution) (2012)
- Holzer, Andreas; Tautschnig, Michael; Schallhart, Christian; Veith, Helmut: An introduction to test specification in FQL (2011)