Le, Quang Loc

Lê Quang Lộc

Lecturer in Programming Principles, Logic, and Verification Group

Department of Computer Science

Office: Room 310, 66-72 Gower St, London, UK, WC1E 6EA

Email: loc.le at ucl.ac.uk

"The whole of science is nothing more than a refinement of everyday thinking". Albert Einstein

My research focuses on automatic, effective methods for finding bugs in real codebase.
We have used an approach based on bug-reporting criterion, bi-abduction, and incorrectness logic.
The following paper gives technical details and initial results.

Finding Real Bugs in Big Programs with Incorrectness Logic.

Proc. ACM Program. Lang. 6 (OOPSLA 2022)

I am looking for PhD students (two scholarships are available). If you know how to hack, we should meet.
[Click here]for an example of topics and studentships. [Click here]for another example of topics and studentships. [Click here]for application process.

Education

Ph.D. Computing, National University of Singapore, 2014
B.Sc. Computer Science & Engineering, Vietnam National University - Ho Chi Minh University of Technology, 2005

PhD Students

Ekaterina Piotrovskaya (2024 - )

Chris Curry (2017 - 2020), (Now, lecturer at Teesside University)

Publications

Awards/Honors

ACM SIGPLAN Distinguished Paper Award, OOPSLA 2022.
Global Young Scientists Summit @One-North 2015 Invitee.
Deans Graduate Research Excellence Award. NUS, 2014.
PhD. Scholarship. School of Computing - NUS, Jan 2010- Dec 2013
3rd prize @ Vietnam Summer Code competition 2009 for students in Vietnam (role: mentor) by Vietnam Ministry of Science and Technology, 2009.

Invited Talk/Workshop

Finding Bugs in Software with Incorrectness Logic. Huawei Hong Kong Formal Methods Workshop. Hong Kong Science Park. June 2024.
Incorrectness Logic and Underapproximation: Foundations of Bug Catching. Formosan Summer School on Logic, Language, and Computation. National Taiwan University. Aug 2023. [slides]
Compositional Incorrectness Proving at Scale. School of Computing - National University of Singapore. Aug 2023.
Finding Real Bugs in Big Programs with Incorrectness Logic. Department of Computer Science, University of Bristol, UK. June 2023.
Finding Real Bugs in Big Programs with Incorrectness Logic. Brno University of Technology, Czech Republic. May 2023.
Incorrectness Logic and Underapproximation: Foundations of Bug Catching. TutorialFest POPL 2023 - Boston, Massachusetts, United States. Jan 2023.
Finding Real Bugs in Big Programs with Incorrectness Logic. KLEE workshop. Imperial College London. September 2022.
Finding Real Bugs in Big Programs with Incorrectness Logic. Infer workshop at PLDI 2022. June 13, 2022.
Cyclic Satisfiability Proofs in Separation Logic. The 4th Working Formal Methods Symposium. September 4-6, 2020 (virtual).
Inductive Inference with Recursion Analysis in Separation Logic. at Schloss Dagstuhl 19371 "Deduction Beyond Satisfiability". 8-13 September 2019 - Germany.
Meeting on String Constraints and Applications. 6-9 May 2019 - Bertinoro, Italy.
Test Case Generation for Heap Inputs using Separation Logic. at NII Shonan Meeting on "Analysis and Verification of Pointer Programs". 2-5.Oct 2017 - Japan. [slides]
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. at National Institute of Informatics, Tokyo- Japan. March-2017. [slides]
A Decision Procedure for String Logic with Equations, Regular Membership and Length Constraints. at University of Waterloo, hosted by Vijay Ganesh.Oct-2016. [slides]
Satisfiability Modulo Heap-Based Programs. Automata, Logic and Games. IMS-NUS. Aug-2016. [slides]

Research Software System: NS2 solver

S2S

here

S2S performed very well at SLCOMP 2019:
- S2S won Gold Medal overall (Click here for the report at TOOLympics @ETAPS 2019)
- Out of 9 divisions, S2S won
  - the first prize at 7 divisions: qf_shid_sat, qf_shid_entl, qf_shlid_entl, shid_entl, qf_shidlia_entl, qf_shidlia_sat, shidlia_entl.
  - the second prize at 2 divisions: qf_shls_entl, qf_shls_sat.
SLCOMP 2018: S2S performed well in 5 divisions: qf_shidlia_sat, qf_shlid_entl, qf_shls_entl, qf_shls_sat, qf_shid_sat.

Teaching

Theory of Computation (COMP0003) @ UCL - 2024 (Autumn)
Compiler (COMP0012) @ UCL - 2024 (Spring, Autumn)
Practical Program Analysis (COMP0174) @ UCL - 2023 (Spring)
Introduction to Programming (COMP0015) @ UCL - 2022 (Autumn), 2023 (Autumn, Spring), 2024 (Spring)
Software Reliability, Information System and Security, Research Method @ Teesside University
Guest Lecture- Software Engineering (50.530) - SUTD, Automatic Verification using Separation Logic. [slides]
TA, CS2104, Programming Language Concepts, SoC-NUS, Fall 2011-2012-2013