Reference: Javier Esparza and Stefan Schwoon. A BDD-based model checker for recursive programs. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Proceedings of CAV 2001, volume 2102 of Lecture Notes in Computer Science, pages 324–336. Springer, July 2001. Suggested BibTeX entry: @inproceedings{ES01,     author = {Javier Esparza and Stefan Schwoon},     booktitle = {Proceedings of CAV 2001},     editor = {G{\'e}rard Berry and Hubert Comon and Alain Finkel},     month = {July},     pages = {324--336},     publisher = {Springer},     series = {Lecture Notes in Computer Science},     title = {A {BDD}-based Model Checker for Recursive Programs},     volume = {2102},     year = {2001} }

GZipped PostScript (61 kB) See www.fmi.uni-stuttgart.de ...