I am interested in developing methods using logic and automata for
automatically reasoning about programs. At the moment, I have been doing lots of
research related to logics over strings. I like applications that
arise from web security/optimisation, analysis of large concurrent programs,
and databases, to name a few.
When doing research, I always try to strike a healthy balance between theory,
tool construction, and case studies.
- Current research projects:
- Some tools:
- satcss -
one of the best CSS minifiers around at the moment in terms of
minification rate. It uses maxsat solvers to iteratively find best
rule-merging opportunities that are difficult to identify otherwise.
- 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).
Current team members:
Graduated team members:
- PC chair/organiser:
- Executive Committee Member:
- Program committee member:
- 2019-present: please see this page
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)