TY - GEN
T1 - Error invariants
AU - Ermis, Evren
AU - Schäf, Martin
AU - Wies, Thomas
PY - 2012
Y1 - 2012
N2 - Localizing the cause of an error in an error trace is one of the most time-consuming aspects of debugging. We develop a novel technique to automate this task. For this purpose, we introduce the concept of error invariants. An error invariant for a position in an error trace is a formula over program variables that over-approximates the reachable states at the given position while only capturing states that will still produce the error, if execution of the trace is continued from that position. Error invariants can be used for slicing error traces and for obtaining concise error explanations. We present an algorithm that computes error invariants from Craig interpolants, which we construct from proofs of unsatisfiability of formulas that explain why an error trace violates a particular correctness assertion. We demonstrate the effectiveness of our algorithm by using it to localize faults in real-world programs.
AB - Localizing the cause of an error in an error trace is one of the most time-consuming aspects of debugging. We develop a novel technique to automate this task. For this purpose, we introduce the concept of error invariants. An error invariant for a position in an error trace is a formula over program variables that over-approximates the reachable states at the given position while only capturing states that will still produce the error, if execution of the trace is continued from that position. Error invariants can be used for slicing error traces and for obtaining concise error explanations. We present an algorithm that computes error invariants from Craig interpolants, which we construct from proofs of unsatisfiability of formulas that explain why an error trace violates a particular correctness assertion. We demonstrate the effectiveness of our algorithm by using it to localize faults in real-world programs.
UR - http://www.scopus.com/inward/record.url?scp=84865966656&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84865966656&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-32759-9_17
DO - 10.1007/978-3-642-32759-9_17
M3 - Conference contribution
AN - SCOPUS:84865966656
SN - 9783642327582
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 187
EP - 201
BT - FM 2012
T2 - 18th International Symposium on Formal Methods, FM 2012
Y2 - 27 August 2012 through 31 August 2012
ER -