Linear Encodings of Bounded LTL Model Checking

DOI10.2168/LMCS-2(5:5)2006MaRDI QIDQ5310676zbMATH OpenFDO

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

Publication date 11 October 2007

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-2(5:5)2006

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2086516
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Verification, Model Checking, and Abstract Interpretation

Cited in

(29)

• Efficient data validation for geographical interlocking systems
• TOrPEDO : witnessing model correctness with topological proofs
• Counterexample-preserving reduction for symbolic model checking
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• Extracting unsatisfiable cores for LTL via temporal resolution
• A compact linear translation for bounded model checking
• Checking EMTLK properties of timed interpreted systems via bounded model checking
• SAT-Based Model Checking
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Bounded model checking of ETL cooperating with finite and looping automata connectives
• Solving parity games by a reduction to SAT
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• scientific article; zbMATH DE number 1979554 (Why is no real title available?)
• Constraint LTL satisfiability checking without automata
• Bounded semantics
• scientific article; zbMATH DE number 7559425 (Why is no real title available?)
• scientific article; zbMATH DE number 7559496 (Why is no real title available?)
• Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Bounded Model Checking for Weak Alternating Büchi Automata
• On simulation-based probabilistic model checking of mixed-analog circuits
• Exhaustive property oriented model-based testing with symbolic finite state machines
• SAT meets tableaux for linear temporal logic satisfiability
• Abstraction-based optimal controller synthesis using dynamic quantization and RRT*
• A collaborative approach for multi-threaded SAT solving
• HRELTL: a temporal logic for hybrid systems

Describes a project that uses

Uses Software

• SPIN
• NuSMV
• SATIRE
• Chaff
• LTL2BA

This page was built for publication: Linear Encodings of Bounded LTL Model Checking

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