About me

I am a postdoctoral research fellow working with Professor Beng Chin Ooi at School of Computing, National University of Singapore (NUS). I obtained my BSc (1st Class Honors) from Hanoi University of Science and Technology (HUST), Vietnam in 2009 and PhD from NUS, Singapore in 2018. My PhD advisors are Professor Siau-Cheng Khoo and Professor Wei-Ngan Chin. I also worked previously in industry on computer security at BKAV, software development at A.N.Lab, Viettel, and FPT, and static software analysis at Oracle Labs Australia.

My email is: taqt [at] comp.nus.edu.sg. Here are my CVs: long CV / short CV.

Recent News

• Nov 11, 2020: Our paper Automated Repair of Heap-Manipulating Programs using Deductive Synthesis was accepted to International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2021. Congratulations to Toan!

• Mar 14, 2020: Our paper A Transactional Perspective on Execute-order-validate Blockchains was accepted to ACM International Conference on Management of Data (SIGMOD) 2020. Congratulations to Pingcheng!

• Feb 06, 2020: My first patent Buffer Overflow Detection Based on A Synthesis of Assertions from Templates and K-Induction was published by the United States Patent and Trademark Office.

Research

I do research in programming languages, software engineering, security, AI, blockchain, database, and networking. My current projects are on formal verification and analysis of smart contracts and 5G mobile network. During my PhD, I developed the theorem prover Songbird for proof obligations generated from automated software verification using separation logic. It is now used as a backend of the tool Hip/Sleek to verify C/C++/Java programs.

The followings are the highlights of my recent work. More details are available in this page.

Papers:

• Automated Mutual Explicit Induction Proof in Separation Logic. FM 2016.

• Automated Lemma Synthesis in Symbolic-Heap Separation Logic. POPL 2018.

• Automatic Program Repair Using Formal Verification and Expression Templates. VMCAI 2019.

• The Disruptions of 5G on Data-driven Technologies and Applications. TKDE 2020.

• A Transactional Perspective on Execute-order-validate Blockchains. SIGMOD 2020.

• Automated Repair of Heap-Manipulating Programs using Deductive Synthesis. VMCAI 2021.

Patents:

• Buffer Overflow Detection Based on A Synthesis of Assertions from Templates and K-Induction.
  United States Patent and Trademark Office 2020.

Teaching

I always enjoy teaching and mentoring junior students. I was inspired by Professor Olivier Danvy’s belief that watching students grow is a joy. I also couldn’t agree more with Professor Richard Feynman that teaching is a great way to learn. Below are the teaching tasks that I have taken recently.

Teaching Assistant:

• CS5218, Principles of Program Analysis, School of Computing, NUS, 2015.

• YSC1212, Introduction to Computer Science, Yale-NUS College, NUS, 2016.

• CS6203, Advanced Topics in Database Systems, School of Computing, NUS, 2019.

Research Mentor:

• Nguyen Thi Tuyet Mai, final year undergraduate, HUST, 2009 - 2010. Topic: SAT solving system.

• Pham Anh Tuan, exchanged undergraduate of HUST at NUS, 2012. Topic: Type inference system.

• Zhu Yongxin, final year undergraduate, NUS, 2014 - 2015. Topic: Eclipse IDE-based GUI development.

• Nguyen Thanh Toan, PhD student, NUS, 2017 - present. Topic: Automated program repair.

• Zhong Yuyi, PhD student, NUS, 2019 - present. Topic: Verification of machine learning algorithms.

• Ren Kunpeng, Master student, Peking University, 2019 - present. Topic: Smart contracts verification.

Services

• Subreviewer: CPP 2012, SAS 2013, ICFEM 2013, FM 2014, APLAS 2014, ICALP 2015, OOPSLA 2016, SV-COMP 2018, APLAS 2018, FLOPS 2018, CAV 2018, SEFM 2018, ATVA 2018, TACAS 2019, CAV 2019, ATVA 2019, ICDE 2020, SIGMOD 2020, KDD 2020, VLDB 2020, VLDB 2021.

• Administrator: the online forum ITBK for undergraduate students at School of Information and Communication Technology, HUST, 2007 - 2010.

Miscellaneous

• I am a big fan of the Emacs editor, especially the Spacemacs distribution. I use it for most of my works. If you are curious about what Emacs can do, please check out this summary or my slides. If you want to try out Emacs, my Spacemacs starter kit could provide some helps.

• Merry Christmas and Happy New Year à la JavaScript.