Introduction
Welcome to the Workshop on Program Analysis and Verification (WPAV 2025)! This workshop aims to bring together researchers and practitioners to discuss the latest advancements, challenges, and future directions in the field of program analysis and software verification. We seek to foster collaboration and exchange of ideas in this critical area of computer science.
Date
May 24 - May 25, 2025
Location
Meeting Room 205, Building 7, Zhongguancun Xinyuan, Haidian District, Beijing
Program
May 24 (Saturday) Afternoon: 13:20 - 17:30
13:20 - 13:30: Zhenjiang Hu (PKU), Opening Remarks
Keynote 1 (Host: Zhenjiang Hu)
13:30 - 14:30: Wei-Ngan Chin (NUS), From Separation Logic to Staged Logic for Higher-Order Programs and Beyond
Abstract: Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated function parameters.
One inherent limitation of existing specification mechanisms is its reliance on {\em only two stages} :an initial stage to denote the precondition at the start of the method and a final stage to capture the postcondition. Such two-stage specifications force abstract properties to be imposed on unknown function parameters, leading to less precise specifications for higher-order methods.
To overcome this limitation, we introduce a novel extension to Hoare logic that supports {\em multiple stages} for a call-by-value higher-order language with ML-like local references. In this talk, we introduce our staged logic with its semantics, and show how it can be used to handle higher-order imperative programs, including those that arise from the use of delimited continuations (from algebraic effects).
Session 1 (Chair: Di Wang)
14:30 - 15:00: Yiyuan Cao (PKU), Reflections on Proof-Integrated Programming: the continuing C* journey
15:00 - 15:30: Xiwei Wu (SJTU), QCP: A Practical Separation Logic-based C Program Verification Tool
15:30 - 16:00: Break
Session 2 (Chair: Jian Zhang)
16:00 - 16:30: Zhiyi Wang (PKU), Stellis: A DSL for Automation Strategies in Separation Logic Entailments
16:30 - 17:00: Shushu Wu (SJTU), Verifying Sequential Programs Intuitively with Relational and Unary Reasoning
17:00 - 17:30: Qihao Lian (PKU), Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
May 25 (Sunday) Morning: 09:30 - 12:00
Keynote 2 (Host: Zhenjiang Hu)
09:30 - 10:30: Chongyi Yuan (PKU), Math Variable, Program Variable, and Program Semantics
Abstract: The concept of variables is one of the most fundamental building blocks in programming. A program variable differs from a mathematical variable: the former refers to the name of a memory location of a specific size, whereas the latter is unrelated to memory locations. Recognizing this distinction has guided the study of formal semantics in a new direction—one that differs from Hoare logic. Important concepts, including semantic predicates (SP for short), SP formulas, and SP calculus, have been proposed. These concepts can be applied to the analysis at every stage of the software lifecycle, except for user requirements. As a result, it is now possible to provide precise formal definitions of program semantics and, further, to compute semantics directly from program text. This semantic computation is independent of initial variable values, and statements are paired to compute semantics in parallel. Consequently, the complexity of semantic computation is O(log N), where N is the number of statements. However, N is usually very large, so automated tools are necessary.
Session 3 (Chair: Qinxiang Cao)
10:30 - 11:00: Zhilei Han (THU), Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification
11:00 - 11:30: Shenghua Feng (ZGC), Probabilistic Program Verification from the Perspective of the Dirichlet Problem
11:30 - 12:00: Wenjian Chai (ISCAS), Evaluating the Effectiveness of Slice-Assisted Program Verification
May 25 (Sunday) Afternoon: 13:30 - 17:30
Session 4 (Chair: Sergey Mechtaev)
13:30 - 14:00: Xie Li (ISCAS), Towards Large Language Model Guided Kernel Direct Fuzzing
14:00 - 14:30: Tianchi Li (PKU), LLM-Based Loop Invariant Synthesis with Iterative Formal Verification Feedback
14:30 - 15:00: Dimitrios Bouras (PKU), HoarePrompt: Structural Reasoning About Program Correctness in Natural Language
15:00 - 15:30: Break
Session 5 (Chair: Naijun Zhan)
15:30 - 16:00: Hao Wu (ISCAS), Optimization-based Invariant Synthesis
16:00 - 16:30: Jun Liu (ISCAS), Development of Large Model-Assisted Code Checkers
Panel (Host: Xin Zhang)
16:30 - 17:30: Panel on Program Analysis and Verification
Meals
Evening Meal on May 24
Heyuan Restaurant Buffet, Zhongguancun Xinyuan, Haidian District, Beijing
Midday Meal on May 25
Guanhu Hall, Building 1, Zhongguancun Xinyuan, Haidian District, Beijing
Organizers
Committee (Alphabetical Order)
- Wang, Di (Co-Chair), Peking University
- Zhang, Xin (Co-Chair), Peking University
- Cao, Qinxiang, Shanghai Jiaotong University
- He, Fei, Tsinghua University
- Hu, Zhenjiang, Peking University
- Mechtaev, Sergey, Peking University
- Wu, Zhilin, Institute of Software, Chinese Academy of Science
- Xiong, Yingfei, Peking University
- Zhan, Naijun, Peking University
- Zhang, Jian, Institute of Software, Chinese Academy of Science
Contact
Please contact us at: yy_sun at pku.edu.cn