Schedule

Monday
11:30-12:00 Registration
12:00-13:30 Lunch
13:30 - 15:30 Andrew Reynolds Synthesis by Quantifier Instantiation in CVC4
Andreas Fröhlich Quantifier-free bit-vectors: Complexity and alternative solving approaches
Marco Gario Presenting PySMT: SMT in Python
Igor Konnov SMT and POR beat Counter Abstraction
15:30-16:00 Coffee Break
16:00-17:00 Dexter Kozen  Invited Talk: Second-Order Abstract Interpretation via Kleene Algebra
17:00-18:00 Thosten Tarrach Succinct Representation of Concurrent Trace Sets
Mitra Tabaei Befrouei Explaining Concurrency Bugs with Interpolants
19:00 Dinner
Tuesday
09:00-10:00 Konstantin Selyunin Neural Programs: Towards Adaptive Control in Cyber-Physical Systems
Stefan Jaksic Hardware Monitoring of Analog and Mixed Signal Systems
10:00-10:30 Coffee Break
10:30-12:30 Ravi Madhavan Algorithmic Grammar Exploration and Analysis
Salomon Sickert Deterministic omega-Automata for LTL: A safraless, compositional and mechanically verified construction
Alfons Laarman Partial-Order Reduction for Multi-Core LTL Model Checking
Stefan Löwe Sliced Path Prefixes: An Effective Method to Enable Refinement Selection
12:30-14:30 Lunch
14:30-16:00 Philipp Wendler Benchmarking and Resource Measurement
Thomas Pani Empirical Software Metrics for Benchmarking of Verification Tools
Grigory Fedyukovich Incremental Proof-Based Verification of Compiler Optimizations
16:00-16:30 Coffee Break
16:30-18:00 Gilles Nies Recharging Probably Keeps Batteries Alive
Martin Chmelik What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Tomas Fiedor Nested Antichains for WS1S
18:30 Short Walk (60 Minutes) + Dinner
Wednesday
9:00-10:30 Sergiy Bogomolov SpaceRover: Parameter Synthesis for Multiaffine Systems beyond RoVerGeNe
Yuliya Butkova Continuous Optimal Timing
Dogan Ulus Timed Pattern Matching
10:30-11:00 Coffee Break
11:00-12:30 Matthias Dangl Boosting k-Induction with Continuously-Refined Invariants
Egor Karpenkov Scalable Code Analysis with Local Policy Iteration
Moritz Sinn Invariant Analysis and Bound Analysis: Better Together
12:30-14:00 Lunch
End of AVM