Improving the encoding of LTL model checking into SAT
From MaRDI portal
Recommendations
- Accelerating LTL satisfiability checking by SAT solvers
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Comparing SAT encodings for model checking
- Saturation-based incremental LTL model checking with inductive proofs
- Theory and Applications of Models of Computation
- Improving saturation-based bounded model checking
Cited in
(14)- An explicit transition system construction approach to LTL satisfiability checking
- Optimized SAT encoding of conformance checking artefacts
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- Counterexample-preserving reduction for symbolic model checking
- A compact linear translation for bounded model checking
- scientific article; zbMATH DE number 5158957 (Why is no real title available?)
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
- Bounded model checking of ETL cooperating with finite and looping automata connectives
- Comparing SAT encodings for model checking
- Linear Encodings of Bounded LTL Model Checking
- Formal Methods in Computer-Aided Design
- Improving the translation from ECTL to SAT
- Verification, Model Checking, and Abstract Interpretation
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
This page was built for publication: Improving the encoding of LTL model checking into SAT
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4736997)
