scientific article; zbMATH DE number 2086516

MaRDI QIDQ4736997zbMATH OpenFDO

Authors Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani

Publication date 11 August 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2294/22940196.htm

Mathematics Subject Classification ID

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

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
• scientific article; zbMATH DE number 2084774
• 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
• scientific article; zbMATH DE number 2084774 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication:

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