Virtual Talk with Anthony Lin
Abstract
We live in a time period, during which computerized systems have become so complex that we often understand very little of how they function. This lack of understanding can sometimes lead to serious consequences, including the loss of money, confidential information, and even human lives. Automated Reasoning is a field that grew out of the desire and need to rigorously and automatically analyze the behavior of complex computerized systems, be they a piece of software artifact, a distributed protocol, a neural network, or a multi-agent system, among others. Loosely speaking, the dynamic of a system is formally specified in a logical language with a precise semantics (typically: predicate logic over certain "base theories" that support arithmetics, string operations, etc.). One then designs algorithms (called "solvers") that prove rigorously specified properties of such systems (e.g. whether a program will "crash", a request for access in a distributed protocol will eventually be granted, or a certain evolutionary biological model will have a genetic drift). In this talk, I will describe an approach called "regular model checking", which reduces the analysis of a complex system to reasoning about a string-rewrite system. I will show how a "proof" of a property of a system can be automatically generated for interesting examples of complex systems, and checked in a "trustworthy" manner. Finally, I will describe the challenges that remain in the area, including scalability, trustworthiness, and the quest for more expressive logical languages.
Bio
Anthony Lin completed his PhD in informatics at Edinburgh University in 2010. He was an assistant professor in computer science at a liberal arts college in Singapore (Yale-NUS College) between 2013 - 2016, and an associate professor in programming languages at Oxford University between 2016 - 2019. He is now a full professor in Automated Reasoning at University of Kaiserslautern-Landau and a Max-Planck Fellow at Max-Planck Institute for Software Systems (MPI-SWS). His research interests span across all theoretical, implementation, and practical aspects of automated reasoning and computational logic. In particular, he is interested in exploring (and continuously inspired by) connections with different fields including programming languages, graph databases, artificial intelligence, machine learning, multi-agent systems, finance, and biology. His work was recognized by several awards including ERC Consolidator Grant, ERC Starting Grant, Amazon Research Award, and Google Faculty Award.
Zoom Registration
Please register with office@c3s.uni-frankfurt.de to receive the Zoom login.