Sunday Evening

Informal gathering at the Klosterwirt. Note: self-serviced drinks only unless you have pre-arranged dinner with us already.

Monday

10:15 Welcoming
10:30-12:00
Julia Eisentraut, MdL NRW keynote Diversity, Equity & Inclusion: How to Fill DEI Statements with Life
12:00 Lunch
13:00 Software Verification
Dirk Beyer, LMU Munich regular Cooperative Verification
Pamina Georgiou, TU Wien short The Rapid Verification Framework
Atefeh Zareh Chahoki, University of Trento short Formal verification of smart contracts
Wolfram Pfeifer, Karlsruhe Institute of Technology short Integrating proof state, source code, and specification into a single view in KeY (Ongoing work)
Po-Chun Chien, LMU Munich short BTOR2C: A BTOR2 to C Converter (ongoing work)
Muqsit Azeem, TU Munich short Optimistic and Topological Value Iteration for Simple Stochastic Games
14:30 Coffee Break
15:00 Miscellaneous
Barbora Šmahlíková, Brno University of Technology regular Next Generation of Rank-Based Algorithms for Omega Automata
Kyveli Doveri, Imdea Software short Inclusion Checking for ω-VPL
Marton Hajdu, TU Wien regular Automating induction for equational reasoning in superposition
Short Break
Martin Blicha, Università della Svizzera italiana short Transition Power Abstraction
Michal Hečko, Brno University of Technology short Developments in our work on deciding Presburger arithmetic with automata
Maximilian Schäffeler, TU Munich short Verified Solution Methods for Markov Decision Processes
18:00 Dinner

Tuesday

9:00 Automated Reasoning
Jasmin Blanchette, VU Amsterdam regular Higher-Order Reasoning with Lambda-Superposition
Petra Hozzová, TU Wien regular Towards synthesis in superposition
Enrico Lipparini, University of Genoa regular Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test
10:30 Coffee Break
11:00 Formalization
Tobias Nipkow, TU Munich regular Gale-Shapley Verified
Katharina Kreuzer, TU Munich Germany short Formalization and Verification of CRYSTAL-KYBER
Sarah Sallinger, TU Wien short A Formalization of Heisenbugs and Their Causes
12:00 Lunch
13:00 Loops
František Nečas, Brno University of Technology short Loop Unwinding in the 2LS Framework for Analysis of Dynamically Allocated Memory
Martin Spiessl, LMU Munich short A Unifying Approach for Control-Flow-Based Loop Abstraction
Anton Varonka, TU Wien short On the Unsolvability of Loop Analysis
14:10 Ferry Departure, Social Event
18:00 Dinner

Wednesday

8:50 Model Checking
Helmut Seidl, Sarah Tilscher, TU Munich regular The Topdown Solver: an Exercise in A2I
9:30 Model Checking (Cont., Parallel Session A)
Jan Onderka regular Machine-Code Model Checking: Approaches & Insights
Emily Yu, JKU Linz short Certifying Model Checking Results
Konstantin Kueffner, IST Austria short Monitoring Fairness Properties over Markov Chains
Philipp Czerner, TU Munich short Space Complexity of Population Protocols
9:30 SAT Solving (Parallel Session B)
Adrian Rebola-Pardo, TU Wien, JKU Linz regular Interference-based Proofs in SAT Solving
Maximilian Heisinger, JKU Linz short QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Simone Atzwanger, JKU Linz short Crafted True QBF
Andreas Plank, JKU Linz short Minimal Unsatisfiable Core Extraction
10:30 Coffee Break
11:00 Concurrency (Parallel Session A)
Dominik Harmim, Brno University of Technology regular Static Deadlock Detection in Low-Level C Code
Michael Schwarz, TU Munich short Analysis of Thread IDs and Uniqueness as an Abstraction of Local Traces
Pavel Parizek, Charles University short Efficient and Scalable Incremental Verification of Multithreaded Programs By Checking Just Pairs of Threads
Frank Schüssele, University of Freiburg short Verification of programs with unbounded threads
11:00 Hybrid Systems and Control (Parallel Session B)
Filip Macák, Brno University of Technology regular New Avenues in Inductive Synthesis of Finite-State Controllers for POMDPs
Stefan Ratschan, Czech Academy of Sciences short Decidability of First-order Theories of Real Functions
Marvin Brieger, LMU Munich short Dynamic Logic of Communicating Hybrid Programs
12:00 Lunch
13:00 Software Verification
Philipp Wendler, LMU Munich regular Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
Filip Kliber, Charles University, Prague regular Fuzzing of Multithreaded Programs in .NET - Challenges and Solutions
Dominik Klumpp, University of Freiburg regular Commutativity in Concurrent Program Verification
14:30 Coffee Break
15:00 Miscellaneous
Marcel Ebbinghaus, University of Freiburg short The Concept of Preference Orders for Concurrent Program Verification
Clemens Eisenhofer, TU Wien short User-Propagation for Custom Theories in SMT Solving
Henrik Wachowitz, LMU Munich short Verification as a Service (VaaSe)
15:45 Closing

Thursday

ConVeY social event