\(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
type: Item
instance of: scholarly article
title: \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
zbMATH Open document ID: 1380.68279
author: Peng Zhang
published in: Formal Methods in System Design
publication date: 2018-02-14T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68M14
Mathematics Subject Classification ID: 68M15
Mathematics Subject Classification ID: 68W15
zbMATH DE Number: 6838878
zbMATH Keywords: parameterized verification
zbMATH Keywords: bounded model checking
zbMATH Keywords: completeness
zbMATH Keywords: partial orders in distributed systems
zbMATH Keywords: reduction
zbMATH Keywords: fault-tolerant distributed algorithms
zbMATH Keywords: Byzantine faults
cites work: Ivy
cites work: An approach to automating the verification of compact parallel coordination programs. I
cites work: Symbolic Counter Abstraction for Concurrent Software
cites work: Impossibility of distributed consensus with one faulty process
cites work: Decidability of Parameterized Verification
cites work: Asynchronous consensus and broadcast protocols
cites work: Q4778617
cites work: Control and data abstraction: The cornerstones of practical formal verification
cites work: Unreliable failure detectors for reliable distributed systems
cites work: Counterexample-guided abstraction refinement for symbolic model checking
cites work: CONCUR 2004 - Concurrency Theory
cites work: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
cites work: A Logic-Based Framework for Verifying Consensus Algorithms
cites work: On Reasoning About Rings
cites work: Q4417919
cites work: Model checking parameterized asynchronous shared-memory systems
cites work: Inductive data flow graphs
cites work: Proof spaces for unbounded parallelism
cites work: Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
cites work: Q4037382
cites work: Non-blocking atomic commit in asynchronous distributed systems with failure detectors
cites work: Reduction
cites work: Efficient Coverability Analysis by Proof Minimization
cites work: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
cites work: On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
cites work: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
cites work: What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
cites work: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
cites work: Q4414397
cites work: Time, clocks, and the ordering of events in a distributed system
cites work: Automated Technology for Verification and Analysis
cites work: Chapar: certified causally consistent distributed key-value stores
cites work: Q3126969
cites work: Q4804890
cites work: Bosco: One-Step Byzantine Asynchronous Consensus
describes a project that uses: Ivy
describes a project that uses: PSync
describes a project that uses: FAST
describes a project that uses: nuXmv
describes a project that uses: Plingeling
describes a project that uses: IronFleet
describes a project that uses: ByMC
describes a project that uses: Verdi
describes a project that uses: Chapar
describes a project that uses: Lingeling
describes a project that uses: z3
describes a project that uses: Treengeling
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: s10703-017-0297-4
OpenAlex ID: W2747225378
Wikidata QID: Q59607712
DOI: 10.1007/S10703-017-0297-4
description: scientific article; zbMATH DE number 6838878