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