About me
I am a
postdoctoral research fellow working with Professor Ooi Beng Chin 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 (supervised by Professor Khoo
Siau Cheng and Professor Chin Wei
Ngan) from NUS in 2018. 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 address is: taqt [at] comp.nus.edu.sg. Here are my CVs: short (2 pages), and long (5 pages).
News
-
Nov 2019. I gave a vision talk on the disruption of 5G on data-driven applications and technologies at The Institution of Engineers, Singapore. [paper]
-
Nov 2019. Job openings (Research Assistant, Research Engineer, Research Fellow) in my Database System Research Group at NUS Computing.
Awards
-
My prover Songbird was the winner of the competition for separation logic provers SL-COMP 2018.
-
I received the Research Achievement Award by School of Computing, NUS in 2018.
-
I was the valedictorian of the undergraduate class of 2009 at School of Information and Communication Technology, HUST (GPA: 8.69/10).
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 (Fabric#) and 5G mobile network (5GEdgelet). 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 following papers are the highlights of my recent work. More details are available in this page.
-
The Disruptions of 5G on Data-driven Technologies and Applications. Accepted to TKDE 2020.
-
The Type Errors of Our Ways: A Quantitative Approach. Accepted to pre-proceedings, IFL 2019.
-
Automatic Program Repair Using Formal Verification and Expression Templates. VMCAI 2019.
-
Automated Lemma Synthesis in Symbolic-Heap Separation Logic. POPL 2018.
-
Automated Mutual Explicit Induction Proof in Separation Logic. FM 2016.
Teaching and Services
-
Teaching Assistant: (1) CS5218, Principles of Program Analysis, School of Computing, NUS, 2015. (2) YSC1212, Introduction to Computer Science, Yale-NUS College, NUS, 2016. (3) CS6203, Advanced Topics in Database Systems, School of Computing, NUS, 2019.
-
Research Mentor: (1) Nguyen Thi Tuyet Mai, final year undergraduate, HUST, 2009 - 2010. (2) Pham Anh Tuan, exchanged undergraduate of HUST at NUS, 2012. (3) Zhu Yongxin, final year undergraduate, NUS, 2014 - 2015. (4) Nguyen Thanh Toan, PhD student, NUS, 2017 - present. (5) Zhong Yuyi, PhD student, NUS, 2019 - present. (6) Ren Kunpeng, Master student, Peking University, 2019 - present.
-
External Reviewer: 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, CAV 2019, ICDE 2020, SIGMOD 2020.
-
Administrator: the online forum ITBK for undergraduate computer science students at HUST, 2007 - 2010.