Case studies on invariant generation using a saturation theorem prover

Kryštof Hoder; Laura Kovács; Andrei Voronkov

doi:10.1007/978-3-642-25324-9_1

Case studies on invariant generation using a saturation theorem prover

Kryštof Hoder, Laura Kovács, Andrei Voronkov

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

Abstract

Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties. We discuss implementation details of the method, present experimental results, and discuss the relation of the program properties obtained by our implementation and the intended meaning of the programs used in the experiments. © 2011 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Pages	1-15
Number of pages	14
Volume	7094
DOIs	https://doi.org/10.1007/978-3-642-25324-9_1
Publication status	Published - 2011
Event	10th Mexican International Conference on Artificial Intelligence, MICAI 2011 - Puebla Duration: 1 Jul 2011 → …

Conference

Conference	10th Mexican International Conference on Artificial Intelligence, MICAI 2011
City	Puebla
Period	1/07/11 → …

Access to Document

10.1007/978-3-642-25324-9_1

Cite this

@inproceedings{225f7eebd41a48a1ab7ade6f468ac758,

title = "Case studies on invariant generation using a saturation theorem prover",

abstract = "Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties. We discuss implementation details of the method, present experimental results, and discuss the relation of the program properties obtained by our implementation and the intended meaning of the programs used in the experiments. {\textcopyright} 2011 Springer-Verlag.",

author = "Kry{\v s}tof Hoder and Laura Kov{\'a}cs and Andrei Voronkov",

year = "2011",

doi = "10.1007/978-3-642-25324-9_1",

language = "English",

isbn = "9783642253232",

volume = "7094",

pages = "1--15",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

note = "10th Mexican International Conference on Artificial Intelligence, MICAI 2011 ; Conference date: 01-07-2011",

}

Hoder, K, Kovács, L & Voronkov, A 2011, Case studies on invariant generation using a saturation theorem prover. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 7094, pp. 1-15, 10th Mexican International Conference on Artificial Intelligence, MICAI 2011, Puebla, 1/07/11. https://doi.org/10.1007/978-3-642-25324-9_1

Case studies on invariant generation using a saturation theorem prover. / Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 7094 2011. p. 1-15.

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

TY - GEN

T1 - Case studies on invariant generation using a saturation theorem prover

AU - Hoder, Kryštof

AU - Kovács, Laura

AU - Voronkov, Andrei

PY - 2011

Y1 - 2011

N2 - Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties. We discuss implementation details of the method, present experimental results, and discuss the relation of the program properties obtained by our implementation and the intended meaning of the programs used in the experiments. © 2011 Springer-Verlag.

AB - Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties. We discuss implementation details of the method, present experimental results, and discuss the relation of the program properties obtained by our implementation and the intended meaning of the programs used in the experiments. © 2011 Springer-Verlag.

U2 - 10.1007/978-3-642-25324-9_1

DO - 10.1007/978-3-642-25324-9_1

M3 - Conference contribution

SN - 9783642253232

VL - 7094

SP - 1

EP - 15

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

T2 - 10th Mexican International Conference on Artificial Intelligence, MICAI 2011

Y2 - 1 July 2011

ER -

Case studies on invariant generation using a saturation theorem prover

Abstract

Conference

Access to Document

Fingerprint

Cite this