FRIDA 2025
who it's for
distributed-systems researchers, formal verification engineers, protocol designers, blockchain protocol researchers, network operators and network verification engineers, program analysis and tool developers
topics
asymmetric quorum systems; game-theoretic security to SMT over reals; stochastic committee selection with random beacons; MSO over finite execution histories (MONA); delaying-the-future theorem for happens-before and TSO; ghost outputs and strong refinement for binding; MPLS label-stack reachability and failover synthesis; round-bounded reduction for parameterized verification; dependency-graph criterion for linearizability; reliable-broadcast depth metric
| title | author | length |
|---|---|---|
| What properties should asymmetric quorum systems satisfy? | Juan Villacis | 34m |
Shows that asymmetric quorum systems collapse to symmetric ones in the crash-fault model by transforming any asymmetric collection into an equivalent symmetric… | ||
| Automated game-theoretic security analysis of blockchain protocols | Ivana Bocevska | 24m |
Presents an automated pipeline that reduces game-theoretic security to SMT over real arithmetic, encodes incentive-compatibility and Byzantine-tolerance as… | ||
| Stochastic reasoning in decentralised systems | Bill Roscoe | 42m |
Argues that choosing committees by a fair beacon with ε = 10⁻¹⁸ per trial yields one billion trials → δ ≈ 10⁻⁹ overall, enabling deterministic reasoning about… | ||
| Automated reasoning on consistency models with MONA | Isabelle Coget | 22m |
Claim: satisfiability of MSO over finite execution histories is decidable and can be checked by translating histories into MONA’s finite-word MSO… | ||
| The delaying the future approach | Raissa Nataf | 40m |
Defines a concrete Delaying the Future theorem that lets a run be transformed by postponing every event outside the past of a chosen cut by delta while… | ||
| Specifying binding and commitment with ghost outputs and strong refinement | Hagit Attiya | 39m |
Argues that hyperproperties like binding and commitment become checkable by adding ghost outputs to module interfaces and proving strong refinement… | ||
| Synthesis of dependable and self-driving communication networks | Stefan Schmid | 29m |
Claim: polynomial-time verification of MPLS label-stack reachability lets the tool check reachability and waypoint compliance under failures by modeling… | ||
| Reduction theorems for effective parameterized verification of round- based distributed algorithms | Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin | 54m |
Presents reduction theorems that collapse the unbounded round dimension into a bounded sliding window (if round jumps are bounded by B) and encode anonymous… | ||
| Proving linearizability of fault-tolerant register protocols: dependency graph approach | Gregory Chockler | 41m |
Framework claims a concrete, automatable criterion: build a per-execution dependency graph as the union of four relations (real-time, write-write total order… | ||
| nothing matches | ||