Program

Friday
Saturday

#I0		Main Room		Main Room (2)

9:00	Neural Stochastic Control and Verification for Safe Autonomy Đorđe Žikelić Table Host Chair: Guy Avni
:15
:30	A high-level view on causal representation learning with actions Sara Magliacane Table Host Chair: Guy Avni
:45
10:00	Round-Table Discussion
:15	Round-Table Discussion
:30	Coffee Break
:45	Coffee Break
11:00	Temporal Guardrails for LLM Conversations: A Runtime Verification Framework Itay Cohen, Klaus Havelund, Moran Omer, Doron Peled Paper Chair: Ekaterina Komendantskaya
:15	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
:30	Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound David Boetius, Stefan Leue, Tobias Sutter Short presentation (7 min) Chair: Ekaterina Komendantskaya	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
:45	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
12:00	Lunch Posters
:15
:30
:45
13:00
:15
:30	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
:45
14:00
:15	Neural Network Verification using Partial Multi-Neuron Relaxation Ido Shmuel, Guy Katz Paper Chair: Taylor T. Johnson
:30	Coffee Break
:45	Coffee Break
15:00	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
:15	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
:30	A Self-Correcting Neuro-Symbolic AI Reasoning Framework Ben Wooding, Kiersten Brennan, Anne M. Tumlin, Hongchao Zhang, Taylor T. Johnson Paper Chair: Omri Isac
:45	Automated Algorithm Configuration of α,β-CROWN Konstantin Kaulen, Holger H. Hoos Paper Chair: Omri Isac
16:00	Hybrid Robustness Verification for Spatio-Temporal Neural Networks Sherwin Varghese, Matthew Wicker, Alessio Lomuscio Paper Chair: Omri Isac

#I0		Main Room		Main Room (2)

9:00	Latent space navigation – interpretation, probing and steering Lenka Tětková Table Host Chair: Christian Schilling
:15
:30	When Control Changes the Data: Safety under Interaction-Driven Distribution Shifts Lars Lindemann Table Host Chair: Christian Schilling
:45
10:00	Round-Table Discussion
:15	Round-Table Discussion
:30	Coffee Break
:45	Coffee Break
11:00	Certified Neural Approximations of Nonlinear Dynamics Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate Paper Chair: Kaushik Mallik
:15	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
:30	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
:45	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	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
12:00	Lunch Posters
:15
:30
:45
13:00
:15
:30	Reliable AI code generation through sound program analysis Armando Solar-Lezama Chair: Guy Avni
:45
14:00
:15
:30	Coffee Break
:45	Coffee Break
15:00	Value Functions as Supermartingale Certificates Alessandro Abate, Daniel Contro, Mirco Giacobbe, Agustín Martínez-Suñé, Diptarko Roy Paper Chair: Mirco Giacobbe
:15	Principled Rewriting of ONNX Operators for Reluctant Solvers Alban Grastien, Guilhem Ardouin, Julien Girard-Satabin Paper Chair: Mirco Giacobbe
:30	Incremental Invariant-based Safety Verification of Neural Controllers Vladislav Nenchev Paper Chair: Mirco Giacobbe
:45	Faster Optimization of Decision Tree Policies for Markov Decision Processes Daniël Vos, Anna Lukina Paper Chair: Mirco Giacobbe
16:00	Enhancing the Robustness of Counterfactual Explanations via Adversarial Training Rithik Appachi Senthilkumar, Francesco Leofante, Vijay Ganesh Paper Chair: Mirco Giacobbe

Caption

Keynote

Invited Talk

Presentation

VNN-COMP

Discussion

Break