@inproceedings{
    LatBieHelJun:FMCAD04,
    editor = "Hu, Alan and Martin, Andy",
    author = "Latvala, Timo and Biere, Armin and Heljanko, Keijo and Junttila, Tommi",
    publisher = "Springer-Verlag",
    title = "Simple bounded {LTL} model checking",
    url = "http://users.ics.tkk.fi/kepa/publications/",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04)",
    corerank = "NA",
    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 = "November",
    volume = "3312",
    juforank = "1",
    flags = "copy SA-53695",
    year = "2004",
    keywords = "{LTL}, Bounded Model Checking, {NuSMV}",
    pages = "186--200"
}