Linear templates of ACTL formulas with an application to SAT-based verification

DOI10.1016/J.IPL.2017.06.008MaRDI QIDQ2398494zbMATH OpenOpenAlexFDO

Authors Zhaowei Xu, Wenhui Zhang

Publication date 16 August 2017

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2017.06.008

zbMATH Keywords

bounded model checkingbounded semanticsformal methodslinear counterexamplesSAT-based verification

Mathematics Subject Classification ID

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

Recommendations

• Formal verification of a generic framework to synthesize SAT-provers
• On ACTL formulas having linear counterexamples
• Linear CNF formulas and satisfiability
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• Verification in ACL2 of a generic framework to synthesize SAT-provers
• scientific article; zbMATH DE number 2090300
• On Some SAT-Variants over Linear Formulas
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• A New Approach to Bounded Model Checking for Branching Time Logics
• A new translation from ECTL* to SAT*
• Bounded model checking for propositional projection temporal logic
• Bounded semantics
• Compressing BMC encodings with QBF
• Computer Aided Verification
• CTL model checking in deduction modulo
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• scientific article; zbMATH DE number 1799521 (Why is no real title available?)
• scientific article; zbMATH DE number 2140441 (Why is no real title available?)
• On ACTL formulas having linear counterexamples
• QBF Encoding of Temporal Properties and QBF-Based Verification
• SAT-based verification for timed component connectors
• Theory and Applications of Satisfiability Testing
• Using branching time temporal logic to synthesize synchronization skeletons
• Verification, Model Checking, and Abstract Interpretation
• “Sometimes” and “not never” revisited

Cited in

(2)

• On ACTL formulas having linear counterexamples
• First order Büchi automata and their application to verification of LTL specifications

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: Linear templates of ACTL formulas with an application to SAT-based verification

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