Program

The summer school features distinguished speakers sharing their knowledge of a range of exciting topics. The abstracts of the presentations and the slides can be found below.

  Thu,
July 10		 Fri,
July 11		 Sat,
July 12
8:00 –
8:30		 Registration Registration
(if required)
8:30 –
10:15		 Introduction to SAT
(Daniel Le Berre)		 Introduction to SMT
(Alberto Griggio)		 Interpolation in SAT & SMT
(Philipp Rümmer)
10:45 –
12:30		 Hardware Verification with IC3
(Fabio Somenzi)		 Non-linear Arithmetic in SMT
(Leonardo de Moura)		 Software Verification with IC3
(Nikolaj Bjørner)
14:00 –
15:45		 Practical Session SAT
(Keijo Heljanko, Tomi Janhunen, Tommi Junttila)		 Practical Session SMT
(Keijo Heljanko, Tomi Janhunen, Tommi Junttila)		 SMT for Cryptography & Software Verification
(Chao Wang)
16:15 –
17:30		 Parallel SAT Solving
(Christoph Wintersteiger)		 Proofs in SAT and CSP
(Ofer Strichman)		  
18:30 – Dinner    
19:00-   Banquet

Social Event

The banquet will take place on the evening of the 11th of July in the panorama restaurant of the Liechtensteinhaus. We will hike there together from the hotel (which should take us about an hour), but the restaurant can also be reached by car or taxi if needed. Please bring shoes that are appropriate for hiking, rain-proof gear in case the weather is bad, and a torch/flashlight in case the banquet takes a little bit longer…

Arriving on July 9

For those who are arriving on the evening of July 9, there’s the opportunity to watch the FIFA world cup semi finals at the bar of the hotel.

Speakers and Talks

Introduction to SAT (Daniel Le Berre, Artois University)
(slides)

Daniel Le Berre

Daniel Le Berre

Abstract: This tutorial will provide a description of the SAT problem and its variants (MAXSAT, Pseudo-Boolean Optimization) which can be solved using modern SAT solvers. The main part will focus on the understanding of the various components of the Conflict Driven Clause Learning (CDCL) architecture used in most SAT and SMT solvers nowadays. Advanced features such has UNSAT core computation and incremental SAT will also be covered. The last part of the tutorial will provide some hints about the importance of the encoding when using SAT technology.

Software Verification using IC3 (Nikolaj Bjørner, Microsoft Research)
(slides, technical details)

Nikolaj Bjorner
Nikolaj Bjørner
Abstract: We illustrate symbolic model checking in the light of SMT: as solving satisfiability of universally quantified Horn clauses with constraints.  We show that this format is suitable for representing procedure calls and data-types that are used in programs.  Methods developed in the context of symbolic model checking and automated deduction can be adapted as solvers for these SMT formulas. In this lecture we adapt IC3 for solving constrained Horn clauses. We then include an overview of selected current research around solving constrained Horn clauses.

SAT-based Model Checking (Fabio Somenzi, UC Boulder)
(slides)

Fabio Somenzi
Fabio Somenzi
Abstract: The talk covers SAT-based techniques for finite-state model checking. It provides a detailed introduction to inductive invariants, and incremental algorithms to construct these invariants (the IC3 algorithm).

Introduction to SMT (Alberto Griggio, Fondazione Bruno Kessler)
(slides)

Alberto Griggio
Alberto Griggio
Abstract: The tutorial will provide an introduction to the SMT problem and the main techniques for solving it. We will describe the basic components of modern SMT solvers, their underlying algorithms and relevant implementation aspects, and show how they are used for implementing efficient decision procedures for various theories of practical interest. Most of the focus will be on the DPLL(T) approach to SMT, but we will also briefly look at alternative techniques and current trends.

Practical sessions for SAT and SMT (Keijo Heljanko, Tomi Janhunen, and Tommi Junttila, Aalto University)

Tomi Janhunen

Tomi Janhunen
Keijo Heljanko
Keijo Heljanko

Abstract: The goal of the practical sessions of the summer school is to make students acquainted with one of the state-of-the-art systems for SAT and SMT based modelling, namely Z3 and its Python interface, and provide hands-on modelling experience. Students are provided with exercise problems which are first modeled using SAT/SMT and then submitted for automated evaluation.

Bios: Keijo Heljanko is an Associate Professor at Aalto University, Department of Computer Science and Engineering. His interests include the use of SAT and SMT technology for the model checking and testing of distributed systems, as well as parallelization of applications exploiting SAT and SMT.

Tomi Janhunen is a Senior Lecturer at Aalto University, Department of Information and Computer Science. His interests include, in addition to SAT and SMT, different paradigms for knowledge representation and reasoning such as answer set programming, linear programming etc.

Tommi Junttila is a Lecturer at Aalto University, Department of Information and Computer Science.  His research interests include SAT and SMT techniques as well as their application to model checking and other areas.

Decision methods for nonlinear arithmetic: An introduction (Leonardo de Moura, Microsoft Research)
(slides)

Leonardo de Moura

Leonardo de Moura

Abstract: Decision methods for nonlinear arithmetic are used in the formal verification and analysis of software and cyber-physical systems, computer algebra, and formalized mathematics. In this lecture, we will introduce decision methods for nonlinear arithmetic, and the key ideas behind Gröbner bases, Muchnik sign matrices, Sturm-Tarski based procedures and Cylindrical Algebraic Decomposition. The lecture will presume only a basic grounding in first-order logic.

Interpolation in SAT and SMT (Philipp Rümmer, Uppsala University)
(slides)

philipp_ruemmer
Philipp Rümmer
Abstract: Craig interpolation is a method for computing a specific form of separators for unsatisfiable conjunctions of formulae (or equivalently of valid implications) and has over the last years become a standard technique for solving fixed-point constraints in model checking. After a general introduction to interpolation, and its applications, this tutorial will survey two aspects: (i) generalised forms of interpolation that have been developed to accommodate various applications, and (ii) techniques to guide interpolation procedures, in order to find those solutions of interpolation problems that are likely to lead to rapid convergence of model checking procedures.
Bio: Philipp Rümmer is researcher at Uppsala University, Sweden. His interests include various forms of program verification, deductive verification and model checking, underlying as theorem proving and SMT, and application in the area of Embedded Systems.

Proofs in SAT and CSP (Ofer Strichman, Technion)
(slides)

Ofer Strichman
Ofer Strichman
Abstract: The tutorial will survey key technologies in modern SAT and CSP solving, with an emphasis on producing minimal resolution proofs of unsatisfiability. Small proofs (minimal or not) play a crucial role in a number of applications in formal verification and Mathematical programming. In several of these the objective is to minimize the number of ‘high-level’ constraints (rather than the number of CNF clauses) that constitute a proof. The tutorial will survey these applications and describe how machine-checkable proofs can also be generated by a CSP solver via a representation called ‘signed clauses’.

SMT for Cryptography & Software Verification (Chao Wang, Virginia Tech)
(slides part 1, part 2)

Chao Wang
Chao Wang
Abstract: We will demonstrate the use of SMT solvers in two applications: (1) quantifying power side channel leakage in cryptographic software code, and (2) detecting concurrency bugs in multithreaded programs. In both cases, we will show that a brute force approach of applying the solver does not work well, due to the complexity of the problem and limitations of the solver. Then, we will present a set of pragmatic strategies that can make the SMT based approach effective and scalable for practical use.

Bio: Chao Wang is an Assistant Professor in the Bradley Department of Electrical and Computer Engineering at Virginia Tech. He is interested using SAT and SMT solvers in the verification of cryptographic software and concurrent software.

Parallel SAT Solving (Christoph Wintersteiger, Microsoft Research Cambridge)
(slides)

christoph
Christoph Wintersteiger
Abstract: In this tutorial we provide a survey of the state of the art in parallel SAT solving. We will investigate traditional divide-and-conquer approaches, guiding-path-based solvers, portfolio-based solvers, as well as decomposition based techniques. We will take a look at the performance of each of those techniques in theory and in practice, and at the various heuristics that are at play. Finally, we discuss current research problems and directions in this area.
Bio: Christoph M. Wintersteiger is a researcher at Microsoft Research. His interests include satisfiability problems of all kinds, decision procedures, automated verification, model checking, and applications thereof in all areas.

Posters from participants