Replicated Data Types: Specification and Verification
Date and Time: To be Announced
Kartik Nagar
Abstract: Modern decentralized applications often use multiple replicas/copies of data, each of which can be independently operated, to minimize data access latency, provide fault tolerance and improve scalability. Replicated Data Types (RDTs) have emerged as a systematic approach to the problem of ensuring that replicas remain eventually consistent despite concurrent conflicting updates. RDTs provide an elegant solution to the classical problem faced by a distributed system of maintaining an illusion of a centralized system without requiring complete synchronisation. After more than a decade since they were first introduced, RDTs are now widely used in the industry and also remain an active area of research, particularly for the verification problem. In this tutorial, we will first go through the main paradigms of RDT design, namely operation-based CRDT, state-based CRDT and MRDT. We will then focus on the specification and verification problem, going through the two main approaches for specifying correctness of RDTs: an axiomatic, declarative approach, and replication-aware linearizability. Finally, we will present some of our recent work in verifying the correctness of MRDTs targeting both the above forms of specifications.
Bio: Kartik Nagar is an Assistant Professor at Department of CSE, IIT Madras. He completed his PhD from IISc Bangalore, after which he was a postdoc at Purdue University. His research interests are in Automated Formal Verification, Program Analysis and Programming Languages, with emphasis on developing practical verification techniques for concurrent and distributed systems.
Quantitative and Probabilistic Verification, Transformer-style
Date and Time: To be Announced
Benjamin Kaminski
Abstract: Will my program terminate? If initially x == 2, will x be even after program termination? These are qualitative problems in program verification with answers either yes or no, true or false. In this tutorial, we will study how to measure quantities instead of truth: How long will it take until my program terminates? Given the input value, what output value will my program produce? Given an observed output value, what was the input value? Can I answer these questions also if my program had access to randomness?
In this tutorial, we will investigate how to reason about such quantitative properties of software, i.e. typically infinite-state systems described symbolically by some programming language. To that end, we will first study qualitative deductive reasoning via Dijkstra’s weakest [liberal] preconditions and strongest postconditions. We will then gradually lift qualitative to quantitative weakest pre / strongest post transformers. In particular, we will learn how to interpret weakest pre and strongest post meaningfully in a quantitative setting. We will also learn about a concept that Dijkstra missed to investigate (or did not care to investigate): strongest liberal post[conditions]. Finally, we will have a look at weakest pre transformers for probabilistic programs. We will learn how to use these transformers to reason about reachability probabilities and expected values. We will also learn how to adapt the probabilistic weakest pre calculus in order to reason about expected runtimes of probabilistic programs.
Bio: Benjamin Kaminski is a Professor of Computer Science at Saarland University. He received his PhD from RWTH Aachen in 2019, where he worked on semantics and verification of probabilistic programs. His PhD thesis von the 2020 Ackermann Award. His research focuses on quantitative verification, particularly probabilistic programs using quantitative predicate transformers and methods from fixed point theory.