Group meeting schedule

The regular group meetings take place every first Wednesday of the month between 11:00 and 12:30 c.t. in Seminarraum Menger. They are not supposed to look like this:

Sign up for future (regular) group meeting talks here:

Month Speaker Notes
March 2020 Adrian
April 2020 Petra, Jure
May 2020 Sarah, Pamina
June 2020 Jakob
July 2020 Miroslav
August 2020
September 2020 Thomas, Vedran
October 2020 Friedrich
November 2020 Thanh-Hai
December 2020

Please send a title and abstract to 1-2 weeks before your talk.


Planning for 2020:

Date Topic Presenters Notes
Apr 8 Type inference in TLA+ Jure Kukovec
Online, Zoom meeting ID: 510 629 442
Mar 4 Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs Adrian Rebola Pardo
Feb 12 Misc. N/A No speaker
Jan 15 Misc. N/A
No speaker


Planning for 2019:

Date Topic Presenters Notes
Dec 4 Probabilistic Programming: Machine Learning for the Masses? Joost-Pieter Katoen in Kontaktraum, Gußhaustrasse 27-29, 6th floor
Nov 20 Quantum Algorithms Hanna Lachnitt
in von Neumann
Oct 16 TLA+ Model Checking Made Symbolic Thanh-Hai Tran
Sep 16 TBA Tanja Schindler
Sep 11 Mutation Testing with Hyperproperties Andreas Feller
May 22 Attacks against Neural Networks Martin Matak In Seminarraum 183/2 (1st floor)
Apr 17 Lonely Points in Simplices Maximilian Jaroschek  
Apr 3 Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking Ilina Stoilkovska  
Mar 19 Effective Entailment Checking for Separation Logic with Inductive Definitions Jens Katelaan
Jan 29 Unfolding Based Test Case Generation Andreas Fellner
Jan 22 Data Race Detection for Industry-Scale OpenMP Applications Zvonimir Rakamarić


Planning for 2018:

Date Topic Presenters Notes
Dec 18 Deciding affine formula equations for finding loop invariants Sebastian Zivota
Nov 27 Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs Klaus von Gleissenthal
Nov 20 Probabilistic model checking for UAV strategy generation Alice Miller  In Seminarraum 188/2 (4th floor)
Nov 6 Analysis and Synthesis of Floating-Point Routines Zvonimir Rakamarić
Oct 23 Towards Robust and Flexible Intermediate Program Verification Yu-Ting (Jeff) Chen
Oct 23 Complete and Efficient DRAT checking Adrian Rebola Pardo
Oct 16 Using Loop Bound Analysis For Invariant Generation Pavel Čadek
Sep 18 Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms Thomas Pani
July 11 Efficient translation of sequent calculus proofs into natural deduction proofs Matthias Schlaipfer
Jun 27 A Separation Logic with Data: Small Models and Automation Jens Katelaan
Jun 20 Two Flavors of DRAT Adrian Rebola Pardo
Jun 13 Local Soundness for QBF Calculi Martin Suda
Apr 18 Iterative Model Checking for Iteratively Relaxed Scheduling Patrick Metzler
Mar 7 Systematic Study of Variable Roles and their Use in Software Verification Yulia Demyanova
Feb 27 Etherium & Smart Contracts Clara Schneidewind Starts at 13:00
Feb 13 Optimizing Big-Data Queries Using Program Synthesis Matthias Schlaipfer
Jan 16 Synthesis of Distributed Algorithms with Parameterized Thresholds Guards Marijana Lazić

Planning for 2017:

Date Topic Presenters Notes
Dec 12 Iteratively-Relaxed Scheduling Patrick Metzler  Guest
Dec 5 Interference Semantics Adrian Rebola Pardo  In von Neumann
Nov 22 Decidable Logics for Path Feasibility of Programs with Strings Anthony Widjaja Lin  Visiting professor, attendance highly desirable
Nov 7 Testing Hyperproperties Andreas Fellner
Oct 24 Reachability in Parameterized Systems: All Flavors of Threshold Automata Jure Kukovec
Sep 26 FMCAD Volunteers should attend
Sep 5 Misc.
July 18 Testing a Saturation-Based Theorem Prover: Experiences and Challenges Martin Suda Starts at 10:30
Jun 13 A Framework for Automated Verification of Synchronous Fault-Tolerant Distributed Algorithms Ilina Stoilkovska
May 9 Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic Jens Katelaan
March 21 Partial Order Reduction Literature Overview Andreas Fellner
February 14

Planning for 2016:

Date Topic Presenters
Oct 25 Error Invariants for Concurrent Traces Mitra Tabaei
Oct 18 Query Optimization Using Program Synthesis Matthias Schlaipfer
Oct 11 Tighter Loop Bound Analysis Pavel Cadek
Aug 11  SMT-based Software Model Checking: Configurable Implementation and Experimental Comparison of Four Algorithms  Matthias Dangl
Aug 9 15:45 Interpolants from SAT solving certificates  Adrian
June 7 User-guided predicate abstraction for TLA+ Thanh Hai
May 31 <Menger not available>
May 24 Generalizing Threshold Automata for Reachability in Parameterized Systems Jure Kukovec (Ljubljana)
May 17 Logical Reasoning about Dynamic Memory: A Survey Jens Katelaan
May 10 Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Safety & Liveness  Marijana
May 3
Apr 26
Apr 19
 Apr 12 (2pm)  Desingularization of Linear Difference Systems Max Jaroschek
Mar 22 Logical Modeling and Analysis of Distributed Algorithms Marijana
Mar 14 Model Based Mutation Testing Andreas Fellner
Feb 23 Verification of Asynchronous Mobile-Robots in Partially-Known Environments Benjamin Aminof
Feb 16 RiSE Keren Censor-Hillel
Feb 9 Abstraction-driven Concolic Testing Przemyslaw Daca
Feb 2 From subexponentials in linear logic to concurrent programming and back Carlos Olarte
Jan 26 Network Verification with Z3 Matthias & Henning
Jan 19 Clausal proof systems for SAT Solving Adrian Rebola
Jan 12 Organizational Helmut

Date  Topic  Presenters
Nov 27
Verification of Parameterized BIP Wang Qiang (EPFL)
Nov 17 IC3 for Parallel Software Henning
Nov 10
Nov 3 Proving Safety with Acceleration and BMC Georg
Oct 27  Language-based Security meets Verification Stefan Brunthaler  (SBA)
Jun 23 Parameterized Model Checking of Fault-tolerant Distributed Algorithms Annu
Jun 9 Extending ALCQIO with Trees Tomer
May 5 — AVM —
Apr 29
Explaining Concurrency Bugs with Interpolants Mitra
Apr 21 Empirical Software Metrics for Benchmarking of Verification Tools Thomas/Yulia
Apr 14 — ETAPS —
Apr 7 — holiday —
Mar 24 On terms in 3-supernilpotent groups with an additional unary operation Marijana
Mar 10 From winning strategy to Nash equilibrium Stephane Le Roux
Mar 3 Generating Feedback for Introductory Programming Assignments Using Repair Against Specifications Ivan
Feb 24 Invariant Analysis and Bound Analysis: Better Together Moritz
Feb 17 Abstraction and Mining of Traces to Explain Concurrency Bugs Mitra
Feb 10 Partial-Order Reduction for Multi-Core LTL Model Checking Alfons

The topics for fall 2014 are:

Date Topic Presenters
Oct 21  no meeting
Oct 28 reading group
Nov 4  practice talks
Nov 11 Hike?
Nov 18 reading group
Nov 25 Azadeh
Dec 2 reading group
Dec 9 business meeting
Dec 16 no meeting (WWTF proposals)

The former topics were

Date Topic Presenters
June 24 Igor
June 17 Florian
June 10 The first attempts at practical DQBF solving Gergely
June 3 A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis Moritz
May 27 Shape and Content: Incorporating Domain Knowledge into Shape Analysis Tomer
May 20 Feedback Generation for Performance Problems in Introductory Programming Assignments Ivan
Apr 1 First Cycle Games Sasha
Mar 25
Mar 18
Mar 11 === no meeting ===
Mar 4 Raphael Löffler
Feb 25 SAT subsumption Matthias Schlaipfer
Feb 18
Feb 11 Business meeting

IC3 software model checking



Date Topic Presenters
Oct 1st, 2013 Previous research Gergely
Oct 8, 2013 Business meeting
Oct 15, 2013 FMCAD practice talk Igor
Nov 5, 2013 ???Plan WWTF meeting Ivanall
Nov 12, 2013 ??? Moritz
Nov 19, 2013 RiSE meeting
Nov 26, 2013 Business meeting
Dec 3, 2013 ??? Francesco
Dec 10, 2013 Helmut un Graz
Dec 17, 2013 Biology Yulia
Jan 14, 2013 Master’s thesis Thomas
Jan 21, 2013 ongoing research Igor, Josef
Date Topic Presenters
Feb 26, 2013 Ivan, Florian
Mar 5, 2013 Henning
Mar 12, 2013 Information Reuse for Multi-goal Reachability Analyses (ETAPS practice talk) Andreas
Mar 19, 2013 ===== no meeting =====
Mar 26, 2013 ===== no meeting =====
Apr 2, 2013 ===== no meeting =====
Apr 9, 2013 Business meeting all
April 16, 2013 Coverage measurement for concurrent programms Daniel
April 23, 2013 formal models for the verification of Cloud infrastructures Soodeh
April 30, 2013 Variable roles Julia
May 7, 2013 Classifying loops Thomas
May 14, 2013 Tree interpolation (in Vampire) Bernhard
May 21, 2013
May 28, 2013 Doron Peled guest
June 4, 2013 Christoph Weidenbach guest
Monday, June 10
Monday, June 17 PhD defense (dress) rehersal Andreas
Monday, June 24 Spin practice talk Mitra
July 2 Content-aware verification of programs with mutable memory Tomer

Reading Group

The reading group will be held every Thursday (either noon or 2pm) in the Menger meeting room.

Here’s the list of papers:

Date Topic Moderator
Sept 5 Dynamic Partial Order Reduction for Model Checking Software Mitra Tabaei
Sept 12 On Interference Abstractions Henning Günther
Sept 19 Con2colic testing Andreas Holzer
Sept 26 Partial Orders for Efficient Bounded Model Checking of Concurrent Software Michael Tautschnig
Nov 28 Detecting Inefficiently-Used Containers to Avoid Bloat Ivan Radiček
Dec 5 Linear Ranking with Reachability Moritz Sinn
Dec 12 A Data Driven Approach for Algebraic Loop Invariants Johannes Birgmeier
Dec 19 Efficiently Solving Quantified Bit-Vector Formulas Gergely Kovasznai
Jan 16 Refinement Types for ML Yulia Demyanova

Private: FORSYTE Internal Portal

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