Spring School 2016

RiSE & LogiCS Spring School on Logic and Verification

The Spring School is targeted at master’s and doctoral students in in Computer Science and Mathematics with a strong interest in Logic and Automated Verification. We particularly encourage members of the ExCape and RiSE research networks, and the LogiCS doctoral college, but the event is open to all interested students.

Dates and Location

Dates: Friday, April 15 to Sunday, April 17, 2016
Venue: TU Wien
Freihaus building (find on OpenStreetMap)
Wiedner Hauptstraße 8-10, 1040 Wien
Zeichensaal 3, green area, 7th floor (map)


The registration is now closed.

Helmut Veith, 1971-2016

With the deepest sadness, we announce the passing of Helmut Veith on March 12, 2016. A collection of obituaries can be found here. Helmut’s lectures will be given by Igor Konnov and Josef Widder.

Program and Schedule

April 15
April 16
April 17
9:00 –
Formal Inductive Synthesis: Theory and Applications
(Sanjit Seshia, Berkeley)
First-Order Theorem Proving and Vampire
(Laura Kovács, Martin Suda, TU Wien)
Verifying Distributed Algorithms
(Igor Konnov, Josef Widder, TU Wien)
10:30 –
Coffee Coffee Coffee
11:00 –
Formal Inductive Synthesis: Theory and Applications
(Sanjit Seshia, Berkeley)
First-Order Theorem Proving and Vampire
(Laura Kovács, Martin Suda, TU Wien)
Verifying Distributed Algorithms
(Igor Konnov, Josef Widder, TU Wien)
12:30 –
Lunch break Lunch break
14:00 –
SMT Solvers
(Martina Seidl, JKU Linz)
First-Order Theorem Proving and Vampire
(Laura Kovács, Martin Suda, TU Wien)
Introduction to Distributed Algorithms
(Josef Widder, TU Wien)
16:00 –
Coffee Coffee
16:30 –
SMT Solvers
(Martina Seidl, JKU Linz)
Presentations by VCLA Award Winners
19:00- Dinner
(12 Apostelkeller)

Travel & Travel Support

Participants who are registered for CPSWeek are encouraged to apply for student travel support. Please be aware that the deadline for this application is March 11, 2016.

If traveling from abroad, we recommend to arrive at Vienna International Airport (VIE).
If you arrive at the airport, the train station Wien Mitte/Landstrasse can be reached by the suburban train (S7 direction Floridsdorf). Avoid the CAT, since it is overpriced. From Wien Mitte, the subway U4 takes you to Karlsplatz, where the main building of TU Wien and Freihaus are located.


There is a range of affordable hotels in Vienna, such as the IBIS Budget Sankt Marx and Wien Messe. More suggestions can also be found on the CPSWeek webpage.

Social Dinner

The dinner is going to take place at the 12 Apostelkeller (Sonnenfelsgasse 3 in the first district of Vienna). We will walk there together from Freihaus after the VCLA Award Talks in Saturday. There will be vegetarian food as well as chicken and pork – please let us know if you have any other dietary restrictions.

The catering (coffee and lunches) during the Spring School is provided by Michl’s, which is part of wienwork, an organization providing jobs for people with disabilities and persons experiencing disadvantages on the labor market.

Abstracts of Talks

As practical exercises will be part of some lectures, we ask all participants to bring laptops.

Title: Formal Inductive Synthesis: Theory and Applications
Speaker: Sanjit Seshia (U. Berkeley)
Sanjit Seshia
Abstract: Formal inductive synthesis refers to the synthesis of artifacts from examples/observations so as to satisfy a formal specification. In this lecture, we will study a theory of formal inductive synthesis and its applications to the specification, verification, and design of systems, with a particular focus on cyber-physical systems.
Slides: Formal Inductive Synthesis

Title: SMT Solvers
Speakers: Martina Seidl (JKU Linz)
Martina Seidl
Abstract: SMT (Satisfiabiliy Modulo Theories) is the meeting point of SAT and first-order: by customizing the inevitable trade-off between efficiency and expressiveness, SMT is widely applied in many (industrial) applications.

In this tutorial we will introduce the basic principles of state-of-the-art SMT solving and we will show concrete SMT encodings using the standardized language SMTLib 2.

In particular, we will discuss the successful DPLL(T) approach and its relation to SAT solving. Then we will give an overview of reasoning with popular theories such as uninterpreted functions with equality, arithmetic, bitvectors, and arrays as well as the combination of different theories.

Various application problems will be encoded and solved using these theories illustrating how SMT can be practically used.

Slides: SMT Tutorial, examples

Title: First-order Theorem Proving and Vampire
Speakers: Laura Kovács and Martin Suda (Chalmers/TU Wien)
Laura Kovacs Martin Suda
Abstract: In this tutorial we give a short introduction in first-order theorem proving and the use of the theorem prover Vampire.

We will discuss the resolution and superposition calculus, introduce the saturation principle, present various algorithms implementing redundancy elimination, preprocessing and clause form transformation and demonstrate how these concepts are implemented in Vampire.

We will also present more advanced features of first-order theorem proving. Some of these features are implemented only in the Vampire prover. This includes reasoning with theories, such as arithmetic, Craig interpolation, and an original technique of symbol elimination, which allows one to automatically discover invariants in programs with loops.

All the introduced concepts will be illustrated by running the first-order theorem prover Vampire.

Material: Slides, Vampire binaries, slides for practical

Title: Verifying Distributed Algorithms
Speakers: Igor Konnov and Josef Widder (TU Wien)
Igor Konnov Josef Widder
Abstract: Fault-tolerant distributed algorithms provide a system designer with a mechanism for constructing reliable computing systems. In the first lecture, we introduce basic notions such as timing assumptions, fault assumptions, and classic problems in this area. By reviewing classic paper & pencil correctness arguments, we motivate the use of automated verification methods such as model checking.

The first step towards automated verification is adequate modeling. Thus, we start the second lecture with explaining how to encode the semantics of fault-tolerant distributed algorithms in Promela, the input language of the Spin model checker. Then we introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA): FTDAs are parameterized by both the number of processes and the assumed maximum number of faults. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking.

Unfortunately, counter abstraction can be used for parameterized model checking only if the number of local states of the concurrent processes is small. Consequently, it does not scale to state-of-the-art FTDAs. Hence, in the third lecture we introduce a more efficient approach that does not use abstract counters. Rather, counter values are encoded in SMT, and we show that SMT-based bounded model checking can be used as a sound and complete method for parameterized verification of safety and liveness of FTDAs.

Slides: part 1, part 2, part 3
Title: VCLA International Student Awards
VCLA Award
Speakers: Felix Dörre (Karlsruhe Institute of Technology), Valeria Vignudelli (University of Bologna), Maximilian Schleich (Oxford University)
About: The VCLA International Student Awards are awarded by the Vienna Center for Logic and Algorithms to the authors of outstanding scientific works in the field of Logic and Computer Science, in particular in the areas Databases and Artificial Intelligence, Verification, and Computational Logic. This year’s winners are going to talk about their work on the Verification of Random Number Generators, The Discriminating Power of Higher-Order Languages: A Process Algebraic Approach, and Learning Regression Models over Factorised Joins.
Slides: Verification of Random Number Generators, The Discriminating Power of Higher Order Languages, Learning Linear Regression Models


If you have questions, please contact Georg Weissenbacher (ta.etysrofnull@bnessiew).

Related Events

CPSWeek 2016 takes place in Vienna from April 11-14.

Support and Sponsors

This event is supported by the Center for Computer Science (Zentrum für Informatikforschung), the RiSE Research Network, the LogiCS Doctoral College, the Vienna Center for Logics and Algorithms, Informatik Austria, and the Austrian Ministry for Transport, Innovation and Technology.

BMVITVCLAInformatik AustriaLogo ARiSEDoctoral Program LogiCS


We thank Andreas Fellner, Adrian Rebola Pardo, Matthias Schlaipfer, and Mitra Tabaei Befrouei for their help with the organization of the spring school, as well as our speakers for their great presentations. All photos courtesy of Matthias Schlaipfer.

Latest News

Jens Pagel wins Bill McCune PhD Award

We congratulate Jens Pagel for receiving the 2021 Bill McCune PhD Award in Automated Reasoning! Jens graduated in 2020; his thesis on Decision procedures for separation logic: beyond symbolic heaps (supervised by Florian Zuleger) presents his substantial contributions to the theory of formal verification and automated reasoning, and to verifying heap-manipulating programs in particular.

Continue reading

Full news archive