I'm currenty a lecturer/researcher at Software Engineering Department, School of Information and Communication Technology, Hanoi University of Science and Technology.

Post-doc at Verimag laboratory, working on ACROSS, a research project that aims to develop and implement an ARTEMIS cross-domain reference architecture for embedded systems. I am also working on the version 2.0 of D-Finder, a tool for compositional and incremental deadlock detection and verification of systems described in BIP (Behavior-Interaction-Priority) modeling language.

Ph.D. in Computer Science: I worked on theory, methods and tools for the compositional and incremental verification of component-based systems. I was the main developer of D-Finder V1.0. I also have experience in the component-based construction of complex systems.

Education

2006 - 2010 : Ph.D. student in Computer Science, Verimag Laboratory.
Thesis title : Constructive verification for component-based systems. Supervisors : Pr. Saddek Bensalem and Pr. Joseph Sifakis.

2005 - 2006 : Masters in Computer Science (Systems and Softwares), Grenoble Institute of Technology.

2002 - 2005 : Program of Excellent Engineering Training (P.F.I.E.V) in Computer Science, Ha Noi University of Technology.

2000 - 2002 : Program of Excellent Engineering Training (P.F.I.E.V), Preparatory Classes, Ho Chi Minh University of Technology.

1997 - 2000 : Special class of science, Lam Son high school, Thanh Hoa, Vietnam.

Professional Experience

Jan 06 - Sept 06 (9 months)

Masters Internship, Verimag Laboratory, working on modeling and validation of an autonomous robotic system, robot Dala developed at Laas Laboratory, in BIP.
Advisors: Pr. Saddek Bensalem and Pr. Joseph Sifakis

June 05 - Sept 05 (2 months)

Software Engineer, Prowess company, Hanoi, Vietnam, working on radiation cancer treatment planning software.

Jan 05 - June 05 (6 months)

Engineering Internship, Center for Development of Information Technology, Hanoi, Vietnam, working on encoder module for the transmission of video in mobile network.

Technical Skills

Operating Systems : Linux, MacOS, Microsoft Windows

Programming Languages : C, C++, Java, PHP, MySQL, HTML, Actionscript, Flex

Tools : BIP, Cudd, Omega, NuSMV, Spin, Yices

Text Processing : Latex, Microsoft Office

Languages : Vietnamese (native), English (fluent), French (fluent)

Research Activities

• Compositional Verification: Compositional approach is used to alleviate the state space explosion in the monolithic verification approaches. The idea is to apply “divide- and-conquer” techniques: a complex system is decomposed into sub-systems that are analyzed individually. The properties of the global system are then inferred from the verified properties of its subsystems. We have developed theory, methods and tools for compositionally proving safety properties of component-based systems described in the BIP (Behavior, Interaction, Priority) framework. Our method is based on the computation of an over-approximation of the reachable states using invariants: component invariants and interaction invariants. We provide efficient methods for computing such invariants.

• Incremental Verification: We also provide a method allowing incremental verification of safety properties. The method uses a formalization of the construction process of a composite component from a set of atomic components. Following the construction process, it decomposes the computation of global invariants of composite components into the computation of invariants of their constituent components. Then the invariants of the global system are computed from the invariants of its constituents.

• Incremental Construction of Robotic Systems: Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software com- ponents and must meet safety properties including in particular temporal and real-time constraints. We proposed a methodology for modeling and analyzing a robotic system using the BIP component framework integrated with an existing framework and architec- ture, the LAAS Architecture for Autonomous System, based on GenoM. We showed how it can be seamlessly integrated in the preexisting methodology. We provided the compo- nentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential safety properties.