Tutorial Speaker
Kenneth McMillan is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research Redmond (USA). He works in formal verification, primarily in model checking for hardware and software. He holds a BS in electrical engineering from the University of Illinois at Urbana (1984), an MS in electrical engineering from Stanford (1986) and a Ph.D. in computer science from Carnegie Mellon (1992). He is the author of the book “Symbolic Model Checking”, and the SMV symbolic model checking system. For his work in model checking, he has received the ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, the Alan Newell award from Carnegie Mellon and the Computer-aided Verification Conference award. He was formerly a member of the technical staff at AT&T Bell Laboratories and a fellow at Cadence research labs.
Abstract
Modern automatic theorem provers such as Z3 or CVC4 are powerful but unpredictable. To get the most out of these tools in practical formal systems development, it is important to understand their strengths and weaknesses, and to plan the development in a way that makes the right division of labor between the human and the automated prover. Ivy is a tool for specifying and implementing distributed protocols that supports this process by providing suitable forms of abstraction and modularity, and by providing actionable feedback when proof obligations fall outside the automated prover’s “comfort zone”.
In this tutorial, we will learn how to use Ivy to develop distributed procotols formally, while minimizing the human proof effort and maximizing the predictability of automated proof. We will illustrate the techniques on very simple protocol examples, and then consider how these techniques can be applied to protocols of more realistic complexity.
Invited Talk
Kedar Namjoshi (Nokia Bell Labs, USA). Modular Verification: Model Checking in Bits and Pieces.
Abstract. State explosion is the fundamental obstacle to automated program verification, especially for concurrent programs. Modular verification methods tackle this problem head-on, by reasoning only about individual processes, abstracting away their interactions with the rest of the system; the intuition being that this drastic abstraction suffices for “loosely coupled” systems. This talk will be on foundational principles for modular verification. I will describe proof rules for modularly establishing safety and liveness properties, automated methods that are derived from those rules, and recently developed notions of localized symmetry and their application to the verification of parameterized systems.
Bio. Kedar Namjoshi is a member of technical staff at Nokia Bell Labs in Murray Hill, NJ. He received his Ph.D. from the University of Texas at Austin with E. Allen Emerson, and the B.Tech. degree from the Indian Institute of Technology, Madras, both in the Computing Sciences. His research interests include program semantics, logics and verification, model checking, static program analysis, distributed computing, and programming methodology.