- Parosh Aziz Abdulla, Uppsala University
- Jasmin Blanchette, LMU Munich
- Byron Cook, Amazon Web Services
- Javier Esparza, Technical University of Munich
- Jan Kretinsky, Technical University of Munich
- Anca Muscholl, University of Bordeaux
- Aleksandar Nanevski, IMDEA Software Institute
- Corina Pasareanu, NASA Ames
- Grigore Rosu, University of Illinois at Urbana-Champaign
- James Worrell, Oxford University
- Hongseok Yang, KAIST
Algorithmic Verification of Infinite-State Systems
Speaker: Parosh Aziz Abdulla
Abstract: Some of the most notable advances in automated (algorithmic) verification during the last three decades have been achieved in the context of finite-state systems. This success has been mainly due to the invention of model checking. The size and complexity of applications that can be handled have increased rapidly through integration with symbolic techniques such as BDDs, and (more recently) using SAT-solvers. While the above frameworks are well suited for reasoning about finite abstractions of system behaviors, several system features cannot be modeled faithfully without the use of infinite state spaces; examples of such features include variables ranging over unbounded domains, unbounded communication media, timing constraints, dynamic process creation, parameterization (systems with unbounded numbers of components), multi-threading, dynamically allocated data structures, and weak memory models. In the lectures, I will describe some prominent frameworks for dealing with infinite-state systems, including abstraction techniques, partial-order methods, bounded context-switching, and well-structured systems. In addition, I will illustrate such techniques' applicability to areas such as distributed systems, communication protocols, parameterized systems, event-driven programs, and programs running on weakly consistent platforms.
Provers and Solvers
Speaker: Jasmin Blanchette
Abstract: Automatic theorem provers are used as backends to various verification tools, including proof assistants. They quickly discharge proof obligations that would take several minutes, sometimes hours for humans to discharge manually. In the lectures, I will present an abstract, mathematical view of how the main automatic theorem proving techniques work, including resolution, superposition, lambda-superposition, SAT/SMT solving, and AVATAR. Resolution and superposition are the leading methods for reasoning about classical first-order logic. Lambda-superposition (developed by my team) is an extension to higher-order logic. SAT solvers are useful to reason efficiently about finite problems. SMT solvers combine SAT with decision procedures for arithmetic and other theories. Finally, the AVATAR architecture extends a superposition prover with a SAT/SMT solver, combining the strengths of both kinds of systems.
Speaker: Byron Cook
Interactive Proof Systems: From Theory to Practice
Speaker: Javier Esparza
Abstract: Interactive protocols between a prover and a verifier (also known as interactive proof systems) are a well-known tool of complexity theory. In this course we show that they can be used in practice to certify the correctness of automated reasoning tools.
Theoretically, interactive protocols exist for all PSPACE problems. The verifier of a protocol checks the prover's answer to a problem instance in polynomial time, with polynomially many bits of communication, and with exponentially small probability of error. (The prover may need exponential time.) However, existing interactive protocols are not used in practice because their provers use naive algorithms, inefficient even for small instances, that are incompatible with practical implementations of automated reasoning.
The goal of the course is to present a novel interactive protocol for QBF whose prover uses binary decision diagrams (BDDs). The prover has only a linear overhead in computation time over the natural algorithm. After an introduction to QBF, BDDs, and interactive protocols, the protocol is presented and its performance on standard QBF benchmarks is discussed.
Learning-aided probabilistic verification and synthesis
Speaker: Jan Kretinsky
Abstract: This course provides a tutorial on analysis of basic probabilistic models
such as Markov chains, Markov decision processes, and stochastic games.
These are classical models for applications ranging from decision making
under uncertainty (as in AI or game theory), to reliability analysis (e.g.,
of network protocols or power plants), to design of biochemical
experiments, to synthesis of controllers (of embedded and cyber-physical
Verification aims at reliable analysis of these models with respect to different properties. For instance, qualitative properties such as "Is a given state reached with probability 1?" or quantitative questions such as "What is the probability that a given logical specification is satisfied?" or synthesis questions such as "What is the optimal resolution of decisions in order to maximize the frequency of visiting a given state?" The lectures will focus on the algorithmic aspects of the analysis, in particular on graph-based and numerical algorithms rather than on probability theory. This includes classical algorithms such as the attractor construction, linear programming, dynamic programming (value iteration, policy iteration), which relate to approximate dynamic programming, reinforcement learning, or probabilistic planning. Besides, we discuss recent results on the reliability of these algorithms. We shall cover the whole spectrum of results: from the theoretical computational complexity over the mentioned algorithms to their practical properties and recent heuristics combining rigorous mathematical guarantees and practical efficiency of machine learning.
Distributed synthesis and control
Speaker: Anca Muscholl
Abstract: The goal of automated synthesis is to design a program that complies with a given logical specification, and reactive synthesis addresses this question in the setting where programs interact with their environment. This lecture will mainly address the synthesis problem for concurrent programs. After a general introduction to synthesis and games we will consider reactive distributed synthesis in various models. Although the problem turns out to be undecidable for most synchronisation paradigms, we will show some realistic restrictions where distributed synthesis is decidable, and even with reasonable complexity. One such setting are lock-sharing programs, where processes synchronise by using locks from a common pool.
Type and Proof Structures for Concurrent Programs
Speaker: Aleksandar Nanevski
Abstract: The main challenge of software verification in general, and of
concurrent software verification in particular, has always been in
achieving modularity, i.e., the ability to divide and conquer the
correctness proofs with the goal of scaling the verification effort.
Types are a formal method well-known for its ability to modularize
programs, and in the case of dependent types, the ability to modularize
and scale mathematical proofs as well.
This series of lectures presents ongoingwork towards reconciling dependent types with state and shared memory concurrency, with the goal of achieving modular proofs. Applying the type-theoretic paradigm permits a view of separation logic as a form of type theory for state. When scaling to concurrency, this view leads to a new notion of ramified framing. Furthermore, it motivates novel abstractions for programs and proofs based on the algebraic structure of concurrent resources, and structure-preserving functions (i.e., morphisms) between resources.
Symbolic Execution and Quantitative Reasoning: Applications to Software Safety and Security
Speaker: Corina Pasareanu
Abstract: In the lectures I will describe symbolic execution, a systematic program analysis technique which explores multiple program behaviors by solving symbolic constraints collected from conditions in the program. The obtained solutions can be used as test inputs that execute feasible program paths. Symbolic execution has been used to uncover subtle errors and unknown vulnerabilities in many software systems. Furthermore, symbolic execution has been extended with probabilistic reasoning enabling quantitative analysis of programs. This probabilistic information can be used for example to compute the reliability of a controller under different environment conditions or to quantify information leakage in a program. I will also review newer applications of symbolic execution and its probabilistic extension, including the analysis of machine learning models, with respect to safety, robustness, and fairness properties.
Designing and verifying programming languages using formal executable semantics
Speaker: Grigore Rosu
Orbit problems for dynamical systems
Speaker: James Worrell
Abstract: The course consists of a brief tour around decision problems for dynamical systems that often arise in research on automata, formal language theory, model checking, and control theory. We will focus on several fundamental open problems, survey the history of the problems and describe the state of the art in terms of decidability, we will introduce relevant mathematical techniques, and finally we will highlight the obstacles to further progress. We will start by explaining the relevance of these open problems to the above-mentioned application areas of computer science. The course will consist of four parts:
- Linear recurrence sequences and the Skolem Problem
- The Skolem and Positivity problems for Polynomial recurrence sequences
- Computing polynomial invariants on dynamical systems
- Sturmian sequences and transcendence.
Speaker: Hongseok Yang
Abstract: Probabilistic programming refers to the idea of developing a programming
language for writing and reasoning about probabilistic models from machine
learning and statistics. Such a language comes with the implementation of
several generic inference algorithms that answer various queries about the
models written in the language, such as posterior inference and
marginalisation. By providing these algorithms, a probabilistic programming
language enables data scientists to focus on designing good models based on
their domain knowledge, instead of building effective inference engines for
their models, a task that typically requires expertise in machine learning,
statistics and systems. Even experts in machine learning and statistics may
benefit from such a probabilistic programming system because using the
system they can easily explore highly advanced models.
This course has two goals. The first is to help students to be a good user of an expressive probabilistic programming language. Throughout the course, we will use a particular language, either Anglican or Pyro, but we will emphasise general principles that apply to a wide range of existing probabilistic programming systems. The second goal is to expose the students to recent exciting results in probabilistic programming, which come from machine learning, statistics, programming languages, and probability theory.