- (Mar'19) I have moved to TU Kaiserslautern's Department of Computer Science
as a professor. I have a number of researcher openings at PhD
and postdoc levels. Potential candidates need to show strong
interests in one of the
following areas: logic, formal language theory, algorithms and/or
programming languages. Contact me if interested.
- (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!
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)