My research interests are in formal methods, especially ML-based safety-critical applications such as autonomous driving software, programming languages, compilers, and language-based security.

I received my Engineer degree (equivalent to Diplôme d’Ingénieur) from Hanoi University of Technology with excellent ranking, my M.Sc in Computer Science (under a French government scholarship, Évariste Galois program) from Joseph Fourier University (Université de Grenoble), and my Ph.D from Inria France under the supervision of Dr. Jean-Pierre Talpin.

I am interested in building reliable and secure computer systems by developing formal frameworks which guarantee that software satisfies formally its specification, especially embedded safety-critical software such as automotive, avionic, and health-care applications. The construction of a formal framework involves the research and knowledge of principles of programming languages, compiler design and development, and formal methods including model checking, theorem proving, and static analysis for providing formal assurances that the specification is fulfilled.

A common theme is constructing correct Machine Learning-based safety-critical systems such as autonomous vehicles by applying formal verification including static analysis, model checking and correctness proof on the source code implementation, or mathematical models of these systems. One of the application is the correctness and robustness analysis of localization, perception, and motion planning software modules in the autonomous software stack. Another application is providing analysis w.r.t the safety standards such as ISO-26262-6 and SOTIF.