A BDD-based model checker for recursive programs

Javier Esparza; Stefan Schwoon

doi:10.1007/3-540-44585-4_30

A BDD-based model checker for recursive programs

Javier Esparza, Stefan Schwoon

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

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

123 Scopus citations

Abstract

We present a model-checker for boolean programs with (possibly recursive) procedures and the temporal logic LTL. The checker is guaranteed to terminate even for (usually faulty) programs in which the depth of the recursion is not bounded. The algorithm uses automata to finitely represent possibly infinite sets of stack contents and BDDs to compactly represent finite sets of values of boolean variables. We illustrate the checker on some examples and compare it with the Bebop tool of Ball and Rajamani.

Original language	English
Title of host publication	Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings
Editors	Hubert Comon, Alain Finkel, Gérard Berry
Publisher	Springer Verlag
Pages	324-336
Number of pages	13
ISBN (Print)	3540423451
DOIs	https://doi.org/10.1007/3-540-44585-4_30
State	Published - 2001
Event	13th International Conference on Computer Aided Verification, CAV 2001 - Paris, France Duration: 18 Jul 2001 → 22 Jul 2001

Publication series

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

Conference

Conference	13th International Conference on Computer Aided Verification, CAV 2001
Country/Territory	France
City	Paris
Period	18/07/01 → 22/07/01

Access to Document

10.1007/3-540-44585-4_30

Cite this

Esparza, J., & Schwoon, S. (2001). A BDD-based model checker for recursive programs. In H. Comon, A. Finkel, & G. Berry (Eds.), Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings (pp. 324-336). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2102). Springer Verlag. https://doi.org/10.1007/3-540-44585-4_30

Esparza, Javier ; Schwoon, Stefan. / A BDD-based model checker for recursive programs. Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings. editor / Hubert Comon ; Alain Finkel ; Gérard Berry. Springer Verlag, 2001. pp. 324-336 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5463318350be449e9bd6d67c2c89e2a1,

title = "A BDD-based model checker for recursive programs",

abstract = "We present a model-checker for boolean programs with (possibly recursive) procedures and the temporal logic LTL. The checker is guaranteed to terminate even for (usually faulty) programs in which the depth of the recursion is not bounded. The algorithm uses automata to finitely represent possibly infinite sets of stack contents and BDDs to compactly represent finite sets of values of boolean variables. We illustrate the checker on some examples and compare it with the Bebop tool of Ball and Rajamani.",

author = "Javier Esparza and Stefan Schwoon",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2001.; 13th International Conference on Computer Aided Verification, CAV 2001 ; Conference date: 18-07-2001 Through 22-07-2001",

year = "2001",

doi = "10.1007/3-540-44585-4_30",

language = "English",

isbn = "3540423451",

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

publisher = "Springer Verlag",

pages = "324--336",

editor = "Hubert Comon and Alain Finkel and G{\'e}rard Berry",

booktitle = "Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings",

}

Esparza, J & Schwoon, S 2001, A BDD-based model checker for recursive programs. in H Comon, A Finkel & G Berry (eds), Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2102, Springer Verlag, pp. 324-336, 13th International Conference on Computer Aided Verification, CAV 2001, Paris, France, 18/07/01. https://doi.org/10.1007/3-540-44585-4_30

A BDD-based model checker for recursive programs. / Esparza, Javier; Schwoon, Stefan.
Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings. ed. / Hubert Comon; Alain Finkel; Gérard Berry. Springer Verlag, 2001. p. 324-336 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2102).

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

TY - GEN

T1 - A BDD-based model checker for recursive programs

AU - Esparza, Javier

AU - Schwoon, Stefan

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2001.

PY - 2001

Y1 - 2001

N2 - We present a model-checker for boolean programs with (possibly recursive) procedures and the temporal logic LTL. The checker is guaranteed to terminate even for (usually faulty) programs in which the depth of the recursion is not bounded. The algorithm uses automata to finitely represent possibly infinite sets of stack contents and BDDs to compactly represent finite sets of values of boolean variables. We illustrate the checker on some examples and compare it with the Bebop tool of Ball and Rajamani.

AB - We present a model-checker for boolean programs with (possibly recursive) procedures and the temporal logic LTL. The checker is guaranteed to terminate even for (usually faulty) programs in which the depth of the recursion is not bounded. The algorithm uses automata to finitely represent possibly infinite sets of stack contents and BDDs to compactly represent finite sets of values of boolean variables. We illustrate the checker on some examples and compare it with the Bebop tool of Ball and Rajamani.

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

U2 - 10.1007/3-540-44585-4_30

DO - 10.1007/3-540-44585-4_30

M3 - Conference contribution

AN - SCOPUS:84958757867

SN - 3540423451

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

SP - 324

EP - 336

BT - Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings

A2 - Comon, Hubert

A2 - Finkel, Alain

A2 - Berry, Gérard

PB - Springer Verlag

T2 - 13th International Conference on Computer Aided Verification, CAV 2001

Y2 - 18 July 2001 through 22 July 2001

ER -

Esparza J, Schwoon S. A BDD-based model checker for recursive programs. In Comon H, Finkel A, Berry G, editors, Computer Aided Verification - 13th International Conference, CAV 2001, Proceedings. Springer Verlag. 2001. p. 324-336. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-44585-4_30

A BDD-based model checker for recursive programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this