Professor Ilya Sergey, a lecturer in computer science at University College London in the UK was on campus Friday, August 11, to give a talk in the CSE department. Sergey is a member of the UCL Computer Science Department's Programming Principles, Logic and Verification group. The talk on "Dependent Types for Compositional Verification of Distributed Systems" reflected joint work by Sergey with University of Washington professor (and CSE alumnus) Zachary Tatlock (Ph.D. '14) and Tatlock's Ph.D. student at UW,. James R. Wilcox.
University College London
In his talk, Sergey presented Disel, the first framework for implementation and compositional verification of distributed systems and their clients, all within the mechanized and foundational context of the Coq proof assistant.
According to Sergey's abstract, Disel users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details.
By virtue of Disel's dependent type system, well-typed implementations always satisfy their protocols' invariants and never go wrong, allowing users to verify system implementations interactively using Disel's Hoare-style program logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting.
In May, Sergey, Tatlock and Wilcox presented a paper on "Programming Language Abstractions for Modularly Verified Distributed Systems" at the 2nd Summit on Advances in Programming Languages (SNAPL 2017).