I am a PhD student at EPFL, working with Prof. Clément Pit-Claudel in the SYSTEMF lab.
My current research focuses on program verification, with a particular interest in making it easier to verify shared and mutable data structures.
I often find myself easily (and happily) distracted by related topics in programming languages and type theory.
About my name
My given name is 雅雯, 雅 is a traditional aesthetic ideal ("elegance"), and 雯 means streaked or patterned clouds.
In everyday life, I go by Miya as the short form of Miyabi (雅・みやび in Japanese), as it is easy to pronounce and carries the same meaning.
Publications
-
Reasoning About Container-Internal Pointers with Logical Pinning 📄 [preprint] 💻 [development]Yawen Guan, Clément Pit-ClaudelProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2026).🏅Distinguished paper.
Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs.
We present logical pinning, a lightweight borrowing model for sequential programs that allows users to selectively track container-internal pointers at the logical level. Our model generalizes the magic-wand operator for representing partial data structures, making it easy to write and prove precise specifications, including pointer-stability properties. Because it only changes the way representation predicates and specifications are written, our approach is compatible with most separation logic variants.
We demonstrate the practicality of logical pinning by verifying small but representative pointer-manipulating programs, and deriving more precise versions of common container specifications. In doing so, we show that our approach subsumes some well-known proof patterns, simplifies some complex proofs, and enables reasoning about program patterns not supported by traditional specifications. All of our results are mechanized in the Rocq proof assistant, using the CFML library.
-
Tracking Dynamically Bound Variable Dependencies 💻 [development]Theory and Practice of Static Analysis (TPSA 2026).
Some Lisp dialects rely heavily on "action at a distance" through dynamically bound variables. We present an analysis that approximates the transitive dynamic-variable dependencies of Emacs Lisp programs, as well as those of Emacs Lisp primitives written in C. Applied to the Emacs code base and 210 popular Elisp libraries, our prototype implementation surfaces subtle bugs and reveals unexpectedly large dynamic-variable dependency sets.