Anthony Widjaja Lin

News

• I have two PhD positions at MPI-SWS. 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

Background

• Professor in Theoretical Computer Science (Automated Reasoning), ERC Starting Grant Fellow, and Max-Planck Fellow at Technical University of Kaiserslautern, Germany
Previously:
• (2016 - 2019) Associate Professor in Programming Languages at Oxford University Department of Computer Science and Governing Body Fellow at Kellogg College
• (2014 - 2016) assistant professor at Yale-NUS, Singapore
• Completed PhD in Informatics at University of Edinburgh in 2010 under Leonid Libkin (supervisor) and Richard Mayr (co-advisor).

Research

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:
  • Algorithmic Verification of String-Manipulating Programs
  • Verification of parameterized concurrent systems:
    • Regular model checking
• 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 reachability games.
  • ParaSymmetry - for automatically verifying/synthesising symmetry patterns and simulation preorder for parameterised systems (see our VMCAI paper).
  • TreePed - for detecting redundant CSS rules in HTML5 applications (see here for a detailed description).
  • ReCount - for verifying integer-manipulating concurrent recursive programs via reversal/synchronisation bounding (see our CAV'11 paper and CAV'12 paper).
• Publications (on Google Scholar|||| on DBLP)

Current team members:

• Shuanglong Kan (Postdoc, 2019 - present)
• Muhammad Najib (Postdoc, 2019 - present)
• Daniel Stan (Postdoc, 2019 - present)
• Pascal Bergstraßer (PhD student, 2020 - present)
• Chih-Duo Hong (PhD student, 2017 - present)
• Oliver Markgraf (PhD student, 2020 - present)

Graduated team members:

• Reino Niskanen (postdoc, 2018 - 2019)
• Xuan-Bach Le (postdoc, 2018 - 2019; PhD student, 2014 - 2017)

Events:

• PC chair/organiser:
  • APLAS 2019
  • MOSCA (Meetings on String Constraints and Applications) 2019
  • ICECCS 2018
  • INFINITY 2016
  • IMS Workshop Series on Automata, Logic and Games (2016)
• Program committee member:
  • CSL 2022
  • POPL 2022
  • ATVA 2021
  • TPSS 2021
  • CAV 2020
  • PPDP 2019
  • ATVA 2019
  • VMCAI 2019
  • CAV 2019 Verification Mentoring Workshop
  • LICS 2018
  • ICALP 2017
  • PSI 2017
  • FoSSaCS 2017
  • APLAS 2016
  • PSI 2015
  • LICS 2015
  • INFINITY 2013

Teaching

• 2019-present: please see this page