4th–8th August 2026, Berlin, Germany
Opening
KeYnote: “Formal Methods for AI First” – Bernhard Steffen
“Case Study on Verifying a Topologic and Geometric Modeller” – Wolfram Pfeifer
“LLM-based Program Synthesis in Correctness-by-Construction Engineering” – Maximilian Kodetzki
“Correct-by-Construction Device Drivers in Pancake” – Jakob Jarebica
“An Approach for Consistent Multi-domain Model-based Testing” – Fynn Demmler
“RustyKeY” – Daniel Drodt
“KeY4CATs: An Extension of KeY for CATs” – Marco Scaletta
“Single Path Model Checking with DA Logic” – Lukas Grätz
“LAGC Trace Semantics for Deductive Verification with Dynamic Logic” – Johannes Jung
“Trace Formulas for Autonomous Driving” – Niklas Heidler
“Formally Guaranteeing Data-Driven Trace Conformance” – Adrian Kulmburg
KeYnote: “The next generation of formal verification tools” – Gidon Ernst
“On the Logic of Bounds in Termination Proofs of While Statements” – Frank de Boer
“A Semantics-Preserving Translation Tool between Contract-LIB and Specifications for Deductive Java Verifiers” – Robert Brune
“Cooperative and Modular Verification of Imperative Programs” – Florian Lanzinger
“Integrating an Ownership Type System into the Workflow of the Program Verifier KeY” – Daniel Grévent
“Differential CSP – Dynamic Logic of Continuously Communicating Sequential Processes” – Marvin Brieger
“Modeling and Verification of Systems with Multiple Obstacles in Heterogeneous Dynamic Logic: A Case Study” – Max Hecht
“Synthesis of Auxiliary Specifications via Large Language Models” – Nils Buchholz
“Proving Challenges for Sorting Nets” – Thomas Baar
“Applying Supervisory Control Theory to Smart Contracts” – Wolfgang Ahrendt
Closing