Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits
Abstract elided by the publisher.
Related papers
- An Algebra for Delay-Insensitive Circuits CAV 1990
- Verifying Liveness Properties by Verifying Safety Properties CAV 1990
- LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs PLDI 2024
- Reducing liveness to safety in first-order logic POPL 2018
- Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions POPL 2024
- Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic OOPSLA 2026
- LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols PLDI 2025
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms POPL 2017