I was eventually persuaded of the need to design programming notations so as to maximize the number of errors which cannot be made, or if made, can be reliably detected at compile time.

C.A.R. Hoare

About Me

I am a Research Scientist at Department of Computer Science, University of Houston. My main research interest is automated and scalable techniques for program analysis and formal verification, including the problems of program termination and non-termination, memory safety, resource consumption, and program security. I am also interested in theorem proving, constraint solving, and the use of formal methods in big data analytics, machine learning, and blockchain technology.


Research Projects

  • Songbird - An automated inductive theorem prover for Separation Logic

  • Automated Specification Discovery for Trusted Software (2014 - 2017)

  • Specification and Verification for Future Programmers (2009 - 2013)



  • Automated Lemma Synthesis in Symbolic-Heap Separation Logic
    Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
    The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'18),
    ACM, Los Angeles, California, United States, January 7 - 13, 2018.
    [ SLS | Technical report ]

  • Automated Mutual Explicit Induction Proof in Separation Logic
    Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
    The 21st International Symposium on Formal Methods (FM'16),
    Springer-Verlag, Limassol, Cyprus, Nov 7 - 11, 2016.
    [ Songbird | Technical report ]

  • Termination and Non-Termination Specification Inference ACM DL Author-ize service
    Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin
    The 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'15),
    ACM, Portland, Oregon, United States, June 13 - 17, 2015.
    [ HipTNT+ | pdf ]

  • A Resource-Based Logic for Termination and Non-Termination Proofs
    Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, and Wei-Ngan Chin
    The 16th International Conference on Formal Engineering Methods (ICFEM'14),
    Springer-Verlag, Luxembourg, Nov 3 - 7, 2014.
    [ HipTNT | Technical report ]

  • A Proof Slicing Framework for Program Verification
    Ton Chanh Le, Cristian Gherghina, Razvan Voicu, and Wei-Ngan Chin
    The 15th International Conference on Formal Engineering Methods (ICFEM'13),
    Springer-Verlag, Queenstown, New Zealand, Oct 29 - Nov 1, 2013.
    [ Technical report ]



  • Winner of the C Integer Programs category (summary result) in the annual Termination Competition 2015, affiliated with the CADE-25 conference.

  • Bronze medal in the Termination category, winner of the termination-crafted-lit division, 4th Intl. Competition on Software Verification held at TACAS 2015 (SV-COMP'15) (jury member of team HipTNT+)

  • Winner of the UDB_sat division, 1st Separation Logic Competition (SL-COMP'14), in conjunction with SMT-COMP 2014 (member of team SLEEK)

  • The Honda Young Engineer and Scientist (Y-E-S) Award, 2009




  • PC member: SV-COMP'15, SV-COMP'17

  • Additional reviewer: ATVA'10, VMCAI'12, CPP'12, ATVA'13, SAS'13, FM'14, ICALP'15, FAOC, OOPSLA'16, RV'16, CAV'17, VMCAI'17




LE, Ton Chanh

Research Scientist
Department of Computer Science
University of Houston
Email: letonchanh at gmail dot com