FShell adapts the “program as database” metaphor previously used by the BLAST verifier from model checking to test generation. It generates families of testcases based on coverage criteria specified using the “FShell” query language (FQL) that (I think) was introduced in this paper.
(FQL is not described in detail in this paper.)
FShell uses CBMC as a backend (FQL was later used with many other tools in SV-Competition).
FShell is compared against the BLAST verifier on five cases ranging from 4800 to 45,000 lloc (logical lines of code == number of semicolons). (The benchmarks come from BLAST.) FShell is faster though the paper admits that BLAST is really a tool for full verification whereas FShell is optimized for generating tests. FShell generates more tests to achieve the same basic block coverage.
Also evaluated on three sorting algorithms (bubble, insertion, selection) while varying the input size. Presented as speedup against a model checker (probaby CBMC?).
Notes related to FShell: Systematic test case generation for dynamic analysis and measurement
Papers related to FShell: Systematic test case generation for dynamic analysis and measurement
- Software verification: Testing vs. model checking [beyer:hvc:2017]
- An introduction to test specification in FQL [holzer:hvc:2010]