• I am a Compiler engineer at IAR Systems Group AB. I have been working in a compiler team to make IAR Embedded Workbench compiles more efficient and smarter.

• In Oct 2019 - Sep 2020, I worked as a C/C++ developer at COMSOL AB. I worked in a brilliant team to solve practical and challenging problems related to geometry, virtual geometry operation, mesh generation, and graphical visualization.

• In Jun 2019 - Oct 2019, I worked as a software verification engineer at IAR Systems Group AB. I developed an extension for the verification engine inside IAR Visual State, targeting to real-world models (such as from Siemens and Panasonic). The topics include State machine, Software verification, Symbolic model checking, and Binary Decision Diagram (BDD).

• In March 2019 - May 2019, I worked as a reseacher in Department of Information Technology at Uppsala University. My Google scholar profile is Tuan Phong Ngo - Google scholar. Some of my publications and taks can also be found in Publications and in Talks.

• From Nov 2013 - Jan 2019, I was a Ph.D. student in Department of Information Technology at Uppsala University and a member of Algorithmic Program Verification group. I worked on the development of model checking algorithms and implementation of tools for verifying the correctness of concurrent programs running under weak memory models (e.g., Intel x86-TSO or IBM POWER), relaxed cache coherence protocols, or programming languages (e.g., C/C++11). My thesis supvervisors are Prof. Parosh Aziz Abdulla, Dr. Mohamed Faouzi Atig, and Dr. Philipp Rümmer. I defended my thesis with title Model Checking of Software Systems under Weak Memory Models in Jan 2019. My work is funded by UPMARC research center.

• In 2011-2013, I studied a Master program in Computer Science in Department of Information Technology at Uppsala University with an Erasmus Mundus scholarship. My thesis supervisor is Dr. Mohamed Faouzi Atig. You can see the list of my courses and results in my transcript .

Recent News

• 1 Sep 2020. I completed my work and left COMSOL AB to start a new journey. Now, I am working as a C/C++ developer - Compiler optimization for ARM at IAR Systems AB.
• 7 Oct 2019. I have been working as a C/C++ mesh algorithm developer at COMSOL AB.
• 4 Oct 2019. I finished a project work at IAR Systems. My verification project was interesting and proved to be very sucessful. I developed several new features and improved the performance of the verification engine inside Visual State.
• Aug 10, 2019. A paper titled “Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency” was accepted in OOPSLA’19.
• 1 Jun 2019. I started my job as a software verification engineer at IAR Systems.
• March 2019 - May 2019. I worked as a reseacher in Department of Information Technology at Uppsala University. I collaborated with Prof. Bengt Jonsson and Dr. KonstantinosSagonas. My Google scholar profile can be found in Tuan Phong Ngo - Google scholar.
• 21 Jan, 2019. I defended my thesis and open for job opportunities in Sweden.
• Oct 12, 2018. I served on the AEC of TACAS’19.
• Nov 4 - Nov 9, 2018. I attended SPLASH’18 held in Boston, USA for a talk on our optimal stateless model checking technique for concurrent programs running under the Release-Acquire memory model. You can watch my video presentation .
• Aug 16, 2018. A paper titled “Optimal Stateless Model Checking under The Release-Acquire Semantics” was accepted in OOPSLA’18.
• Jan 23, 2018: A journal paper titled “A Load-Buffer Semantics for Total Store Ordering” was accepted in LMCS. This is an extension of our CONCUR’16 paper “The Benefits of Duality in Verifying Concurrent Programs under TSO”.
• Apr 22 - Apr 29, 2017. I attended ETAPS’17 held in Uppsala, Sweden for a talk on our context-bounded model checking technique for concurrent programs running under the POWER memory model.
• Jan 20, 2017. Our TACAS’17 paper “Context-bounded Analysis for POWER” was nominated as one of the best papers in ETAPS’17.
• Dec 22, 2016. A paper titled “Context-bounded Analysis for POWER” was accepted in TACAS’17.
• Oct 2, 2016: We got an invitation to submit a journal version of our CONCUR’16 paper “The Benefits of Duality in Verifying Concurrent Programs under TSO” to the special issue of LMCS devoted to the conference.
• Aug 23 - Aug 26, 2016. I attended CONCUR’16 held in Quebec, Canada for a talk on our novel Dual TSO memory model and its application to (parameterized) verification of concurrent programs running under the TSO memory model.
• Jun 10, 2016. A paper titled “The Benefits of Duality in Verifying Concurrent Programs under TSO” was accepted in CONCUR’16.
• May 13 - May 15, 2015. I attended NETYS’15 held in Agadir, Morocco for a talk on our fence insertion technique to automatically correct concurrent programs running under the PSO memory model.
• Mar 16, 2015. A paper titled “Precise and Sound Automatic Fence Insertion Procedure under PSO” was accepted in NETYS’15.
• Apr 14 - Apr 16, 2015. I attended ESOP’15 held in London, UK for a talk on our fence insertion technique to automatically correct concurrent programs running under the TSO memory model.
• Feb 23 - Feb 24, 2015. I attended MM’15 held in Uppsala, Sweden for a talk on our fence insertion technique to automatically correct concurrent programs running under the TSO model.
• Dec 14, 2014. A paper titled “The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO” was accepted in ESOP’15.
• Nov 2013, I worked as Ph.D student at Uppsala University. I worked on the topic Model Checking of Software Systems under Weak Memory Models. My thesis supvervisors are Prof. Parosh Aziz Abdulla, Dr. Mohamed Faouzi Atig, and Dr. Philipp Rümmer. I am funded by UPMARC research center in five years.
• Aug 2011, I started a new chapter in my file by going to Sweden and studying a Master program in Computer science in Department of Information Technology at Uppsala University with an Erasmus Mundus scholarship.