QBF Encoding of Temporal Properties and QBF-Based Verification

DOI10.1007/978-3-319-08587-6_16MaRDI QIDQ3192192zbMATH OpenOpenAlexFDO

Authors Wenhui Zhang

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_16

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• QBF-Based Symbolic Model Checking for Knowledge and Time
• Publication:4945224
• scientific article; zbMATH DE number 1512710
• On the expressivity and complexity of quantitative branching-time temporal logics
• Verifying quantitative temporal properties of procedural programs
• Theoretical Aspects of Computing – ICTAC 2005
• scientific article; zbMATH DE number 2084388
• Temporal logics for reasoning about quantum systems
• scientific article; zbMATH DE number 2087443

Cited in

(7)

• CAQE and QuAbS: Abstraction Based QBF Solvers
• QBF-Based Symbolic Model Checking for Knowledge and Time
• Linear templates of ACTL formulas with an application to SAT-based verification
• First order Büchi automata and their application to verification of LTL specifications
• Compressing BMC encodings with QBF
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• CTL model checking in deduction modulo

This page was built for publication: QBF Encoding of Temporal Properties and QBF-Based Verification

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