Higher-order quantifier elimination, counter simulations and fault-tolerant systems
From MaRDI portal
Publication:2031422
DOI10.1007/s10817-020-09578-5OpenAlexW3081978399MaRDI QIDQ2031422
Publication date: 9 June 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09578-5
satisfiability modulo theories2nd order quantifier eliminationcounter abstractionsverification of parameterized distributed systems
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Decision procedures for flat array properties
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Deciding Boolean algebra with Presburger arithmetic
- On the hardness of failure-sensitive agreement problems.
- Cardinality constraints for arrays (decidability results and applications)
- Counterexample-guided quantifier instantiation for synthesis in SMT
- An introduction to mathematical logic and type theory: To truth through proof.
- Constraint-based verification of parameterized cache coherence protocols
- Cutoff bounds for consensus algorithms
- The Heard-Of model: computing in distributed systems with benign faults
- Counting Constraints in Flat Array Fragments
- Generalized Property Directed Reachability
- A Logic-Based Framework for Verifying Consensus Algorithms
- Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
- What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
- On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
- Asynchronous consensus and broadcast protocols
- Reaching Agreement in the Presence of Faults
- Uniform consensus is harder than consensus
- Predicate abstraction for software verification
- Interpolation and Symbol Elimination
- Automated Deduction – CADE-20
- Tolerating corrupted communication
- On Verifying Fault Tolerance of Distributed Protocols
- MCMT: A Model Checker Modulo Theories
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
This page was built for publication: Higher-order quantifier elimination, counter simulations and fault-tolerant systems
