FShell: Systematic test case generation for dynamic analysis and measurement

Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 23 June 2020

Computer Aided Verification
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 209-213
2008
Note(s): BLAST verifier, CBMC verifier, FQL, SV-competition
Papers: holzer:hvc:2010

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?).

FShell Query Language (FQL)