Model Checking the Speculative Primary-Order Atomic Broadcast Protocol
Jim Kemp and Jun Pang
LLM-Generated Separation Logic Specifications for Heap-Manipulating Programs: Are We There Yet?
Wenjie Wu, Cheng Wen, Shengchao Qin, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun and Cong Tian
Verifying Register Protection in AArch64 Hypervisor
Hongbai Su, Di Luo, Zhuoruo Zhang, Rui Chang and Yongwang Zhao
Formalization of the Completeness Theorem for First-Order Logic with Equality in Rocq
Xiang Ji, Dakai Guo and Wensheng Yu
Formal Verification of Graham's Scan Algorithm and its Implementation in C
Yuxuan Sun, Yingjun Lan and Qinxiang Cao
Complete Formalization of TLA in a Foundational Theorem Prover
Yizhou Mao and Yuting Wang
SCALC: A Safety-Case-Guided Assurance Framework for Lustre Compilers
Shurong Shi, Yuxin Deng, Yanhong Huang and Wenjie Du
Context-dependent Runtime Enforcement
Saumya Shankar, Srinivas Pinisetty, Thierry Jéron and Srishti Gupta
Caster: Cost-Aware Selection of BTOR2 Verifiers
Xuhui Li, Yiyuan Zhang, Tianjun Bu, Qiusong Yang, Fu Song and Zhilin Wu
A Linear-time Parameterized Algorithm for Optimal Register Allocation with Copy Coalescing
Amir Kafshdar Goharshady, Tian Shu and Ahmed Khaled Zaher
A Hybrid SMT-NRA Solver: Integrating 2D-Cell-Jump-Based Local Search, MCSAT and OpenCAD
Tianyi Ding, Haokun Li, Xinpeng Ni, Bican Xia and Tianqi Zhao
Preserving Semantics for Transpilation of Data Modelling Languages using CafeOBJ
Manoj Gudi, Ahmed Bouabdallah, Jean-Marie Bonnin and Frédéric Weis
Compositional Automata Learning of Timed Synchronous Systems
Hanyue Chen, Chang Liu and Miaomiao Zhang
MSLR-ARB: Graph Learning with Multi-Scale Local and Relation-Specific Views for Function-Level Aging-Related Bug Detection
Xingyu Chen and Jing Liu
Exact Loop Bound Analysis via Exit Invariants
Yi Zhou, Hongfei Fu and Guoqiang Li
Craig Interpolation for Trigonometric Polynomial Formulas with Affine Phases
Yuxiang Zhao, Ruiting Wang and Ting Gan
Synthesis and Verification of Register Automata over Data Sequences
Chih-Duo Hong, Hongjian Jiang, Anthony Lin, Oliver Markgraf, Julian Parsert and Tony Tan
The Bounded Treedepth of Programs and Treedepth-guided CDCL
Mohsen Alambardar Meybodi, Amir Kafshdar Goharshady, Kerim Kochekov and Harshit Jitendra Motwani
Formal Explanations of Machine Learning Ranking Systems via Answer Set Programming
Francesco Chiariello and Joao Marques-Silva
Learning Safe Neural Controllers via Barrier Certificate Guided Polynomial Abstraction
Ying Ma, Xia Zeng and Zhiming Liu
An Information-flow Proof System for Preemptive Kernel Specifications
Jingqing Feng, Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan, Yongzhi Cao and Zhenzhou Shao
Handling Complex Interference Compositionally: A Concurrent Garbage Collector Case Study
Nisansala Yatapanage
Probabilistic Timed Automata with Multiple Sure and Threshold Objectives
Jeremy Sproston