The interplay between logic and automata has been a fruitful theme in computer science that can be traced back to the classic results of Buchi, Rabin, Elgot, and Mezei from 5-6 decades ago. The field of formal verification has been one of the many beneficiaries of the useful interplay between logic and automata; the classic automata-based algorithm for Linear Temporal Logic by Vardi-Wolper being a prime example. In this talk, I will discuss the problem of verifying programs that manipulate complex data types (e.g. strings), and how the intimate connection between logic and automata can be exploited to derive a clean, and yet expressive, framework and powerful algorithms. I will also describe applications to different domains including reasoning about cross-site scripting vulnerabilities in web applications, and parameterised verification of distributed protocols.
Dr. Anthony W. Lin is currently an Associate Professor in Programming Languages at Oxford University Department of Computer Science, and a holder of ERC Starting Grant and Google Faculty Research Award. Previously, he was an Assistant Professor in Computer Science at Yale-NUS College (Singapore), and an EPSRC Postdoctoral Research Fellow at Oxford University. He completed his PhD in Informatics at Edinburgh University (UK) in 2010, and a BSc (Hons) in Computer Science and Informatics at Melbourne University in 2004. Dr. Lin's research interests lie in logical methods for programming technologies including constraint solving, formal verification, and program analysis focussing on the applications to cybersecurity, web performance optimisation, concurrent systems, and databases.