Accepted Papers

Authors	Title
Ilana Shapiro, Sorin Lerner and Nikolaj Bjørner	Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection
Alexander Bai, Chris Hawblitzel and Andrea Lattuada	Tunable Automation in Automated Program Verification
Filippo Fantinato, Alessandro Cimatti and Stefano Tonetta	Symbolic Automata for MTL0,inf with Super-Dense Semantics
Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett and Guy Katz	PICID: Proof-Driven Clause Learning in Neural Network Verification
Martin Jonáš, Lea Petřivalská and Jakub Šárník	On the Complexity of Word-Level Model Checking with Arrays
Emina Torlak	SymCert: Verifying SMT-Based Policy Analyses
Guy Frankel, Rudi Schneider, Michel Steuwer and Elizabeth Polgreen	Synthesis with Counterexample Guided Observational Equivalence Graphs
Raya Elsaleh, Liam Davis, Haoze Wu and Guy Katz	Incremental Neural Network Verification via Learned Conflicts
Dao Bo Yang, Arie Gurfinkel and Richard Trefler	Prophecy Variables and Invariants in the Move Prover
Joseph Tafese, Arie Gurfinkel, Sam Bayless, Nick Feng and Milad Hooshyar	Verifiable Checks for Business Rule Consistency
Xuyang Li, Jiahao Xia, Ahmed Adnan and Jingbo Wang	PSOUFFLÉ: Scaling Exact Probabilistic Logic Inference for Program Analysis
Max Barth and Marie-Christine Jakobs	Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
Piotr Wojciechowski and K. Subramani	F-QLPs over unit relative constraints
Derek Egolf, Yuhao Zhou and Stavros Tripakis	Can LLMs Perform Synthesis?
Jan Onderka, Armin Biere and Mathias Fleury	Lean Certified Bitvector Solving without Bitblasting
Jesse Looney, Jonah McDonald, Allison Klingler, Gloria Wu, Jonad Pulaj and Haoze Wu	Solution Space Partitioning for Extremal Set Theory
Pedro Saccomani, Abdalrhman Mohamed, Elizaveta Pertseva, Daniela Kaufmann, Cesare Tinelli, Clark Barrett and Haniel Barbosa	Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean
Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Lars Lindemann, Alberto Speranzon and Jyotirmoy Deshmukh	Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO
Jakovs Ratners, Nikolajs Tihomorskis and Arturs Aboltins	Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines
Arınç Demir and Dogan Ulus	Multi-Property Temporal Logic Monitoring
Tereza Kinská, Jan Kretinsky, Tobias Meggendorfer, Sabine Rieder and Maximilian Weininger	dtControl2+ε: Trading Optimality for Explainability in MDPs via Decision Trees
Jule Schmidt, Maximilian Weininger, Clemens Dubslaff, David Parker and Nils Jansen	Property-driven Causal Abstractions for Markov Decision Processes
Aditi Kabra, Jonathan Laurent, Ruben Martins, Stefan Mitsch and André Platzer	LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games
Dexin Zhang, Timothy Alberdingk Thijm, David Walker and Aarti Gupta	CB-VER: A Stable Foundation for Modular Network Control Plane Verification
Arman Ferdowsi and Laura Kovács	Certificate-Aware Property-Directed Reachability
Gera Weiss and Jules Zisser	Conditional Sampling of Symbolic Markov Chains
Alexander Nadel, Yam Slonimski and Ofer Strichman	Aperture: an Anytime, Complete and Incremental MaxSAT Solver
Anoud Alshnakat, Roberto Guanciale and Mads Dam	PolyGram: A Certifying Compiler for Network Policies
Yogev Shalmon, Alexander Nadel and Ofer Strichman	NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT
Liu Jun, Liu Jingxuan, Shenghao Yuan, David Sanan, Chen Kang, Cao Donggang and Yongwang Zhao	Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees
Ocan Sankur, Thierry Jéron, Nicolas Markey, David Mentré and Reiya Noguchi	Requirement-Based Testing: Enhancing Reinforcement Learning with Game Theory
Shuangyu Lyu, Chuan Luo, Ruizhi Shi, Yuechen Duan and Chunming Hu	SATDiv: An Effective Solver for Diverse SAT Problem
Lee Barnett, Loris D’Antoni, Amit Goel, Rami Gökhan Kıcı, Tim King, Kasper Luckow, Neha Rungta and Yasmine Sharoda	Efficient Enumeration of Cloud Access Permissions
Massimo Bartoletti, Riccardo Marchesin and Roberto Zunino	Certifying optimal MEV strategies with Lean
Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo and Mark Turnbull	Trimming Pseudo-Boolean Proofs
Verner Vlacic	Beyond Lemma Sharing – Novel Parallelization Strategies for PDR
Kunal Sheth and Sara Achour	Lemma Pattern Matching for SMT-based Verification of Analog Mixed-Signal Hardware
Jorge Gallego-Hernández, Enrico Lipparini and Alessio Mansutti	MCSAT Modulo Transcendental Arithmetics
Ekanshdeep Gupta and Thomas Wies	An Extension API for the Concurrent Program Verifier Raven
Andrew Cheung, Chandrakana Nandi and Sorin Lerner	Conditional Rewrite Rule Synthesis Using E-Graphs and Implication Propagation
Hadar Frenkel and Sarai Sheinvald	On the Hierarchy of Finite-Word Hyperlanguages
Yizhak Elboher, Reuven Peleg, Zhouxing Shi, Guy Katz and Jan Křetínský	Talking with Verifiers: Automatic Specification Generation for Neural Network Verification
Charles Koll, Houssam Abbas and Mike Rosulek	Privacy-Preserving Robust Monitoring of Dense-Time Temporal Logic
Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap and Jake Silverman	Formal Verification of Imperative First-Class Functions in Move
Pete Austin, Daniele Dell’Erba and Patrick Totzke	The Game Graph Gym
Augusto Mafra and Haniel Barbosa	Formal Verification of Mixed-Signal Systems Using Real Number Modeling with SMT-based Model Checking
Tung-Che Chang, Sehyeok Park, Jay Lim and Santosh Nagarakatte	Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean
Alicia Michael, Nicholas Coughlin, Kait Lam and Kirsten Winter	Validated Binary Decompilation Without Tears
Christopher Johannsen and Kristin Yvonne Rozier	Shrinking Mission-time LTL Runtime Monitors with Equality Saturation
Yong Kiam Tan, Dominik Schreiber, Johannes Åman Pohjola and Magnus O. Myreen	Verified Real-time Proof Checking for Large-Scale SAT Solving
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli and Clark Barrett	Extending an SMT Solver with LIA⋆ Constraints
Cynthia Peyrer, Maximilian Heisinger and Martina Seidl	ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework
Niccolò Rigi-Luperti, Armin Biere and Dominik Schreiber	Parallel SAT Sweeping on CNFs
Amir Kafshdar Goharshady, Thomas Hader, Laura Kovács and Harshit Jitendra Motwani	Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields
Rüdiger Ehlers, Nils Hölzner and Tobias Kühnel	Translating LTL to Lasso Automata
Tobias Seufert and Christoph Scholl	Certified Sequential Sweep Without Unrolling
Nicolai Fiege and Martin Lange	Optimising Constant Matrix Multiplication Circuits is NP-complete
Lorenzo Ceragioli, Letterio Galletta and Edoardo Lunati	Checking Information Flow in Cloud-based IoT Access Control Policies
Jesse Looney, Nikolaj Bjørner, Haoze Wu and Nina Narodytska	Weight-Aware Transformations for MaxSAT
Yi-De Wu	Compositional ISA-Compliance Verification of Out-of-Order RISC-V Cores
Jaehyeok Choi and Andrew Miner	Binary Decision Diagrams Unchained
Leni Aniva, Iori Oikawa, David Dill and Clark Barrett	Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
Zachary Kent and Amar Shah	Parallelizing Congruence Closure
Yu-An Shih, Soohyuk Cho, Aarti Gupta and Sharad Malik	SVAEval: An Evaluation Framework for LLM-based SVA Property Generators
Tiago Campos, Sophie Tourret, Jasmin Blanchette and Haniel Barbosa	IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL
Sam Kouteili, William Fishell, Mark Santolucito and Ruzica Piskac	Learning GR(1) Specifications from Traces
Noah Schwartz, Chandra Kanth Nagesh, Sriram Sankaranarayanan, Ramneet Kaur, Tuhin Sahai and Susmit Jha	Optimized Piecewise Affine Abstractions of Neural Networks with Learnable Activation Functions
Shimin Zhang, Yechuan Xia, Chunxiao Li, Jianwen Li, Moshe Y. Vardi and Vijay Ganesh	Understanding CDCL Solvers via Scalability Studies and Proofdoors
Tate Rowney, Riyaz Ahuja, Jeremy Avigad and Sean Welleck	DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Sinai Kakishita, Akira Hasegawa, Aoki Toshiaki, Ryuta Kambe and Yuuki Takano	Verifying a Memory Allocator for Rust
Chih-Hsiang Chuang, Chi-Kit Ng and Jie-Hong R. Jiang	Stochastic Boolean Satisfiability for Two-Player Sequential Games under Uncertainty