- I have two PhD positions at
Topic is flexible, but has to be
aligned with my general interests (see below). Email me with your CV and
explain why you are interested.
- Submit to CAV 2020
- I have been recently awarded a Max-Planck Fellowship. Thanks to
everyone who supported me
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:
- 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 parameterized concurrent systems:
- 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:
- Program committee member:
(Bachelor) [Summer Semester]
- Logic and Verification Seminar (Bachelor/Masters) [Summer Semester]
- 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)