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.
Probabilistic Datatypes
Annabelle McIver
Computer Science
Macquarie University in Sydney
Abstract:
Datatypes — in which data is encapsulated together with methods that access it — play an important role in the organisation of large software projects. Correctness of datatypes has traditionally been carried out using simulation relations to simplify the verification by separating concerns: the datatype can be verified independently from the programs that use it, whilst those programs themselves can be verified using the specifications of the datatype’s methods.
In this talk I introduce the idea of probabilistic datatypes in which probabilistic choices are used to implement probabilistic specifications. I will show, by example, how the standard Markov Decision Process model fails the well known “copy rule” when both nondeterminism and probability are present, and that a more sophisticated model using ideas from the theory of Quantitative Information Flow is necessary for sound proof rules based on the well-known technique of simulations.
Short Bio
Annabelle McIver is a professor of Computer Science at Macquarie University in Sydney, and co-director of the Future Communications Research Centre. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book “Abstraction, Refinement and Proof for Probabilistic Systems”, and “The Science of Quantitative Information Flow”.