@inproceedings{
    LatBieHelJun:FMCAD04,
    editor = "Hu, Alan J. and Martin, Andrew K.",
    author = "Latvala, Timo and Biere, Armin and Heljanko, Keijo and Junttila, Tommi",
    publisher = "Springer",
    title = "Simple bounded {LTL} model checking",
    url = "http://www.springerlink.com/link.asp?id=a1jnfcb7q9knc1q1",
    series = "Lecture Notes in Computer Science",
    booktitle = "Formal Methods in Computer-Aided Design 2004, 5th International Conference FMCAD'04, Austin, Texas, USA",
    abstract = "We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the formula and the length of the bound. The resulting CNF-formula has a linear number of variables and clauses.",
    month = "nov",
    volume = "3312",
    flags = "SA-53695",
    year = "2004",
    keywords = "{LTL}, Bounded Model Checking, {NuSMV}",
    pages = "186-200"
}