publications

2026

1. Fixing the Fixpoint: A Sound Convergence Criterion for Incremental Recursive Computation

   Chengxi Yang, Tej Chajed, and Thomas Reps

   2026

   Submitted to OOPSLA 2026; currently under review.
2. Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)

   Shushu Wu, Chengxi Yang, Xiwei Wu, and 1 more author

   2026

   Accepted at ICFP 2026.
3. QCP: A Practical Separation Logic-based C Program Verification Tool

   Xiwei Wu, Yueyang Feng^*, Xiaoyang Lu^*, and 10 more authors

   2026

   In TASE 2026.

   Abs arXiv

   As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbfQualified C Programming Verifier (QCP), a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes.

4. Intuitive Verification of Sequential Programs Using Hybrid Reasoning

   Shushu Wu, Xiwei Wu, Chengxi Yang, and 1 more author

   2026

   In TASE 2026.

   Abs DOI

   Verifying the functional correctness of real-world code with complex algorithms requires reasoning about both implementation correctness and algorithm correctness. Implementation correctness, which relates concrete programs to abstract functional models, is inherently relational, yet is traditionally formalized using standard Hoare logic alone. This paper proposes a hybrid reasoning approach that combines relational Hoare logic and standard Hoare logic. Our key insight is that verifying implementation correctness naturally calls for relational Hoare logic, while algorithm correctness is well-suited to standard Hoare logic. Compared to traditional verifications that rely exclusively on standard Hoare logic, our approach simplifies proofs and offers more intuitive reasoning patterns. We demonstrate this in a setting where the concrete language is a C-like imperative language and the abstract algorithm is written in a simple nondeterministic functional language. Through case studies on binary search trees and merge sort, we show how our hybrid reasoning approach addresses challenges in verifying complex algorithms, reduces proof complexity, and enhances clarity.

2025

1. A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms

   Chengxi Yang^*, Shushu Wu^*, and Qinxiang Cao

   In Theoretical Aspects of Software Engineering, 2025

   Abs DOI arXiv

   Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algorithms with states and flexible control flow. For verification, formal proof based on Hoare logic cannot reflect the logical structure of natural proof. To address these challenges, we introduce a formal framework for naturally specifying and verifying sequential algorithms in Coq. We use the state relation monad to integrate Coq’s expressive type system with the flexible control flow of imperative languages. It supports nondeterministic operations and customizable program states, enabling specifying algorithms at an appropriate level of abstraction. For verification, we build a Hoare logic for the monad and propose a novel two-stage proof approach that separates natural logical reasoning from mechanical composition. It reflects the logical structure of natural proof, enhancing modularity and readability. We evaluate the framework by formalizing the Depth-First Search (DFS) algorithm and verifying the Knuth-Morris-Pratt (KMP) algorithm.