Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
A. Holzer, D. Kroening, C. Schallhart, M. Tautschnig, H. Veith:
"Proving Reachability Using FShell";
Vortrag: Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Tallinn, Estland;
24.03.2012
- 01.04.2012; in: "Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
Springer,
LNCS 7214
(2012),
ISBN: 978-3-642-28755-8;
S. 538
- 541.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-28756-5
Elektronische Version der Publikation:
http://www.springerlink.com/content/u125m751276420u3/fulltext.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.