Simple Bounded LTL Model Checking (2004)
AUTHORS:
Latvala Timo
,
Biere Armin,
Heljanko Keijo
,
Junttila Tommi
URL:
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A92.shtml
@techreport{ HUT-TCS-A92, author = "Latvala, Timo and Biere, Armin and Heljanko, Keijo and Junttila, Tommi", institution = "Helsinki University of Technology, Laboratory for Theoretical Computer Science", title = "Simple Bounded {LTL} Model Checking", url = "http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A92.shtml", 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.", year = "2004", number = "A92", month = "July", juforank = "NA", corerank = "NA", flags = "copy SA-53695", address = "Espoo, Finland", keywords = "{LTL}, Bounded Model Checking, {NuSMV}", type = "Research Report", pages = "16" }