Boolean Abstraction for Temporal Logic Satisfiability

DOI10.1007/978-3-540-73368-3_53MaRDI QIDQ5429344zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_53

Mathematics Subject Classification ID

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

Recommendations

• A satisfiability-based approach to abstraction refinement in model checking
• Propositional temporal proving with reductions to a SAT problem
• A satisfiability procedure for quantified Boolean formulae
• Temporal induction by incremental SAT solving
• scientific article; zbMATH DE number 3974944

Cited in

(10)

• Tightening the contract refinements of a system architecture
• An explicit transition system construction approach to LTL satisfiability checking
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Reactive synthesis with maximum realizability of linear temporal logic specifications
• Extracting unsatisfiable cores for LTL via temporal resolution
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Diagnostic Information for Realizability
• Boolean abstractions for realizability modulo theories
• Computing minimal unsatisfiable core for LTL over finite traces

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: Boolean Abstraction for Temporal Logic Satisfiability

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