Location: Meeting Room, 5th Floor, East Building, North Park, Xixi Campus
Online Meeting: https://meeting.tencent.com/dm/7jXKQi3GLV1Z
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| – | Opening Remarks | Mingshuai Chen | 9:45-10:00 |
| – | Language Design Where Paradigms Meet | Yizhou Zhang | 10:00-10:40 |
| ICFP 2025 | Compiling with Generating Functions | Jianlin Li | 10:40-11:20 |
| OOPSLA 2025/2024 | Lexical Effect Handlers: Fast by Design, Correct by Proof | Cong Ma | 11:20-12:00 |
| – | Lunch Break | – | 12:00-13:50 |
| POPL 2026 | Piecewise Analysis of Probabilistic Programs via k-Induction | Shenghua Feng | 13:50-14:30 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| FM 2025 | Staged Specification Logic for Verifying Higher-Order Imperative Programs | Linyu Yang | 10:00-10:30 |
| – | Probabilistic Program Sensitivity | Mingqi Yang | 10:30-11:00 |
| HSCC 2025 | Robust Identification of Hybrid Automata from Noisy Data | Hengzhi Yu | 11:00-11:30 |
| CGO 2022, ISSTA 2025 | Tristate Numbers Abstract Domain in eBPF Verifier | Yazhou Tang | 13:00-13:30 |
| CAV 2025 | Automated Verification of Monotonic Data Structure Traversals in C | Yucheng Wang | 13:30-14:00 |
| JPK’s Festschrift | What is Formal Verification without Specifications? A Survey on mining LTL Specifications | Xiaqing Zhou | 14:00-14:30 |
| CAV 2024 | Distributed SMT Solving Based on Dynamic Variable-Level Partitioning | Zhiyang Li | 14:30-15:00 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| CAV 2013 | Probabilistic Program Analysis with Martingales | Mingqi Yang | 10:00-10:30 |
| – | Security Analysis of Decoy-State Quantum Key Distribution Based on Probabilistic Model Checking | Yiyang Zhou | 10:30-11:00 |
| – | Preguss: Potential Runtime Errors GUided Specification Synthesis | Zhongyi Wang and Tengjie Lin | 11:00-11:30 |
| CVPR 2025 | Thinking in Space: How Multimodal Large Language Models See, Remember, and Recall Spaces | Yutao Sun | 12:30-13:00 |
| CAV 2025 | Quantitative Supermartingale Certificates | Zhiyang Li | 13:00-13:30 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| CAV 2023, CAV 2024 | Causation Monitoring of Signal Temporal Logic and Its Application to Reinforcement Learning | Jie An | 10:00-10:40 |
| – | Practice in OS Kernel Verification | Shenghua Feng | 10:40-11:00 |
| – | Verify DPDK using VST? | Xiaqing Zhou | 11:00-11:30 |
| – | Runtime Error Assertion Guided Verification | Zhongyi Wang | 12:30-13:00 |
| LICS 2016 | Coinduction All the Way Up | Linyu Yang | 13:00-13:30 |
| – | The Self-Improvement Paradox: Can Language Models Bootstrap Reasoning Capabilities without External Scaffolding? | Yutao Sun | 13:30-14:00 |
| J. ACM | On Strongest Algebraic Program Invariants | Zhiyang Li | 14:30-15:00 |
| – | On the Almost-Sure Termination of Probabilistic Counter Programs | Mingqi Yang | 15:30-16:00 |
| – | Hybrid System Identification | Hengzhi Yu and Bohan Ma | 16:00-16:30 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| LICS 2016, POPL 2023 | Probabilistic Trees | Linyu Yang | 10:30-11:00 |
| USENIX Security 2023 | AnimateDead: Debloating Web Applications Using Concolic Execution | Zhongyi Wang | 11:00-11:30 |
| OSDI 2024 | Using Dynamically Layered Definite Releases for Verifying the RefFS File System | Xiaqing Zhou | 11:30-12:00 |
| HSCC 2024 | FaMoS – Fast Model Learning for Hybrid Cyber-Physical Systems | Hengzhi Yu | 12:00-12:30 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| – | From Interpreters to Compilers: The Algebraic Approach | Linyu Yang | 11:00-11:30 |
| SAS 2019 | Verifying Numerical Programs via Iterative Abstract Testing | Zhongyi Wang | 11:30-12:00 |
| FASE 2024 | Refinement Verification of OS Services based on a Verified Preemptive Microkernel | Xiaqing Zhou | 13:00-13:30 |
| NeurIPS 2022 | Autoformalization with Large Language Models | Yutao Sun | 13:30-14:00 |
| CAV 2023 | Local Search for Solving Satisfiability of Polynomial Formulas | Zhiyang Li | 14:00-14:30 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| ICLR 2024 | Don’t Trust: Verify – Grounding LLM Quantitative Reasoning with Autoformalization | Yutao Sun | 10:00-10:30 |
| – | Autoformalization with Large Language Models | Yutao Sun | 10:30-11:00 |
| Paper Venue | Title of the Presentation | Presenter | Time Slot |
|---|---|---|---|
| ICFP 2024 | Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System | Linyu Yang | 10:00-10:30 |
| POPL 2024 | Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs | Sergei Novozhilov | 10:30-11:00 |
| OOPSLA 2024 | Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach | Yutao Sun | 11:00-11:30 |
| PLDI 2024 | Equivalence and Similarity Refutation for Probabilistic Programs | Mingqi Yang | 13:00-13:30 |
| OSDI 2023 | BWoS: Formally Verified Block-based Work Stealing for Parallel Processing | Xiaqing Zhou | 13:30-14:00 |