Error invariants

Evren Ermis, Martin Schäf, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationFM 2012: Formal Methods - 18th International Symposium, Proceedings
Pages187-201
Number of pages15
Volume7436 LNCS
DOIs
StatePublished - 2012
Event18th International Symposium on Formal Methods, FM 2012 - Paris, France
Duration: Aug 27 2012Aug 31 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7436 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other18th International Symposium on Formal Methods, FM 2012
CountryFrance
CityParis
Period8/27/128/31/12

Fingerprint

Invariant
Trace
Slicing
Debugging
Interpolants
Violate
Assertion
Correctness
Fault
Demonstrate

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Ermis, E., Schäf, M., & Wies, T. (2012). Error invariants. In FM 2012: Formal Methods - 18th International Symposium, Proceedings (Vol. 7436 LNCS, pp. 187-201). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7436 LNCS). https://doi.org/10.1007/978-3-642-32759-9_17

Error invariants. / Ermis, Evren; Schäf, Martin; Wies, Thomas.

FM 2012: Formal Methods - 18th International Symposium, Proceedings. Vol. 7436 LNCS 2012. p. 187-201 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7436 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Ermis, E, Schäf, M & Wies, T 2012, Error invariants. in FM 2012: Formal Methods - 18th International Symposium, Proceedings. vol. 7436 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7436 LNCS, pp. 187-201, 18th International Symposium on Formal Methods, FM 2012, Paris, France, 8/27/12. https://doi.org/10.1007/978-3-642-32759-9_17
Ermis E, Schäf M, Wies T. Error invariants. In FM 2012: Formal Methods - 18th International Symposium, Proceedings. Vol. 7436 LNCS. 2012. p. 187-201. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-32759-9_17
Ermis, Evren ; Schäf, Martin ; Wies, Thomas. / Error invariants. FM 2012: Formal Methods - 18th International Symposium, Proceedings. Vol. 7436 LNCS 2012. pp. 187-201 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{8d3a7e69b5074ce79c41d5f0a95593b2,
title = "Error invariants",
abstract = "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.",
author = "Evren Ermis and Martin Sch{\"a}f and Thomas Wies",
year = "2012",
doi = "10.1007/978-3-642-32759-9_17",
language = "English (US)",
isbn = "9783642327582",
volume = "7436 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "187--201",
booktitle = "FM 2012: Formal Methods - 18th International Symposium, Proceedings",

}

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

SN - 9783642327582

VL - 7436 LNCS

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: Formal Methods - 18th International Symposium, Proceedings

ER -