Simple bounded LTL model checking. (English)
Hu, Alan J. (ed.) et al., Formal methods in computer-aided design. 5th international conference, FMCAD 2004, Austin, Texas, USA, November 15‒17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23738-0/pbk). Lecture Notes in Computer Science 3312, 186-200 (2004).
Summary: 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
Contact
Print
General Help
