MOD23
Speakers
- 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
Program
The schedule for the summer school can be found here.Lectures
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.
Material: The material and slides to the course can be found here.
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.
Material:
Reasoning about, and in, the cloud
Speaker: Byron Cook
Abstract: These lectures will describe methods used at Amazon to reason about the security, safety, and durability of AWS services. The lectures will also discuss methods of using the cloud itself to scale automated reasoning tools.
Material:
Lecture 1:
Lecture 2:
Lecture 3:
Lecture 4:
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.
Material:
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
systems).
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.
Material:
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.
Material:
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.
Material:
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.
Material:
Matching Logic - A Minimal Foundation for Programming Languages
Speaker: Grigore Rosu
Abstract: Matching logic is a logical foundation for programming languages. It was initially designed as a foundation for the K Framework, which is used to formally define programming language semantics. Once a programming language is semantically defined, the K Framework offers a suite of tools specialized for that language, which are correct by construction: interpreters, compilers, model checkers, symbolic execution engines, and even full-fledged deductive verifiers. Matching logic allows the programming language semantics to be regarded as a mathematical theory, and all the tasks performed by the various K tools as deriving theorems. Minimality of the logic was an important design factor, because we want it to be eventually implemented as a circuit (in zero-knowledge or hardware or both). Because of its minimality and expressiveness, matching logic can also serve as a foundation to other similar programming language or interactive proving frameworks. In this lecture series I will focus on the basics of matching logic and how it serves as a foundation to K, but interested students are welcome to consult http://www.matching-logic.org for further reading and to contact us for discussions or collaborations.
Material:
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.
Material:
Probabilistic Programming
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.
Material:
Imprint