The Blame Game for Property-based Testing

We report on work in progress aiming to add blame features to property-based-testing in logic programming, in particular w.r.t. the mechanized meta-theory model checker αCheck. Once the latter reports a counterexample to a property stated in αProlog, a combination of abduction and proof explanation tries to help the user to locate the part of the program that is responsible for the unintended behavior. To evaluate whether these explanations are in fact useful, we need an unbiased collection of faulty programs, where the bugs location is unknown to us. We have thus implemented a mutation testing tool for αProlog that generates such a set. Preliminary experiments point to the usefulness of our blame allocator. The mutator is of independent interest, allowing us to gauge the effectiveness of the various strategies of αCheck in finding bugs in αProlog specifications.