2 citations · 2 across the 1 of their papers we have counts for
2 papers
cs.PL2026
Verification of a Generational Garbage Collector
Shengyi Wang, Kathrin Stark, Andrew W. Appel
We have formally verified in Rocq+VST a multi-generation collector with support for mutable references, written in C and compatible with OCaml data types. Its carefully specified A…
cs.PL2019★ 2 cited
VST-A: A Foundationally Sound Annotation Verifier
Litao Zhou, Jianxing Qin, Qinshi Wang +2
Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where…