ULTIMATE AUTOMIZER with array interpolation (Competition contribution)

Matthias Heizmann; Daniel Dietsch; Jan Leike; Betim Musa; Andreas Podelski

doi:10.1007/978-3-662-46681-0_43

ULTIMATE AUTOMIZER with array interpolation (Competition contribution)

Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Andreas Podelski

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

17 Citations (Scopus)

Abstract

Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
Editors	Cesare Tinelli, Christel Baier
Publisher	Springer Verlag
Pages	455-457
Number of pages	3
ISBN (Electronic)	9783662466803
DOIs	https://doi.org/10.1007/978-3-662-46681-0_43
Publication status	Published - 2015
Event	21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom Duration: 11 Apr 2015 → 18 Apr 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9035
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Country/Territory	United Kingdom
City	London
Period	11/04/15 → 18/04/15

Access to Document

10.1007/978-3-662-46681-0_43

Cite this

Heizmann, M., Dietsch, D., Leike, J., Musa, B., & Podelski, A. (2015). ULTIMATE AUTOMIZER with array interpolation (Competition contribution). In C. Tinelli, & C. Baier (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings (pp. 455-457). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035). Springer Verlag. https://doi.org/10.1007/978-3-662-46681-0_43

Heizmann, Matthias ; Dietsch, Daniel ; Leike, Jan et al. / ULTIMATE AUTOMIZER with array interpolation (Competition contribution). Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. editor / Cesare Tinelli ; Christel Baier. Springer Verlag, 2015. pp. 455-457 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7e9e1f9619db4331a74b8ff05ae89581,

title = "ULTIMATE AUTOMIZER with array interpolation (Competition contribution)",

abstract = "Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.",

author = "Matthias Heizmann and Daniel Dietsch and Jan Leike and Betim Musa and Andreas Podelski",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2015.; 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 ; Conference date: 11-04-2015 Through 18-04-2015",

year = "2015",

doi = "10.1007/978-3-662-46681-0_43",

language = "English",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "455--457",

editor = "Cesare Tinelli and Christel Baier",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings",

address = "Germany",

}

Heizmann, M, Dietsch, D, Leike, J, Musa, B & Podelski, A 2015, ULTIMATE AUTOMIZER with array interpolation (Competition contribution). in C Tinelli & C Baier (eds), Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9035, Springer Verlag, pp. 455-457, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, United Kingdom, 11/04/15. https://doi.org/10.1007/978-3-662-46681-0_43

ULTIMATE AUTOMIZER with array interpolation (Competition contribution). / Heizmann, Matthias; Dietsch, Daniel; Leike, Jan et al.
Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. ed. / Cesare Tinelli; Christel Baier. Springer Verlag, 2015. p. 455-457 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - ULTIMATE AUTOMIZER with array interpolation (Competition contribution)

AU - Heizmann, Matthias

AU - Dietsch, Daniel

AU - Leike, Jan

AU - Musa, Betim

AU - Podelski, Andreas

PY - 2015

Y1 - 2015

N2 - Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.

AB - Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with interpolation.

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

U2 - 10.1007/978-3-662-46681-0_43

DO - 10.1007/978-3-662-46681-0_43

M3 - Conference contribution

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

SP - 455

EP - 457

BT - Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings

A2 - Tinelli, Cesare

A2 - Baier, Christel

PB - Springer Verlag

T2 - 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015

Y2 - 11 April 2015 through 18 April 2015

ER -

Heizmann M, Dietsch D, Leike J, Musa B, Podelski A. ULTIMATE AUTOMIZER with array interpolation (Competition contribution). In Tinelli C, Baier C, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Springer Verlag. 2015. p. 455-457. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-46681-0_43

ULTIMATE AUTOMIZER with array interpolation (Competition contribution)

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this