From complementation to certification

DOI10.1016/j.tcs.2005.07.021zbMath1079.68060MaRDI QIDQ2575735

Moshe Y. Vardi, Orna Kupferman

Publication date: 6 December 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.07.021

Mathematics Subject Classification ID

68Q45: Formal languages and automata

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

Related Items

Proving the Refuted: Symbolic Model Checkers as Proof Generators, MODULAR RANKING ABSTRACTION

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Alternating finite automata on \(\omega\)-words
• The complementation problem for Büchi automata with applications to temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Reasoning about infinite computations
• Safety, liveness and fairness in temporal logic
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• The complexity of verification
• Temporal logic can be more expressive
• Weak alternating automata are not that weak
• Synthesis of Communicating Processes from Temporal Logic Specifications
• Correct Hardware Design and Verification Methods
• A new heuristic for bad cycle detection using BDDs
• Model checking of safety properties