Speakers
Proving Safety of Automated Driving Vehicles
Prof. Dr. Ichiro Hasuo
Director of Research Center for Mathematical Trust in Software and Systems
National Institute of Informatics – Tokyo, Japan
Abstract:
I will introduce our recent work on using formal logic to rigorously prove the safety of automated driving vehicles. The main challenge in such formal verification attempts for real-world systems is the absence of target system models. We follow the methodology called RSS (responsibility-sensitive safety, Shalev-Shwartz et al., 2017) that tells what to model (and what not to model) in a both technically and socially sensible way. Our formalization and extension of RSS with a Floyd–Hoare-style program logic allows us to handle complex driving scenarios compositionally, and to cover real-world scenarios such as emergency pull over for the first time. I will demonstrate the use of obtained proofs with driving simulation. Overall, the work suggests the potential of formal logic as a social infrastructure for establishing trust in novel ICT. The talk is based on the following papers:
Short Bio
Ichiro Hasuo, Ph.D., is a Professor at National Institute of Informatics (NII), Tokyo, Japan. He is at the same time the Research Director of the JST ERATO “Metamathematics for Systems Design” Project, and the Director of Research Center for Mathematical Trust in Software and Systems at NII. He received PhD (cum laude) in Computer Science from Radboud University Nijmegen, the Netherlands, in 2008. His research field is software science and his interests include formal verification, mathematical and logical structures, integration of formal methods and testing, and application to cyber-physical systems and systems with statistical machine learning components.
The Unreasonable Effectiveness of Automated Reasoning in Quantum Computing
Dr. Alfons Laarman
System Verification Lab (SVL) – Leiden University
Leiden, Netherlands
Abstract:
In this talk, we will show that existing classical automated reasoning methods perform exceedingly well for computationally hard problems in quantum computing. In particular, we demonstrate a linear-length #SAT encoding of the simulation and equivalence checking of universal quantum circuits. An implementation of this method, called Quokka#, outcompetes other state-of-the-art approaches using an off-the-shelve #SAT solver that supports negative weights (GPMC).
While decision diagrams offer a viable alternative, we unveil their inherent limitations stemming from their inability to represent the prevalent stabilizer states. This limitation is particularly noteworthy considering the efficient classical simulatability of circuits generating such states. To address this constraint, we introduce Local Invertible Map Decision Diagrams (LIMDDs), which offer exponential improvements in succinctness compared to the combination of stabilizer formalism and existing decision diagrams.
Finally, we show how these findings can be translated back to the domain of quantum physics, so that the results will be useful regardless of the existence of quantum computers. For this, we use Darwiche’s seminal “knowledge compilation map” approach by providing a first knowledge compilation map for quantum information comparing various decision diagrams against tensor networks and Boltzmann machines; two formalisms extensively used in physics to tackle quantum-hard problems like simulation of many-body systems and finding the ground energy of such a system. Our results show that existing automated reasoning methods have a strong potential for quantum computing and physics.
Short Bio
Alfons Laarman is associate professor at Leiden University, where he leads the System Verification Lab (SVL) and is co-founder of the inter-departmental Applied Quantum Algorithms (aQa) initiative. Prior to moving to Leiden, he was postdoc at the TU Vienna and completed his PhD at University of Twente with distinction (cum laude).
Laarman is known for parallel DFS-based graph algorithms, divide & quantum algorithms, a knowledge compilation map for quantum information and #SAT-based quantum circuit compilation methods. In general, his research spans reliable computing, parallel computing and quantum computing, often bridging theory and practice. His research is funded by several national and European consortia as well as by personal grants from the Dutch Scientific Research Council.
Automated Synthesis: Fusing Formal Methods and AI
Dr. Priyanka Golia
Computer Science and Engineering Department
Indian Institute of Technology Delhi – New Delhi, India
Abstract:
We increasingly entrust large parts of our daily lives to computer systems, which are becoming more complex. Developing scalable and trustworthy techniques for designing, developing, and verifying these systems is crucial. In this talk, we will focus on automated synthesis, a technique that uses formal specifications to automatically generate systems (such as functions, programs, or circuits) that provably satisfy the specified requirements.
The talk will overview recent approaches that combine advances in automated reasoning, knowledge compilation, and machine learning to address a wide variety of practical automated synthesis problems. Additionally, we will introduce a state-of-the-art functional synthesis algorithm that leverages artificial intelligence to provide an initial guess for the system and then uses formal methods to repair and verify this guess, resulting in a system that is correct by construction.
Short Bio
Priyanka Golia is an Assistant Professor in the Computer Science and Engineering Department at the Indian Institute of Technology Delhi. Prior to that, she was a faculty at the CISPA Helmholtz Center for Information Security, Germany. She completed her Ph.D. through a joint degree program between Indian Institute of Technology Kanpur, India, and National University of Singapore.
Her research interests lie at the intersection of formal methods and artificial intelligence. Specifically, her work has focused on designing scalable automated synthesis and testing techniques. Her research has received a Best Paper Nomination at ICCAD-21, a Best Paper Candidate at DATE-23, and an invitation for special issues in FMSD. She was named one of the EECS Rising Stars in 2022.