@inproceedings{chen2026conflict,author={Chen, Siyu and Sung, Chungha and Li, Xuyang and Wang, Jingbo},title={Conflict Extraction in Probabilistic Datalog Analyses},booktitle={41st IEEE/ACM International Conference on Automated Software Engineering},year={2026},note={Accepted; to appear.},}
FMCAD 2026
PSoufflé: Scaling Exact Probabilistic Logic Inference for Program Analysis
Xuyang Li*, Jiahao Xia*, Ahmed Adnan, and Jingbo Wang
In Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design, 2026
@inproceedings{li2026psouffle,author={Li*, Xuyang and Xia*, Jiahao and Adnan, Ahmed and Wang, Jingbo},title={PSouffl{\'e}: Scaling Exact Probabilistic Logic Inference for Program Analysis},booktitle={Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design},year={2026},publisher={TU Wien Academic Press},pages={372--378},doi={10.34727/2026/isbn.978-3-85448-093-8_42},note={* Equal contribution.},}
CAV 2026
Incremental Inference for Probabilistic Datalog
Xuyang Li, Weiyi Chen, Isil Dillig, and Jingbo Wang
@inproceedings{li2026incremental,author={Li, Xuyang and Chen, Weiyi and Dillig, Isil and Wang, Jingbo},title={Incremental Inference for Probabilistic Datalog},booktitle={Computer Aided Verification},year={2026},series={Lecture Notes in Computer Science},volume={16684},publisher={Springer},pages={169--190},doi={10.1007/978-3-032-32537-2_8},}
2024
TASE 2024
Verified Validation for Affine Scheduling in Polyhedral Compilation
Xuyang Li, Hongjin Liang, and Xinyu Feng
In Theoretical Aspects of Software Engineering, 2024
Structural nested loops can be abstracted into polyhedral models, based on which one can perform aggressive loop optimizations; however, the optimizations are often heuristic and complex, and therefore error-prone. Meanwhile, verified compilers, though rigorously correct, still miss powerful optimizing transformations and therefore produce less efficient code than industrial ones. To bridge this gap, this work provides a general verified validation framework based on Bernstein’s conditions for affine scheduling, the core component of polyhedral optimization techniques. It is parameterized over the concrete definitions and proofs of the instruction language to be reusable. As shown in our evaluation, the framework is flexible enough to support both existing verified compilers like CompCert and existing polyhedral compilers like Pluto. The result is fully mechanized in the Coq proof assistant.
@inproceedings{10.1007/978-3-031-64626-3_17,author={Li, Xuyang and Liang, Hongjin and Feng, Xinyu},editor={Chin, Wei-Ngan and Xu, Zhiwu},title={Verified Validation for Affine Scheduling in Polyhedral Compilation},booktitle={Theoretical Aspects of Software Engineering},year={2024},publisher={Springer Nature Switzerland},address={Cham},pages={287--305},isbn={978-3-031-64626-3},}