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.