Charlie Murphy will present his Pre FPO "Relational Verification via Weak Simulation" on Thursday April 7th, 2022 at 2pm in CS 402 and Zoom.

Zoom link: https://princeton.zoom.us/j/93257853666

His committee is as follows:

Aarti Gupta (Reader)

Dave Walker (Examiner)

Lennart Beringer (Reader)

Wyatt Lloyd (Examiner)

Zak Kincaid (Advisor)

All are welcome to attend.

Title: Relational Verification via Weak Simulation

Abstract:

Distributed systems are notoriously hard to get right, even when based on existing protocols. The system implementor needs to worry about faulty nodes, asynchronous and delayed or dropped messages, and global correctness properties. Given this complexity, distributed systems are an attractive target for formal verification; however, direct verification of distributed systems is extremely expensive. As such, there is very little work on formally reasoning about distributed systems. Instead, there has been more work on formally verifying distributed protocols, but there is still a gap between the distributed system and a distributed protocol it is based on.

In this talk, I propose formally verifying that a distributed system correctly implements a distributed protocol. By formally connecting a distributed system to a protocol, the system inherits the correctness properties of the protocol.

This strategy is not new: it’s the method of executable specifications. Executable specifications have long been considered in formally verifying distributed systems; however, existing techniques are unable to handle systems and protocols with infinite state. I propose Contextual Simulation, a relational Hoare logic based on weak simulation for specifying a system implements a protocol. I provide a sound but incomplete set of inference rules for reasoning about contextual simulations. I conclude by presenting simulation synthesis, a semi-algorithm to automatically prove or refute contextual simulations. Simulation synthesis is based on the game semantics of weak simulation (an infinite state infinite duration game). The simulation game is solved by iteratively solving longer finite duration games. When the algorithm terminates, it does so with a winning strategy that (depending on the winning player) either proves or refutes the input contextual simulation.