FMCAD 2004
START ConferenceManager
Simple Bounded LTL Model Checking
Timo Latvala, Armin Biere, Keijo Heljanko and Tommi Junttila
Presented at
Formal Methods in Computer-Aided Design (FMCAD 2004), Austin, Texas, November 14-17, 2004
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.
START
Conference Manager (V2.46.3)
Maintainer:
sanders@cs.ubc.ca