Publications

You can also find my articles on my Google Scholar profile.

Conference Papers

Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle

Published in FSE 25, 2025

A software engineering work for proof repair over Isabelle.

Authors: Xiaokun Luan, David Sanan, Zhe Hou, Qiyuan Xu, Chengwei Liu, Yufan Cai, Meng Sun
Download Paper | Download Bibtex

Generically Automating Separation Logic by Functors, Homomorphisms, and Modules

Published in POPL 25, 2025

Several generic abstract algebras for Separation Logic predicates are found, above which generic automations are built to reason about data structures and algorithms

Authors: Qiyuan Xu, David Sanan, Zhe Hou, Xiaokun Luan, Conrad Watt, Yang Liu
Download Paper | Download Slides | Download Bibtex