Formal Methods in Computer-Aided Design

DOI10.1007/B102264MaRDI QIDQ5492980zbMATH OpenOpenAlexFDO

Authors Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila

Publication date 20 October 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b102264

zbMATH Keywords

bounded model checkinglinear translationLTLNuSMV

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A compact linear translation for bounded model checking
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2086516
• Bounded model checking with SNF, alternating automata, and Büchi automata

Cited in

(10)

• Limitations of restricted branching in clause learning
• Counterexample-preserving reduction for symbolic model checking
• Easy instances for model checking
• A compact linear translation for bounded model checking
• SAT-Based Model Checking
• Limitations of Restricted Branching in Clause Learning
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Bounded model checking of ETL cooperating with finite and looping automata connectives
• Formal Methods in Computer-Aided Design
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Formal Methods in Computer-Aided Design

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5492980)