Higher-order quantifier elimination, counter simulations and fault-tolerant systems (Q2031422): Difference between revisions

@@ Property / describes a project that uses @@
+ETPS
@@ Property / describes a project that uses: ETPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SeaHorn
@@ Property / describes a project that uses: SeaHorn / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+nuXmv
@@ Property / describes a project that uses: nuXmv / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mcmt
@@ Property / describes a project that uses: Mcmt / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ByMC
@@ Property / describes a project that uses: ByMC / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-020-09578-5
+Normal rank
@@ Property / OpenAlex ID @@
+W3081978399
@@ Property / OpenAlex ID: W3081978399 / rank @@
+Normal rank
@@ Property / cites work @@
+Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
+Normal rank
@@ Property / cites work @@
+Counting Constraints in Flat Array Fragments
@@ Property / cites work: Counting Constraints in Flat Array Fragments / rank @@
+Normal rank
@@ Property / cites work @@
+Cardinality constraints for arrays (decidability results and applications)
+Normal rank
@@ Property / cites work @@
+Decision procedures for flat array properties
@@ Property / cites work: Decision procedures for flat array properties / rank @@
+Normal rank
@@ Property / cites work @@
+An introduction to mathematical logic and type theory: To truth through proof.
+Normal rank
@@ Property / cites work @@
+Tolerating corrupted communication
@@ Property / cites work: Tolerating corrupted communication / rank @@
+Normal rank
@@ Property / cites work @@
+Asynchronous consensus and broadcast protocols
@@ Property / cites work: Asynchronous consensus and broadcast protocols / rank @@
+Normal rank
@@ Property / cites work @@
+Uniform consensus is harder than consensus
@@ Property / cites work: Uniform consensus is harder than consensus / rank @@
+Normal rank
@@ Property / cites work @@
+The Heard-Of model: computing in distributed systems with benign faults
+Normal rank
@@ Property / cites work @@
+Constraint-based verification of parameterized cache coherence protocols
+Normal rank
@@ Property / cites work @@
+Q4945217
@@ Property / cites work: Q4945217 / rank @@
+Normal rank
@@ Property / cites work @@
+A Logic-Based Framework for Verifying Consensus Algorithms
+Normal rank
@@ Property / cites work @@
+On Verifying Fault Tolerance of Distributed Protocols
+Normal rank
@@ Property / cites work @@
+Predicate abstraction for software verification
@@ Property / cites work: Predicate abstraction for software verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q3543581
@@ Property / cites work: Q3543581 / rank @@
+Normal rank
@@ Property / cites work @@
+Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
+Normal rank
@@ Property / cites work @@
+MCMT: A Model Checker Modulo Theories
@@ Property / cites work: MCMT: A Model Checker Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+On the hardness of failure-sensitive agreement problems.
+Normal rank
@@ Property / cites work @@
+Generalized Property Directed Reachability
@@ Property / cites work: Generalized Property Directed Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
+Normal rank
@@ Property / cites work @@
+What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
+Normal rank
@@ Property / cites work @@
+On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination
@@ Property / cites work: Interpolation and Symbol Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding Boolean algebra with Presburger arithmetic
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3126969
@@ Property / cites work: Q3126969 / rank @@
+Normal rank
@@ Property / cites work @@
+Cutoff bounds for consensus algorithms
@@ Property / cites work: Cutoff bounds for consensus algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Reaching Agreement in the Presence of Faults
@@ Property / cites work: Reaching Agreement in the Presence of Faults / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided quantifier instantiation for synthesis in SMT
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:2031422