I am working as a researcher in the School of Computer Science, and am a member of the Principles of Programming Group at Carnegie Mellon University. My research interests are in formal methods, 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 embedded systems (i.e., control software in safety-critical systems, embedded system hardware designs) by applying formal verification including static analysis, model checking and correctness proof on the source code implementation, or mathematical models of these systems producing by model-based design tool-chains, and formally certifying the correctness of the compilers and code generators in the model-based design tool-chains.