SETTA 2026: THE 12TH INTERNATIONAL SYMPOSIUM ON DEPENDABLE SOFTWARE ENGINEERING, THEORIES, TOOLS AND APPLICATIONS

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

Disclaimer | Powered by EasyChair Smart Program