Showing cs.PLShow all
3 papers · 1 filter
cs.PL2026
Fixing the Fixpoint: A Formal Theory of Convergence Detection for Incremental Recursive Computation
Chengxi Yang, Tej Chajed, Thomas Reps
Modern incremental computation theories like DBSP have enabled efficient incrementalization of general recursive computations. To do so, they require a runtime Fixpoint Detection (…
cs.PL2025
QCP: A Practical Separation Logic-based C Program Verification Tool
Xiwei Wu, Yueyang Feng, Xiaoyang Lu +12
As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite signif…
cs.PL2025
A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
Chengxi Yang, Shushu Wu, Qinxiang Cao
Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algor…