Under-approximating loops in C programs for fast counterexample detection
Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. U...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Springer Verlag
2015
|