Counter Example Analysis Papers
Checking properties of abstracted systems can produce results that are inconclusive. For Bandera, we may get a false result that does not correspond to a real system defect, rather it arises because the abstractions have introduced infeasible sequences of system actions that violate the property.
A variety of techniques can be used to help address this problem ranging from attempting to exercise the counter-example via directed-testing to full-blown symbolic execution. We are investigating several approaches that are cheap and appear effective on the systems we have studied. We are also interested in comparing these techniques to more computationally demanding theorem-prover based techniques, such as those incorporated in InVest.
- Finding Feasible Counter-examples when Model Checking Java Programs, Corina S. Pasareanu, Matthew B. Dwyer and Willem Visser, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer-Verlag, April, 2001.