Time: 14:00-17:10, March 24th (Tuesday), 2026.

Venue: Lecture room (334), the 3rd floor, Building 5, Software Park, Chinese Academy of Sciences.

Program:

Information about the talks:

Data-driven verification of procedural programs with integer arrays

Abstract. We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose an algorithmic method for synthesizing loop invariants and procedure pre/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a new learning technique based on reducing a complex classification problem of vectors of integer arrays to a simpler classification problem of vectors of integers. The obtained classifier is generalized to get universally quantified invariants and procedure pre/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark. This is a joint work with Wael-Amine Boutglay and Peter Hebermehl.

Speaker. Ahmed Bouajjani (Université Paris Cité, France)

Introduction of the speaker.

Ahmed Bouajjani is currently Professor at the Université Paris Cité. He has obtained his PhD and his Habilitation in Computer Science from the University of Grenoble where he was Associate Professor. He was appointed at the Université Paris Cité in 1999 where he was leading the "Modeling and Verification" team, and he is leading currently the "Automata, Structures, and Verification" research cluster. His main research interests are formal methods, program verification, concurrency, automata and logic. He has published more than 140 scientific articles. Ahmed Bouajjani is Senior Member of the Institut Universitaire de France since 2013. He received in 2018 the Humboldt Research Award.

Data-driven Termination and Non-termination Analysis

Abstract. Liveness properties are complicated for data-driven approaches. We explore methods to enable proving and disproving program termination by learning termination and non-termination arguments. For termination analysis, we propose an algorithm to learn symbolic loop bounds from a sample set, and validate the hypothesis using a safety checker. For non-termination analysis, we aim to find a recurrent set as the witness. Recurrent set learning is similar to invariant learning, but it poses a challenge as it contains an existential constraint, thus no positive samples can be obtained from a counterexample. To address this problem, we propose to speculate positive samples and backtrack when the prediction is false. Both methods achieve competitive performance compared with state-of-the-art analysis tools.

Speaker. Zhilei Han (Tsinghua University)

Introduction of the speaker.

Zhilei Han is currently a senior PhD candidate at School of Software, Tsinghua University. He has published 5 academic articles in broad fields of formal methods, including probabilistic program verfication, termination and non-termination analysis, constraint solving, and robustness verification for non-volatile memory. His current research interests are memory and persistency models, concurrent program verification, and formal semantics of distributed systems on disaggregated shared memory.

Can LLM Aid in Solving Constraints with Inductive Definitions?

Abstract. Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e.g., abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

Speaker. Weizhi Feng (Institute of Software, CAS)

Introduction of the speaker.

Weizhi Feng is currently a PhD student at the Institute of Software, Chinese Academy of Sciences. His main research interests include hardware/software program verification and model checking. His work has been published on prestigious international conferences/journals including CAV, DAC, FM, Information and Computation.

A Dive into State-of-the-art Open-Source Hardware model Checker ric3

Abstract. 2024 saw a new open-source champion in hardware model checking. As a pinnacle of multiple now-published novel techniques, the `ric3` checker outperformed existing checkers by at least twice in its debut in late 2024 and then again in 2025. This talk gives a general dive into this checker. The talk explains base IC3/PDR algorithm and what makes it powerful, gives an overview of the techniques involving IC3 blocking, generalization, propagation and why or why not each technique is adopted.

Speaker. Tianjun Bu

Introduction of the speaker.

Tianjun Bu is currently pursuing a master degree in Computer Science with the Institute of Software, Chinese Academy of Sciences, advised by Professor Qiusong Yang. He has made some contribution to the ric3 hardware checker, and his research has been accepted by DAC 2026. His research interest is proposing techniques for and optimizing performance of hardware model checker engines.

AssertSynth: LLM-Based Assertion Synthesis via Multimodal Specification Extraction

Abstract. Assertion-Based Verification (ABV) is critical for hardware verification, yet manually writing SystemVerilog Assertions (SVAs) is labor-intensive and error-prone. While Large Language Models (LLMs) offer automation potential, existing methods struggle to process multimodal design specifications, often leading to limited functional coverage. To bridge this gap, we propose AssertSynth, a unified framework that synthesizes high-quality SVAs directly from multimodal hardware specifications. AssertSynth employs modality-aware preprocessing to parse heterogeneous formats into structured representations aligned with signal-level semantics. These representations then drive an assertion synthesis engine via multi-step chain-of-thought (CoT) prompting. To ensure robustness, the framework incorporates a mutation-based evaluation approach using model checking to iteratively refine assertions against undetected mutations. Evaluated on three real-world Register-Transfer Level (RTL) designs, AssertSynth outperforms state-of-the-art methods, achieving an average increase of 8.4% in functional correctness and 5.8% in mutation detection.

Speaker. Enyuan Tian (Institute of Software, Chinese Academy of Sciences)

Introduction of the speaker.

Enyuan Tian is currently pursuing the Ph.D. degree in Computer Science with the Institute of Software, Chinese Academy of Sciences, advised by Professor Qiusong Yang. His research interests lie in the areas of hardware formal verification and LLM-driven Electronic Design Automation, with his work published in international conferences such as ISCAS and CSCWD.