I am currently a Ph.D. student in SPADES team at Inria Grenoble and in PACSS team at Verimag. My advisors are Pascal Fradet, Jean-François Monin and Sophie Quinton. I work on formal proofs for real-time systems analysis. Recently, my main focus has been on providing formal guarantees to the results of industrial analysis tools.
Before starting my Ph.D., I received a master degree in Computer Science and Electronics for Embedded Systems (its French name is IESE and former name is 3i) from Polytech Grenoble in 2016 and a Bachelor degree from Wuhan University in 2013.
Projects
Formal Proofs for Real-Time Systems
I participate in RT-PROOFS project which aims to build the foundations for computer-assisted verification of real-time systems analysis and which is a joint effort of INRIA, MPI-SWS, TU Braunschweig, and Verimag.
CASERM: Design and Analysis of Reconfigurable Multi-View Embedded Systems
I participate in CASERM project which aims at building a Coq-based design, analysis, and verification framework for reconfigurable multi-view embedded systems and which is a joint effort of INRIA, LIG, and Verimag.
Publications
X. Guo, M. Lesourd, M. Liu, L. Rieg, Z. Shao. Integrating Formal Schedulability Analysis into a Verified OS Kernel. In 31st International Conference on Computer Aided Verification (CAV), 2019. [PDF]
P. Fradet, X. Guo, J.-F. Monin, and S. Quinton. CertiCAN: A Tool for the Coq Certification of CAN Analysis Results. In 25th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), 2019. [PDF]
P. Fradet, X. Guo, J.-F. Monin, and S. Quinton. A Generalized Digraph Model for Expressing Dependencies. In 26th International Conference on Real-Time Networks and Systems (RTNS), 2018. [PDF]
X. Guo, S. Quinton, P. Fradet, and J.-F. Monin. Work-in-progress: Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets. In 38th Real-Time Systems Symposium (RTSS), 2017, short paper. [PDF]
