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

DOI10.1016/j.ipl.2017.06.008zbMath1409.68176OpenAlexW2690776731MaRDI QIDQ2398494

Zhaowei Xu, Wen-Hui 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

formal methodsbounded model checkingbounded semanticslinear counterexamplesSAT-based verification

Mathematics Subject Classification ID

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

Uses Software

• MiniSat

Cites Work

• Unnamed Item
• Unnamed Item
• SAT-based verification for timed component connectors
• Bounded semantics
• Using branching time temporal logic to synthesize synchronization skeletons
• Compressing BMC Encodings with QBF
• QBF Encoding of Temporal Properties and QBF-Based Verification
• CTL Model Checking in Deduction Modulo
• A New Approach to Bounded Model Checking for Branching Time Logics
• “Sometimes” and “not never” revisited
• A New Translation from ECTL* to SAT
• Bounded Model Checking for Propositional Projection Temporal Logic
• Theory and Applications of Satisfiability Testing
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• On ACTL formulas having linear counterexamples