Please use this identifier to cite or link to this item:
http://arks.princeton.edu/ark:/88435/dsp01pv63g3494
Title: | Relational Verification of Distributed Systems via Weak Simulations |
Authors: | Murphy, Timothy Charles |
Advisors: | Kincaid, Zachary |
Contributors: | Computer Science Department |
Keywords: | Automated Reasoning Game Semantics Logic Simulation Synthesis Verification |
Subjects: | Computer science |
Issue Date: | 2023 |
Publisher: | Princeton, NJ : Princeton University |
Abstract: | Distributed systems are notoriously hard to get right, even when based on existing protocols. This thesis explores the use of executable specifications for (semi-) automatic verification of distributed systems. Rather than proving a distributed system is correct with respect to a given temporal property, this thesis proposes instead verifying a distributed system implements a given distributed protocol via per-node simulation. To prove a distributed system implements a protocol this thesis defines (1) contextual simulation logic, (2) simulation synthesis, and (3) fine-grained strategy improvement. Contextual simulation logic is a relational Hoare logic that consists of a judgement called contextual simulation and a set of inference rules to prove a contextual simulation valid. A contextual simulation relates an implementation program to a specification program via divergence preserving weak simulation. The set of rules are defined using the structure of both programs and used to align the implementation and specification programs. Simulation synthesis is a semi-algorithm that may prove or refute the validity of a (per-node) contextual simulation. Simulation synthesis is based on the game semantics of contextual simulation. Simulation synthesis will (1) construct a complete well-labeled simulation unwinding (a finite representation of a winning strategy proving the validity of a contextual simulation), (2) a counter-strategy to simulation of finite duration (a winning strategy refuting the validity of a contextual simulation), or (3) diverge. To solve a simulation game---an infinite state game of infinite duration---simulation synthesis incrementally expands and solves a finite-horizon of the game. Finite-horizon games are solved by reduction to satisfiability of quantified linear integer arithmetic (LIA) formulas. Further, this thesis develops fine-grained strategy improvement a decision procedure for proving (or refuting) satisfiability of quantified LIA formulas based on the game-semantics of LIA formulas. This procedure produces a certificate (a winning strategy proving or refuting) satisfiability of a LIA Formula. This certificate is used to construct the (winning) strategy for the finite-horizon game. |
URI: | http://arks.princeton.edu/ark:/88435/dsp01pv63g3494 |
Type of Material: | Academic dissertations (Ph.D.) |
Language: | en |
Appears in Collections: | Computer Science |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Murphy_princeton_0181D_14432.pdf | 976.07 kB | Adobe PDF | View/Download |
Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.