| CARVIEW |
Select Language
HTTP/2 200
date: Fri, 16 Jan 2026 04:37:15 GMT
content-type: text/html
server: AtlassianEdge
last-modified: Mon, 01 Dec 2025 23:27:52 GMT
etag: W/"7a6eae88bf65443f584b52947d7ba766"
x-used-mesh: False
vary: Accept-Language, origin
content-language: en
x-view-name: bitbucket.apps.hosted.views.serve
x-dc-location: Micros-3
x-served-by: b9390e1994ed
x-version: c44cce1017f7
x-static-version: c44cce1017f7
x-request-count: 1687
x-render-time: 0.1445178985595703
x-b3-traceid: 2224e0d9892f4092ba4a33c82a2dd351
x-b3-spanid: 84ea3df779a2d50d
cache-control: max-age=900
x-usage-quota-remaining: 997406.312
x-usage-request-cost: 2634.57
x-usage-user-time: 0.071247
x-usage-system-time: 0.007790
x-usage-input-ops: 0
x-usage-output-ops: 0
content-encoding: gzip
x-content-type-options: nosniff
x-xss-protection: 1; mode=block
atl-traceid: 2224e0d9892f4092ba4a33c82a2dd351
atl-request-id: 2224e0d9-892f-4092-ba4a-33c82a2dd351
strict-transport-security: max-age=63072000; includeSubDomains; preload
report-to: {"endpoints": [{"url": "https://dz8aopenkvv6s.cloudfront.net"}], "group": "endpoint-1", "include_subdomains": true, "max_age": 600}
nel: {"failure_fraction": 0.01, "include_subdomains": true, "max_age": 600, "report_to": "endpoint-1"}
server-timing: atl-edge;dur=361,atl-edge-internal;dur=3,atl-edge-upstream;dur=359,atl-edge-pop;desc="aws-ap-south-1"
Le, Quang Loc
"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.
 |
Lê Quang LộcLecturer in Programming Principles, Logic, and Verification Group Department of Computer Science
University College London
Office: Room 310, 66-72 Gower St, London, UK, WC1E 6EA
Office hour: Thursday 14.00 - 15.00
Email: loc.le at ucl.ac.uk
|
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.
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 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] and
[here] for examples of PhD topics.
[Click here]for application process of UCL EPSRC Landcape scholarship and
[here]for application process of UCL CS scholarship.
Biography
- Lecturer, UCL, 2022 -
- Deputy Director of MEng in Mathematical Computations , UCL, 2025 -
- Research Scientist II (part time), Meta, 2020-2022
- Senior Lecturer, Teesside University, 2017-2020
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
- Vorashil Farzaliyev (2025 - )
- Chris Curry (2017 - 2020), (Now, lecturer at Teesside University)
Publications
PPLV Seminars
Awards/Honors
- ACM SIGPLAN Distinguished Paper Award, OOPSLA 2022.
- Global Young Scientists Summit 2015 Invitee.
- Dean's Graduate Research Excellence Award. NUS, 2014. (2013-14, Semester 2)
- 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 Meetings
- Schloss Dagstuhl Seminar 25441 on Competitions and Empirical Evaluations in Automated Reasoning. 26 – 31, October 2025, Germany.
- Schloss Dagstuhl Seminar 19371 on Deduction Beyond Satisfiability. 8 - 13 September 2019, Germany.
- Bertinoro Meeting on String Constraints and Applications. 6 – 9, May 2019. Bertinoro international Center for informatics (BiCi). University Residential Centre, Bertinoro, Italy.
- Shonan meeting No. 100. on Analysis and Verification of Pointer Programs.2 - 5, October 2017, Japan.
Invited Talks/Workshops
- Provably Finding Bugs in Big Programs with Incorrectness Logic. UCL-Huawei Trustworthy Software Engineering, UCL, London. March 2025.
- 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]
Short Courses
- Summer School: Incorrectness Logic and Underapproximation: Foundations of Bug Catching. Formosan Summer School on Logic, Language, and Computation. National Taiwan University. Aug 29, 2023.
- Tutorial Lecture: Incorrectness Logic and Underapproximation: Foundations of Bug Catching. TutorialFest POPL 2023 - Boston, Massachusetts, United States. Jan 2023
Research Software System: NS2 solver
- S2S: An Efficient Solver for Separation Logic.
Click here to go to the S2S website.
- 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 - Module Lead, 2025, 2026
- Compiler (COMP0012) @ UCL - 2024, 2025, 2026
- 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
Links
-
Demystify Good Research and Good Papers •
Advice on Research and Writing •
How to Be a Good Graduate Student
|
Last update: Mar-2020 |