Talks

Keynote

• Reliable AI code generation through sound program analysis

  Armando Solar-Lezama

  Chair: Guy Avni 

Invited Talk

• Neural Stochastic Control and Verification for Safe Autonomy

  Đorđe Žikelić

  Table Host Chair: Guy Avni 

• A high-level view on causal representation learning with actions

  Sara Magliacane

  Table Host Chair: Guy Avni 

• Latent space navigation – interpretation, probing and steering

  Lenka Tětková

  Table Host Chair: Christian Schilling 

• When Control Changes the Data: Safety under Interaction-Driven Distribution Shifts

  Lars Lindemann

  Table Host Chair: Christian Schilling 

Presentation

• Temporal Guardrails for LLM Conversations: A Runtime Verification Framework

  Itay Cohen, Klaus Havelund, Moran Omer, Doron Peled

  Paper Chair: Ekaterina Komendantskaya 

• Certified Neural Approximations of Nonlinear Dynamics

  Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

  Paper Chair: Kaushik Mallik 

• Value Functions as Supermartingale Certificates

  Alessandro Abate, Daniel Contro, Mirco Giacobbe, Agustín Martínez-Suñé, Diptarko Roy

  Paper Chair: Mirco Giacobbe 

• Principled Rewriting of ONNX Operators for Reluctant Solvers

  Alban Grastien, Guilhem Ardouin, Julien Girard-Satabin

  Paper Chair: Mirco Giacobbe 

• Incremental Invariant-based Safety Verification of Neural Controllers

  Vladislav Nenchev

  Paper Chair: Mirco Giacobbe 

• Enhancing the Robustness of Counterfactual Explanations via Adversarial Training

  Rithik Appachi Senthilkumar, Francesco Leofante, Vijay Ganesh

  Paper Chair: Mirco Giacobbe 

• MetaMoE: Formal Verification of Compositional Robustness and Scalability of Mixture-of-Experts Architecture

  Quang Pham, Ben Wooding, Luke Nam, Samuel Sasaki, Taylor T. Johnson

  Paper Chair: Ekaterina Komendantskaya 

• Faster Optimization of Decision Tree Policies for Markov Decision Processes

  Daniël Vos, Anna Lukina

  Paper Chair: Mirco Giacobbe 

• Neural Network Verification using Partial Multi-Neuron Relaxation

  Ido Shmuel, Guy Katz

  Paper Chair: Taylor T. Johnson 

• Verified Tensor Operators for Safety-Critical ML: From Specification to Reference Implementation

  João Machado, Ricardo Silva, Loïc Correnson, João Galego, Eric Jenn, Hugo Daniel Macedo, Jean Souyris, Jorge Sousa Pinto

  Paper Chair: Omri Isac 

• Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features

  Anne M. Tumlin, Ben Wooding, Zhenxuan Shao, Diego Manzanas Lopez, Tyler Derr, Taylor T. Johnson

  Paper Chair: Omri Isac 

• A Self-Correcting Neuro-Symbolic AI Reasoning Framework

  Ben Wooding, Kiersten Brennan, Anne M. Tumlin, Hongchao Zhang, Taylor T. Johnson

  Paper Chair: Omri Isac 

• Automated Algorithm Configuration of α,β-CROWN

  Konstantin Kaulen, Holger H. Hoos

  Paper Chair: Omri Isac 

• Hybrid Robustness Verification for Spatio-Temporal Neural Networks

  Sherwin Varghese, Matthew Wicker, Alessio Lomuscio

  Paper Chair: Omri Isac 

• Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound

  David Boetius, Stefan Leue, Tobias Sutter

  Short presentation (7 min) Chair: Ekaterina Komendantskaya 

• Optimizing VNN Solver Configuration Selection using Large Language Models

  Salil Kamath, Matthew Davis, Jonathan Andreason, Yatis Dodia, Vijay Ganesh

  Short presentation (7 min) Chair: Kaushik Mallik 

• VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change

  Sterre Lutz, Matthijs T.J. Spaan, Anna Lukina

  Short presentation (7 min) Chair: Ekaterina Komendantskaya 

• PICID: Proof-Driven Clause Learning in Neural Network Verification

  Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz

  Short presentation (7 min) Chair: Ekaterina Komendantskaya 

• Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

  Hengjie Liu, Zhenya Zhang, Jianjun Zhao

  Short presentation (7 min) Chair: Ekaterina Komendantskaya 

• Verification of LTL properties on Neural Networks for Chemical Process Monitoring

  Julien Girard-Satabin, Simon Lutz, Daniel Neider

  Paper Short presentation (7 min) Chair: Kaushik Mallik 

• Vancomycert: A Certified Neuro-Symbolic Drug Delivery System

  Alistair Sirman, Fleur Conway, Jessica Ciupa, Gusts Gustavs Grīnbergs, Ekaterina Komendantskaya, Thai Son Hoang, Michael Rawson, Alessandro Bruni, Vaishak Belle, Michael John Williams

  Paper Short presentation (7 min) Chair: Kaushik Mallik 

• veriFIRE: An Industrial Case Study in Verifying Consistency Properties for DNN-Based Wildfire Detection System

  Idan Refaeli, Maya Swisa, Itay Buchnik, Alon Zada, Guy Amir, Elad Mandelbaum, Ziv Freund, Guy Katz

  Paper Short presentation (7 min) Chair: Kaushik Mallik 

• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

  Prithwish Jana, Kaan Kale, Ahmet Ege Tanriverdi, Cruise Song, Sriram Vishwanath, Vijay Ganesh

  Short presentation (7 min) Chair: Kaushik Mallik 

• Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

  Samuel Teuber, Debasmita Lohar, Bernhard Beckert

  Short presentation (7 min) Chair: Kaushik Mallik 

VNN-COMP

• VNN-COMP

  Taylor T. Johnson, Lukas Koller, Tobias Ladner, Benedikt Kellner, Matthias Althoff, Linhan Li, ThanhVu Nguyen, Lukas Rohwer, Samuel Teuber, Matthew L. Daggitt, Samuel Sasaki, Ben Wooding, Hanchen David Wang, Anne M. Tumlin, Meiyi Ma

  Chair: Taylor T. Johnson 

Discussion

• Round-Table Discussion

  on  Fri, 10:00 in  Main Room

Break

• Coffee Break

  on  Fri, 10:30 in  Main Room

• Lunch

  on  Fri, 12:00 in  Main Room

  Posters