Error invariants

Evren Ermis, Martin Schäf, Thomas Wies

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


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
Subtitle of host publicationFormal Methods - 18th International Symposium, Proceedings
Number of pages15
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)0302-9743
ISSN (Electronic)1611-3349


Other18th International Symposium on Formal Methods, FM 2012

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Error invariants'. Together they form a unique fingerprint.

Cite this