Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets. - Xiaojie Guo 003; Sophie Quinton; Pascal Fradet; Jean-François Monin (RTSS, 2017)

A Generalized Digraph Model for Expressing Dependencies. - Pascal Fradet; Xiaojie Guo 003; Jean-François Monin; Sophie Quinton (RTNS, 2018)

Integrating Formal Schedulability Analysis into a Verified OS Kernel. - Xiaojie Guo 003; Maxime Lesourd; Mengqi Liu 001; Lionel Rieg; Zhong Shao 001 (CAV (2), 2019)

CertiCAN: A Tool for the Coq Certification of CAN Analysis Results. - Pascal Fradet; Xiaojie Guo 003; Jean-François Monin; Sophie Quinton (RTAS, 2019)

Certified Tools for Schedulability Analyses. (Outils certifiés pour les analyses d'ordonnançabilité). - Xiaojie Guo 003 (2020)

A generic approach for the certified schedulability analysis of software systems. - Xiaojie Guo 003; Lionel Rieg; Paolo Torrini (RTCSA, 2021)

CertiCAN certifying CAN analyses and their results. - Pascal Fradet; Xiaojie Guo 003; Sophie Quinton (Real Time Syst., 2023)