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...
| मुख्य लेखकों: | , , |
|---|---|
| अन्य लेखक: | |
| स्वरूप: | Conference item |
| प्रकाशित: |
Springer
2013
|