A Compact Linear Translation for Bounded Model Checking

DOI10.1016/J.ENTCS.2006.12.020zbMath1277.68134OpenAlexW2148461683MaRDI QIDQ2864381

Paul B. Jackson, Daniel Sheridan

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.12.020

zbMATH Keywords

denotational semanticslinear temporal logicSATbounded model checkingfixpoints

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Computer Aided Verification
• Unnamed Item
• Unnamed Item

This page was built for publication: A Compact Linear Translation for Bounded Model Checking