[madPL] 1/30 1st PL Seminar of the Semester, plus sign-up link

[LAUREN MARIE NEUDORF <lneudorf@xxxxxxxx>]

Hello Everyone!

Hello everyone! Hope the first day of classes is going well! Our first seminar will be this Monday 1/30, at 1:05pm in room 3310. Charlie Murphy will be presenting on âRelational Verification via Weak Simulationâ You can read the abstract below. Hope to see everyone there! 

Additionally, please sign up to present at a seminar using this google sheet, under the tab "Spring". 

https://docs.google.com/spreadsheets/d/1bw4XnEWC4XdGns9eLpClUpxmc__IXzGCTA_PKYxq_TU/edit?usp=sharing

Google Sheets: Sign-in

Access Google Sheets with a personal Google account or Google Workspace account (for business use).

docs.google.com

î

î

î

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 I present (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 counterstrategy 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, I develop 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.

Best,

Lauren Neudorf

Program Manager, MadPL Research Group

University of Wisconsin-Madison

Department of Computer Sciencesâ

(716) 704-4463

(she/her/hers)