Accepted papers
| Authors | Title |
|---|---|
| KeY4CATs: A Deductive Verification Tool for Context-aware Trace Contracts | Marco Scaletta |
| Practical Range Refinement Types with Inference | Valentin Aebi and Carlo A. Furia |
| Modular Composition of Inductive Types Using Lean Meta-programming | Ramy Shahin |
| Efficient Verification of C Programs with Pointers, Structs, and Arrays | Alexander Stekelenburg and Marieke Huisman |
| Borderlines of Soundness: Verifying C Aliasing Properties | Jérémy Damour, Loïc Correnson, Frédéric Loulergue and Allan Blanchard |
| PETRIFY: Petri-net Based Analysis of Concurrency Properties in Java Bytecode | Akshatha Shenoy and Carlo A. Furia |
| Automata-Guided Local Proof Obligations for Temporal Safety in Synchronous Programs | Térence Clastres and Frédéric Dabrowski |
| Verifying Numerical Methods with Isabelle/HOL | Dustin Bryant, Jonathan Julian Huerta Y Munive and Simon Foster |
| Encodability Criteria for Labelled Semantics | Lukas Bartl, Cinzia Di Giusto and Kirstin Peters |
| Verifying a Rust Bitmap Allocator in RocQ | Rahul Sankalana Gunawardhana, Narges Khakpour and Conrad Grobler |
| Integrating Parallel Trace Abstraction and Explicit Exploration for Test-Case Generation | Max Barth and Marie-Christine Jakobs |
| Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers | Rosa Abbasi and Eva Darulova |
| Diverse Counterexample Pools for Hybrid Automata: Generation and Selection | Sergio Quijano, József Kovács, Georg Arapatsakos, Erika Ábrahám, Mahsa Varshosaz and Andrzej Wasowski |
| Revisiting Sequentialization of Concurrent C Programs | Dirk Beyer, Noah Koenig and Marian Lingsch-Rosenfeld |
| Formal Verification of Stability in Provisioning Changes with BPlan | Eloi Perdereau, Daniel Sokolowski, Jolan Philippe, Hélène Coullon and Guido Salvaneschi |
| Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python | Akira Tanaka and Yusuke Kawamoto |
| Runtime Verification of Communicating Systems Using Data-Aware Interaction Models and Broker-Based Observations | Darine Rammal, Chana Weil-Kennedy, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, Pascale Le Gall, Erwan Mahe, Maxime Morin and Abdelaziz Ouazzani Chahidi |
| Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring | Daisuke Ishii |
| Policy-Guided Test Generation for Autonomous Driving Systems via Probabilistic Model Checking | Srajan Goyal, Radu Calinescu, Alberto Griggio, Ioannis Stefanakos and Stefano Tonetta |
| Robust Skill Execution for Autonomous Robots | Pierre Malafosse, Alexandre Albore, David Doose, Jérémie Guiochet and Charles Lesire |
| Protecting Sensitive Data Against Deductions in Business Processes: Formal Semantics and Model-Checking | Vincent Hugot, Sabine Frittella and Amine Rifi |
| A Formal Case Study of Side-Channel Attacks on a Water Supply System | Julian Klein and Sabine Glesner |
| Formally Verifying Noir Zero Knowledge Programs with NAVe | Pedro Antonino and Namrata Jain |
| SMAC: A Calculus for Verifying Memory Arrays in Isabelle/Solidity | Diego Marmsoler and Asad Ahmed |
| Formal Verification of a Blockchain-Based Healthcare Consent Management Protocol | Suraj Gupta, Frédéric Lang, Umar Ozeer and Gwen Salaün |
| Verification of a Configurable Railway Protection System: Pushing the Envelope | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi, Giuseppe Scaglione and Dylan Trenti |
| Automated Abstraction Refinement for Information Flow Security in Embedded Systems | Jonas Becker-Kupczok, Lukas Ernst and Paula Herber |
| Formal Verification of Credential Provisioning in ISO 15118 Park-and-Charge and Introducing Secure Ownership Transfer | Gabriele Bellini and Roberto Metere |
| Discovering Markovian Models from Event Logs for Resource-Aware Process Analysis | Carlos E. Budde, Vlad Paul Cosma, Alyzia Konsta and Hugo A. López |
| Another Brick in the Loop: From Graphical Loop Invariant to Formal Proofs | Géraldine Brieven, Antoine Grosjean, Pascal Fontaine and Benoit Donnet |
| Don’t Blame the Model, Verify the Data: An Evaluation of SMT-based Dataset Verification | Sehee Park, Dominik Geißler, Andrei Aleksandrov and Kim Völlinger |
| Navigating the Random Forest: Verifying ML Models in Safety-Critical Applications with SMT Solvers | Iwo Kurzidem, Nina Vucenovic, Jakob Schleicher, Karsten Roscher and Dirk Beyer |
| Bridging the Integration Bottleneck: A Java Architecture for Model Checking-Guided Reinforcement Learning | Ahmed Nagy Abdelkhalek Mansour, Samuele Grillo, Matteo Rossi and Vincenzo Viscusi |
| Reactive Correspondence Relationships for Incremental Triple Graph Grammar-Style Model Synchronisation | Monalisha Ojha, Shilpi Gupta, Mohammad Sadeghi, Colin Atkinson, Sebastian Bergemann, Derui Zhu and Alexander Pretschner |
| The Scaffolding Paradox: Evidence from AI-Assisted Dafny Proof Synthesis | Anastasiya Kravchuk-Kirilyuk, Dat Nguyen, Rhea Karty, Simon Henniger, Gabriel Poesia and Nada Amin |
| Functional Basis Reduction of Neural Networks via Approximate Hidden-Neuron Lumping | Ravi Dhiman, Andrea Passarella, Mirco Tribastone and Lorenzo Valerio |
Edit the content of this page here.