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 checkingLTLNuSMVlinear translation

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)

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

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)