2 papers
cs.PL2026
Denotation-based Compositional Compiler Verification
Zhang Cheng, Jiyang Wu, Di Wang +1
A desired but challenging property of compiler verification is compositionality, in the sense that the compilation correctness of a program can be deduced incrementally from that o…
cs.PL2025
C*: Unifying Programming and Verification in C
Yiyuan Cao, Jiayi Zhuang, Houjin Chen +8
Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite…