Information
I am a Ph.D. student in Computer Science at Uppsala University, Sweden (2014-now). My supervisors are Dr. Mohamed Faouzi Atig
, Prf. Parosh Aziz Abdulla, and Dr. Philipp Rümmer. I am a member of the Algorithmic Program Verification group and UPMARC center.
Before I was a master student at Uppsala University (2011-2013), and a teaching assistant at Hanoi University of Science and Technology (2009-2011). I graduated from Hanoi University of Science and Technology, Vietnam (2004-2009).
Research interests
I am working on development of algorithms and tools for ensuring correctness of multi-threaded programs running on top of multicore memory models or relaxed cache coherence protocols.
Tools
- Dual-TSO: Dual-TSO is a tool that precisely and soundly checks safety properties of (parameterised) concurrent programs under Total Store Order Memory models (TSO).
- PSO Memorax: PSO-Memorax is a tool that precisely and soundly checks safety properties of concurrent programs under Partial Order Memory models (PSO), and find smallest sets of fences to correct the programs (if these sets exist).
- PERSIST: PERSIST is a tool that checks the Persistent property of concurrent programs under Total-Store-Order memory model such as in Intel x86 and fixes erroneous programs by inserting fences. Persistence is a weaker definition than data race, and defined by program order and total store order. Following the link, you will know how to download and install, and run many programs with PERSIST.
Publications
- The Benefits of Duality in Verifying Concurrent Programs under TSO, Abdulla Parosh Aziz, Atig Mohamed Faouzi, Ahmed Bouajjani, and Ngo Tuan Phong. In 27th International Conference on Concurrency Theory, CONCUR 2016, Quebec, Canada, 2016.
- Precise and Sound Automatic Fence Insertion Procedure under PSO, Abdulla Parosh Aziz, Atig Mohamed Faouzi, and Ngo Tuan Phong. In Networked Systems: NETYS 2015, Lecture Notes in Computer Science, Springer Berlin/Heidelberg, Agadir, Morocco, 2015.
- The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO, Abdulla Parosh Aziz, Atig Mohamed Faouzi, and Ngo Tuan Phong. In 24th European Symposium on Programming, ESOP 2015, volume 9032 of Lecture Notes in Computer Science, pp 308-332, Springer Berlin/Heidelberg, London, UK, 2015.
- Ensuring the Correctness of Concurrent Programs under TSO Memory Models, Master thesis, supervisor: Mohamed Faouzi Atig, examiner: Parosh Abdulla, Ivan Christoff, IT nr 13 085, 2013 (fulltext
).
Teaching
| Course | Code | Year | Period |
|---|---|---|---|
| Programming Theory | 1DT034 | 2016 | VT1-2 |
| Automata and Logic IT-system modeling | 1DL500 | 2016 | VT2 |
| Algorithms and Data Structure 1 | 1DL210 | 2016 | VT1 |
| Automata and Logic IT-system modeling | 1DL500 | 2015 | VT2 |
| Algorithms and Data Structure 1 | 1DL210 | 2015 | VT1 |
| Algorithms and Data Structure 1 | 1DL210 | 2014 | VT1 |