[26 Jan]

Slicing + Model Checking applied to Fault Localization/Verification:

"Programmers use slicing while debugging", is well known. But while researching for dynamic slicing, I found two pieces of recent work that are very interesting because they combine slicing and model checking. They are:

[1] Error Explanation with Distance Metrics, Alex Groce, TACAS 04. (Fault Localization)
[2] Static Program Transformations for Efficient Software Model Checking. S. Vasudevan et. al., World Computer Congress. 04. (Verification)

Fault localization
The first paper is one of the latest of a series of paper by Alex Groce, which started with the paper "What went Wrong? Explaining Counterexamples" with Willam Visser. The goal here is: Localize the fault in a counterexample prodcued by a model checker. Model checker finds a counter-example, which is a trace showing how the property of interest is violated. It is similar to a trace of failing test case. This paper tries to find the cause of the bug in the failing trace by computing a trace using the model checker(statically) that is as "similar" as possible to the failing trace, but such that the property is not violated. That is, they find a successful, but very similar trace. Then the cause of the bug is the difference between the two. He defines it as delta-slicing – "the smallest subset of changes in values between two executions that result in a change in the value of this predicate?"

Comments:

Delta slicing is very close to "dicing". But surprisingly they dont mention that.
The idea is similar to Zeller's FSE paper in the sense that Groce also tries to find a successful trace from the failing trace. But Groce's way of finding the successful trace is more sound and systematic using a model checker whereas Zeller's technique is quite experimental. On the other hand, Groce's results are only applicable to programs of complexity and size that model checkers can handle.
I wonder if there is another way to find (statically) a successful, but similar trace systematically and using techniques of program analysis and that can handle real programs. The input is a dynamic slice obtained from a failing run and the error condition. Output is a dyanamic slice that is very similar to the one that is input, but that makes the error condition false. Something that comes close is, backward conditioned slicing[1,2]. Given a condition and a program point, the "backward conditioned" slice does not contain those statements of the program, such that if those statements are executed the condition will not be satisfied at that program point. For our problem, the condition is the negation of error condition. But what we need is a dynamic slice (data values), not just static slice(just program stmts) as conditioned slicing produces. Can we compute such a dyanmic slice using the insights of conditioned slicing?

[3] Backward conditioning: A new specialization technique and its application to program comprehension. Workshop on Program Comprehension 2001.
[4] Pre/Post Conditioned Slicing. ICSM 2001.

Verification
I have not read this paper well enough. But the idea is to use conditioned slicing and amorphous slicing to reduce the size of the program that is subjected to model checkeing. The numbers look extremely impressive: an order of improvement in speed on average. Looks to me a lot to do in this area as this is their first paper and also, amorphous and conditioned slicing are relatively recent ideas – atleast their use to aid model checking is most probably novel.

[5] Amorphous Program Slicing. WPC 97.

Last modified 27 January 2005 at 12:13 am by Saswat Anand