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 Fellow at Department of Computer Science, National University of Singapore. My research interests are program analysis and verification, automated reasoning and specification, focusing on termination and non-termination reasoning and detecting security vulnerabilities in heap-manipulating programs using separation logic.

 

Research Projects

  • Automated Specification Discovery for Trusted Software (2014 - 2017)
    Currently, we are working on program termination and non-termination inference, that follows from our prior work of a specification logic for termination and non-termination reasoning (online verification system HipTNT, inference system HipTNT+ and tutorial).

  • Specification and Verification for Future Programmers (2009 - 2013)
    I am involving the development of the HIP/SLEEK verification system. We have proposed a formal framework for proof slicing mechanisms to enhance program verification by aggressively reducing the size of proof obligations.

 

Publications

  • 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 ]

 

Awards

  • 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

 

Others

Service

  • PC member: SV-COMP'15

  • Additional reviewer: ATVA'10, VMCAI'12, CPP'12, ATVA'13, SAS'13, FM'14, ICALP'15, FAOC


Teaching

 

Contact

LE, Ton Chanh

Research Fellow
Department of Computer Science
School of Computing
National University of Singapore
Programming Languages & Software Engineering Lab
COM2 #04-04
15 Computing Drive, Singapore 117418

Email: chanhle at comp.nus.edu.sg