Talks

Keynote

• Reliable AI code generation through sound program analysis

  Armando Solar-Lezama

  Chair: TBA 

Invited Talk

• Neural Stochastic Control and Verification for Safe Autonomy

  Đorđe Žikelić

  Table Host Chair: TBA 

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

  Sara Magliacane

  Table Host Chair: TBA 

• Latent space navigation – interpretation, probing and steering

  Lenka Tětková

  Table Host Chair: TBA 

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

  Lars Lindemann

  Table Host Chair: TBA 

Presentation

• Temporal Guardrails for LLM Conversations: A Runtime Verification Framework

  Itay Cohen, Moran Omer, Doron Peled, Klaus Havelund

  Paper Chair: TBA 

• Certified Neural Approximations of Nonlinear Dynamics

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

  Paper Chair: TBA 

• Value Functions as Supermartingale Certificates

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

  Paper Chair: TBA 

• Principled Rewriting of ONNX Operators for Reluctant Solvers

  Alban Grastien, Guilhem Ardouin, Julien Girard-Satabin

  Paper Chair: TBA 

• Incremental Invariant-based Safety Verification of Neural Controllers

  Vladislav Nenchev

  Paper Chair: TBA 

• Enhancing the Robustness of Counterfactual Explanations via Adversarial Training

  Rithik Appachi Senthilkumar, Francesco Leofante, Vijay Ganesh

  Paper Chair: TBA 

• 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: TBA 

• Faster Optimization of Decision Tree Policies for Markov Decision Processes

  Daniël Vos, Anna Lukina

  Paper Chair: TBA 

• Neural Network Verification using Partial Multi-Neuron Relaxation

  Ido Shmuel, Guy Katz

  Paper Chair: TBA 

• 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: TBA 

• 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: TBA 

• A Self-Correcting Neuro-Symbolic AI Reasoning Framework

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

  Paper Chair: TBA 

• Automated Algorithm Configuration of α,β-CROWN

  Konstantin Kaulen, Holger H. Hoos

  Paper Chair: TBA 

• Hybrid Robustness Verification for Spatio-Temporal Neural Networks

  Sherwin Varghese, Matthew Wicker, Alessio Lomuscio

  Paper Chair: TBA 

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

  David Boetius, Stefan Leue, Tobias Sutter

  Short presentation (7 min) Chair: TBA 

• Optimizing VNN Solver Configuration Selection using Large Language Models

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

  Short presentation (7 min) Chair: TBA 

• 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: TBA 

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

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

  Short presentation (7 min) Chair: TBA 

• Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

  Hengjie Liu, Zhenya Zhang, Jianjun Zhao

  Short presentation (7 min) Chair: TBA 

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

  Julien Girard-Satabin, Simon Lutz, Daniel Neider

  Paper Short presentation (7 min) Chair: TBA 

• Vancomycert: A Certified Neuro-Symbolic Drug Delivery System

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

  Paper Short presentation (7 min) Chair: TBA 

• 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: TBA 

• 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: TBA 

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

  Samuel Teuber, Debasmita Lohar, Bernhard Beckert

  Short presentation (7 min) Chair: TBA 

VNN-COMP

• VNN-COMP

  Chair: TBA 

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