Program

PROGRAM

Thursday, December 3rd

09:05

TBD

10:05-10:35Coffee Break

10:35	Jim Kemp and Jun Pang Model Checking the Speculative Primary-Order Atomic Broadcast Protocol (abstract)
10:55	Yuxuan Sun, Yingjun Lan and Qinxiang Cao Formal Verification of Graham's Scan Algorithm and its Implementation in C (abstract)
11:15	Hongbai Su, Di Luo, Zhuoruo Zhang, Rui Chang and Yongwang Zhao Verifying Register Protection in AArch64 Hypervisor (abstract)
11:35	Yuxiang Zhao, Ruiting Wang and Ting Gan Craig Interpolation for Trigonometric Polynomial Formulas with Affine Phases (abstract)

11:55-13:25Lunch Break

13:25

From Attention to Automata: Towards Understanding Neural Language Models (abstract)

14:25	Nisansala Yatapanage Handling Complex Interference Compositionally: A Concurrent Garbage Collector Case Study (abstract)
14:45	Saumya Shankar, Srinivas Pinisetty, Thierry Jéron and Srishti Gupta Context-dependent Runtime Enforcement (abstract)
15:05	Yi Zhou, Hongfei Fu and Guoqiang Li Exact Loop Bound Analysis via Exit Invariants (abstract)
15:25	Mohsen Alambardar Meybodi, Amir Kafshdar Goharshady, Kerim Kochekov and Harshit Jitendra Motwani The Bounded Treedepth of Programs and Treedepth-guided CDCL (abstract)

15:45-16:15Coffee Break

16:15	Francesco Chiariello and Joao Marques-Silva Formal Explanations of Machine Learning Ranking Systems via Answer Set Programming (abstract)
16:35	Wenjie Wu, Cheng Wen, Shengchao Qin, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun and Cong Tian LLM-Generated Separation Logic Specifications for Heap-Manipulating Programs: Are We There Yet? (abstract)
16:55	Xingyu Chen and Jing Liu MSLR-ARB: Graph Learning with Multi-Scale Local and Relation-Specific Views for Function-Level Aging-Related Bug Detection (abstract)
17:15	Ying Ma, Xia Zeng and Zhiming Liu Learning Safe Neural Controllers via Barrier Certificate Guided Polynomial Abstraction (abstract)

Friday, December 4th

09:00

A Systems Programming Language Integrating Coding and Proving (abstract)

10:00-10:30Coffee Break

10:30	Yizhou Mao and Yuting Wang Complete Formalization of TLA in a Foundational Theorem Prover (abstract)
10:50	Jingqing Feng, Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan, Yongzhi Cao and Zhenzhou Shao An Information-flow Proof System for Preemptive Kernel Specifications (abstract)
11:10	Xiang Ji, Dakai Guo and Wensheng Yu Formalization of the Completeness Theorem for First-Order Logic with Equality in Rocq (abstract)

11:30	Hanyue Chen, Chang Liu and Miaomiao Zhang Compositional Automata Learning of Timed Synchronous Systems (abstract)
11:50	Jeremy Sproston Probabilistic Timed Automata with Multiple Sure and Threshold Objectives (abstract)

12:10-13:40Lunch Break

13:40	Shurong Shi, Yuxin Deng, Yanhong Huang and Wenjie Du SCALC: A Safety-Case-Guided Assurance Framework for Lustre Compilers (abstract)
14:00	Manoj Gudi, Ahmed Bouabdallah, Jean-Marie Bonnin and Frédéric Weis Preserving Semantics for Transpilation of Data Modelling Languages using CafeOBJ (abstract)
14:20	Tianyi Ding, Haokun Li, Xinpeng Ni, Bican Xia and Tianqi Zhao A Hybrid SMT-NRA Solver: Integrating 2D-Cell-Jump-Based Local Search, MCSAT and OpenCAD (abstract)

14:40-15:10Coffee Break

15:10	Xuhui Li, Yiyuan Zhang, Tianjun Bu, Qiusong Yang, Fu Song and Zhilin Wu Caster: Cost-Aware Selection of BTOR2 Verifiers (abstract)
15:30	Amir Kafshdar Goharshady, Tian Shu and Ahmed Khaled Zaher A Linear-time Parameterized Algorithm for Optimal Register Allocation with Copy Coalescing (abstract)
15:50	Chih-Duo Hong, Hongjian Jiang, Anthony Lin, Oliver Markgraf, Julian Parsert and Tony Tan Synthesis and Verification of Register Automata over Data Sequences (abstract)