Incremental and Complete Bounded Model Checking for Full PLTL

Reference:

Keijo Heljanko, Tommi Junttila, and Timo Latvala. Incremental and complete bounded model checking for full PLTL. In Kousha Etessami and Sriram K. Rajamani, editors, Proceedings of the 17th International Conference on Computer Aided Verification (CAV'2005), volume 3576 of Lecture Notes in Computer Science, pages 98–111, Edinburgh, Scotland, United Kingdom, July 2005. Springer-Verlag.

Abstract:

Bounded model checking is an efficient method for finding bugs in system designs. The major drawback of the basic method is that it cannot prove properties, only disprove them. Recently, some progress has been made towards proving properties of LTL. We present an incremental and complete bounded model checking method for the full linear temporal logic with past (PLTL). Compared to previous works, our method both improves and extends current results in many ways: (i) our encoding is incremental, resulting in improvements in performance, (ii) we can prove non-existence of a counterexample at shallower depths in many cases, and (iii) we support full PLTL. We have implemented our method in the NuSMV2 model checker and report encouraging experimental results.

Keywords:

Bounded Model Checking, Incremental, Complete, PLTL, NuSMV

Suggested BibTeX entry:

@inproceedings{HelJunLat:CAV05,
    address = {Edinburgh, Scotland, United Kingdom},
    author = {Keijo Heljanko and Tommi Junttila and Timo Latvala},
    booktitle = {Proceedings of the 17th International Conference on Computer Aided Verification (CAV'2005)},
    editor = {Kousha Etessami and Sriram K. Rajamani},
    month = {July},
    pages = {98--111},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Incremental and Complete Bounded Model Checking for Full {PLTL}},
    volume = {3576},
    year = {2005},
}