Classifying bugs with interpolants

Andreas Podelski, Martin Schäf, Thomas Wies

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

Abstract

We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.

Original languageEnglish (US)
Title of host publicationTests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings
PublisherSpringer Verlag
Pages151-168
Number of pages18
Volume9762
ISBN (Print)9783319411347
DOIs
StatePublished - 2016
Event10th International Conference on Tests and Proofs, TAP 2016 and Held as Part of Software Technologies: Applications and Foundations, STAF 2016 - Vienna, Austria
Duration: Jul 5 2016Jul 7 2016

Publication series

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

Other

Other10th International Conference on Tests and Proofs, TAP 2016 and Held as Part of Software Technologies: Applications and Foundations, STAF 2016
CountryAustria
CityVienna
Period7/5/167/7/16

Fingerprint

Interpolants
Signature
Java
Interpolation
Interpolate
Semantics
Benchmark
Experiment
Experiments

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Podelski, A., Schäf, M., & Wies, T. (2016). Classifying bugs with interpolants. In Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings (Vol. 9762, pp. 151-168). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9762). Springer Verlag. https://doi.org/10.1007/978-3-319-41135-4_9

Classifying bugs with interpolants. / Podelski, Andreas; Schäf, Martin; Wies, Thomas.

Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings. Vol. 9762 Springer Verlag, 2016. p. 151-168 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9762).

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

Podelski, A, Schäf, M & Wies, T 2016, Classifying bugs with interpolants. in Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings. vol. 9762, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9762, Springer Verlag, pp. 151-168, 10th International Conference on Tests and Proofs, TAP 2016 and Held as Part of Software Technologies: Applications and Foundations, STAF 2016, Vienna, Austria, 7/5/16. https://doi.org/10.1007/978-3-319-41135-4_9
Podelski A, Schäf M, Wies T. Classifying bugs with interpolants. In Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings. Vol. 9762. Springer Verlag. 2016. p. 151-168. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-41135-4_9
Podelski, Andreas ; Schäf, Martin ; Wies, Thomas. / Classifying bugs with interpolants. Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings. Vol. 9762 Springer Verlag, 2016. pp. 151-168 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{07bd378274ae41bfaebfd51143ef2800,
title = "Classifying bugs with interpolants",
abstract = "We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.",
author = "Andreas Podelski and Martin Sch{\"a}f and Thomas Wies",
year = "2016",
doi = "10.1007/978-3-319-41135-4_9",
language = "English (US)",
isbn = "9783319411347",
volume = "9762",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "151--168",
booktitle = "Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Classifying bugs with interpolants

AU - Podelski, Andreas

AU - Schäf, Martin

AU - Wies, Thomas

PY - 2016

Y1 - 2016

N2 - We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.

AB - We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.

UR - http://www.scopus.com/inward/record.url?scp=84977595111&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84977595111&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-41135-4_9

DO - 10.1007/978-3-319-41135-4_9

M3 - Conference contribution

AN - SCOPUS:84977595111

SN - 9783319411347

VL - 9762

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 151

EP - 168

BT - Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016, Proceedings

PB - Springer Verlag

ER -