Accepted Papers

Authors	Title
Samuel Teuber, Debasmita Lohar and Bernhard Beckert	Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Aaron Tomb and Anjali Joshi	Static Coverage in Deductive Software Verification
Lee Barnett, Loris D’Antoni, Amit Goel, Rami Gökhan Kıcı, Neha Rungta, Mary Southern and Chungha Sung	Modeling the AWS Authorization Engine
Yuan Xia, Aabha Shailesh Pingle, Deepayan Sur, Srivatsan Ravi, Mukund Raghothaman and Jyotirmoy V. Deshmukh	Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models
Leiqi Ye, Guy Frankel, Yixuan Li, Jianyi Cheng and Elizabeth Polgreen	Unlocking Hardware Verification with Oracle Guided Synthesis
Alexander Konrad and Christoph Scholl	FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
Matthew Sotoudeh and Zachary Yedidia	A Formally Verified Software Fault Isolation System
Jackson Melchert, Caleb Terrill, Áron Ricardo Perez-Lopez, Clark Barrett and Priyanka Raina	Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Carl Kwan, Yutong Xin and William D. Young	A Formal Y86 Simulator with CHERI Features
Meghan Stuart and Parasara Sridhar Duggirala	Quantifying Robustness of 3D BioMedical Image Segmentation Networks Using TensorStars
Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Marsha Chechik	Bounded Quantifiers for Finite Relations
Amirmohammad Nazari, Matin Amini and Mukund Raghothaman	“How Does my Circuit Work?”: Local Explanations for the Behavior of Sequential Circuits
Sewon Park and Atsushi Igarashi	Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops
Oliver Markgraf, Anthony W. Lin, Matthew Hague, Philipp Rümmer, Zhilin Wu, Denghang Hu and Artur Jeż	OSTRICH: Solver for Complex String Constraints
Raven Beutner and Bernd Finkbeiner	On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Amar Shah, Twain Byrnes, Joseph Reeves and Marijn J. H. Heule	Learning Short Clauses via Conditional Autarkies
Mitja Kulczynski, Kevin Lotz and Dirk Nowotka	s2s: An Eager SMT Solver for Strings
Christopher Johannsen, Phillip Jones, Tichakorn Wongpiromsarn and Kristin Yvonne Rozier	Scalable MLTL Reasoning via Logarithmic Bit-Vector Encoding
Alexis Aurandt, Kristin Yvonne Rozier and Phillip H. Jones	R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor
Amalee Wilson, Nina Narodytska, Clark Barrett and Haoze Wu	Per-Instance Subproblem Generation for Strategy Selection in SMT
Yahya Sohail and Warren Hunt	A Method for the Verification of Memory Management Software in the Presence of TLBs
Joseph Tafese, Siddharth Priya, Giuliano Losa, Arie Gurfinkel and Graydon Hoare	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli and Clark Barrett	Towards SMT Solver Stability via Input Normalization
Petra Hozzová and Nikolaj Bjørner	Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward Lee and Sanjit Seshia	PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch and André Platzer	Can Large Language Models Autoformalize Kinematics?
Ilo Chen, Che Cheng and Jie-Hong R. Jiang	Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications