Name
Abstract | ||
|---|---|---|
It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a theoretically sound test-generation procedure, it scales poorly for computing complex test suites for large sets of test goals, because each test goal requires an expensive run of the model checker. We represent test goals as automata and exploit relations between automata in order to reuse existing reachability information for the analysis of subsequent test goals. Exploiting the sharing of sub-automata in a series of reachability queries, we achieve considerable performance improvements over the standard approach. We show the practical use of our multi-goal reachability analysis in a predicate-abstraction-based test-input generator for the test-specification language FQL. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-37036-6_26 | ESOP |
Keywords | Field | DocType |
practical use,multi-goal reachability analysis,model checker,test input,reachability query,subsequent test goal,reachability information,complex test suite,test goal,information reuse,reachability specification | Model checking,Programming language,Reuse,Computer science,Automaton,Exploit,Basic block,Reachability,Theoretical computer science,Counterexample | Conference |
Volume | ISSN | Citations |
7792 | 0302-9743 | 11 |
PageRank | References | Authors |
0.51 | 24 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dirk Beyer | 1 | 1736 | 100.85 |
| Andreas Holzer | 2 | 197 | 13.62 |
| Michael Tautschnig | 3 | 425 | 25.84 |
| Helmut Veith | 4 | 2476 | 140.58 |