Proving the Refuted: Symbolic Model Checkers as Proof Generators

DOI10.1007/978-3-642-11512-7_14zbMath1274.68174OpenAlexW1665907676MaRDI QIDQ5187831

Ittai Balaban, Amir Pnueli, Lenore D. Zuck

Publication date: 9 March 2010

Published in: Concurrency, Compositionality, and Correctness (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-11512-7_14

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Completing the temporal picture
• A compositional approach to CTL\(^*\) verification
• Model checking and abstraction to the aid of parameterized systems (a survey)
• From complementation to certification
• MODULAR RANKING ABSTRACTION
• All You Need Is Compassion

This page was built for publication: Proving the Refuted: Symbolic Model Checkers as Proof Generators