Proving Reachability Using FShell - (Competition Contribution)

8 years 9 months ago
Proving Reachability Using FShell - (Competition Contribution)
FShell is an automated white-box test-input generator for C programs, computing test data with respect to user-specified code coverage criteria. The pillars of FShell are the declarative specification language FQL (FShell Query Language), an efficient back end for computing test data, and a mathematical framework to reason about coverage criteria. To solve the reachability problem posed in SV-COMP we specify coverage of ERROR labels. As back end, FShell uses bounded model checking, building upon components of CBMC and leveraging the power of SAT solvers for efficient enumeration of a full test suite. 1 Overview FShell implements automatic white-box test-input generation according to a user-defined coverage specification given in the declarative language FQL [5,6]. To resemble formal verification and solve the reachability problem presented in the SW Verification Competition we specify coverage of all ERROR labels. FQL is built on top of a concise mathematical framework for formal...
Andreas Holzer, Daniel Kroening, Christian Schallh
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Authors Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith
Comments (0)