- (Dec'18) Two papers accepted for
presentations at POPL'19.
- (May'18) I will be chairing the PC of ICECCS'18 with Jun Sun, to be held
in Melbourne (Australia) this December. I will also be chairing the PC of
APLAS'19 to be held in Indonesia. Please submit your best papers!
- (Nov'17) Our new string solver
Sloth that combines
regular constraints, and length constraints to be presented at POPL'18.
- (Oct'17) I have PhD studentships and postdoc positions
for those who have
solid backgrounds in PL and/or formal methods. The projects are on two different
topics: (i) algorithmic verification of string manipulating programs (including
developing constraint solvers over the string domain), and (ii)
analysis of Cascading Style Sheets. Email me if you are interested.
- (Sept'17) Papers on string solving accepted
- (Sept'17) I have been awarded an ERC Starting Grant. Thanks to everyone who
- (July'17) New paper accepted at FMCAD'17 on learning to prove safety over parameterised concurrent systems
- (Feb'17) Thanks to Google for the Faculty Research Award
for a project on Cascading Style Sheet Minification (with M. Hague as a co-PI)
- Please submit your best work to LICS 2018
My research interests lie in the development of logical methods for
programming technologies, which includes constraint
solving (especially, over the string domain), formal verification, and
program analysis, especially motivated by problems in (i)
web security/optimisation, (ii) analysis of concurrent programs with many
processes, and (iii) databases.
I am interested in all aspects of the field, ranging from theory to systems.
In particular, I strongly believe in the importance of theory, tool
construction, and case studies to make serious research advances.
- Current research projects:
- Constraint solving and program analysis for the Web:
- String solving for vulnerability detection in web
- Web performance optimisation, e.g., detecting redundant CSS
- Verification of sequential and concurrent programs:
- Parameterised systems: reasoning about an unbounded number
- Systematic testing and debugging via model checking
- Regular model checking
- Past projects:
- Some tools:
- OSTRICH -
hitherto the fastest string solver that supports concatenation,
replaceall, regular constraints, and other complex string
operations like transducers.
- Sloth - a
new string solver that combines concatenation, transducers, replace, regular
constraints, and length constraints.
- SLRP - for automatically verifying liveness for randomised
parameterised systems and distributed protocols, and reasoning about two-player
- for automatically verifying/synthesising symmetry
patterns and simulation preorder for parameterised systems
(see our VMCAI paper).
- for detecting redundant CSS rules in HTML5 applications
(see here for a
- ReCount - for verifying integer-manipulating concurrent
recursive programs via reversal/synchronisation bounding (see our
CAV'11 paper and CAV'12 paper).
- PC chair/organiser:
- Program committee member:
- Past (selected):
Oriented Programming (2017)
- Theory of Computation - Instructor/Lecturer (Spring 2016)
- Introduction to Computational Thinking and Programming for All -
Instructor/Lecturer (Spring 2016)
- 2 x Scientific Inquiry - Instructor/Lecturer (Fall 2015)
- Logic for
formal verification - co-lecturer (Summer 2015, National
- Introduction to Computational Thinking and Programming for All
- Instructor/Lecturer (Spring 2015, Yale-NUS)
- Quantitative Reasoning - Instructor/Lecturer (Spring 2015,
- Scientific Inquiry - Instructor/Lecturer (Fall 2014, Yale-NUS)
- Automata, Logic, and Games - Co-lecturer (2012, Oxford)
- Theory of Data and Knowledge Bases - Tutor (2011, Oxford)