High-Order Fixpoint Logic for Automated Program Verification
(Joint keynote with APLAS 2024)
Thursday, October 24th, 9:00 – 10:00
Speaker: Naoki Kobayashi, University of Tokyo
Abstract:
We present an overview of our recent project on automated program verification based on higher-order fixpoint logic HFL(Z), a higher-order logic equipped with fixpoint operators and integer arithmetic. Various problems for higher-order program verification can naturally be reduced to the validity checking problem for HFL(Z) formulas. Thus, an HFL(Z) validity checker can serve as a common backend for automated verification tools for higher-order programs. We explain why the HFL(Z) approach is preferable to other representative approaches to automated higher-order program verification, such as the one based on the model checking of higher-order recursion schemes. We also outline how an automated HFL(Z) validity checker can be constructed, and discuss the remaining challenges and future directions.
Bio: Naoki Kobayashi is a professor at the Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo. He received his PhD from the University of Tokyo in 1996. His current major research interests are in principles of programming languages, especially type systems, higher-order model checking, and automated program verification. He is a fellow of IPSJ and JSSST.
Playing Games on Automata
Tuesday, October 22nd, 9:30 – 10: 30
Speaker: Orna Kupferman, Hebrew University
Abstract:
The interaction between a system and its environment corresponds to a game in which the system and the environment generate a word over the alphabet of assignments to the input and output signals. The system player wins if the generated word satisfies a desired specification. A correct reactive system has to satisfy its specification in all environments, and thus corresponds to a winning strategy for the system player in the above game. This view is the key to the game-based approach for reactive synthesis. It reduces synthesis to the problem of generating winning strategies in two-player games whose winning conditions are on-going behaviors, which can be specified by automata on infinite words. The paper presents the game-based approach, focusing on ways to cope with the fact that the game cannot be played over nondeterministic automata.
Bio: Prof. Orna Kupferman is a faculty member at the School of Computer Science and Engineering, the Hebrew University. Her research areas cover the theoretical foundations of the formal verification and synthesis of computer systems, with a focus on automata theory and game theory and their applications. In the last 20 months, Orna’s main activity has been protesting against Israel’s government, joining hundreds of thousands of Israelis in a struggle for the end of the war and for Israel’s democracy.
The Power of Feedback — Rethinking Reactive Synthesis for Autonomy-Driven Control of Cyber-Physical Systems
Wednesday, October 23rd, 9:00 – 10:00
Speaker: Anne-Kathrin Schmuck, Max Planck Institute for Software Systems
Abstract:
Feedback allows systems to seamlessly and instantaneously adapt their behavior to their environment and is thereby the fundamental principle of life and technology — it lets animals breathe, it stabilizes the climate, it allows airplanes to fly, and the energy grid to operate. During the last century, control technology excelled at using this power of feedback to engineer extremely stable, robust, and reliable technological systems.
With the ubiquity of computing devices in modern technological systems, feedback loops become cyber-physical — the laws of physics governing technological, social or biological processes interact with (cyber) computing systems in a highly nontrivial manner, pushing towards higher and higher levels of autonomy and self-regulation. True autonomy, however, requires complex strategic and reactive decision making to interacting with classical feedback control. While stability, robustness and reliable self-adaptation remain to be of uppermost importance in these systems, the understanding of autonomy-driven strategic feedback loops and their utilization for this purpose is lacking behind.
In this talk, I will discuss how a control-inspired view on formal methods, in particular reactive synthesis, holds high promises for the design of robust and adaptable autonomy-driven strategic feedback loops in cyber-physical systems.
Bio: Anne-Kathrin Schmuck is a tenure-track faculty member at the Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany, leading the Control Software Systems Group. She is a member of the Emmy Noether Programme of the German Science Foundation (DFG) since 2020 and her independent research group was hosted at MPI-SWS until she became a faculty member in July 2023. She studied Engineering Cybernetics at OvGU Magdeburg (Germany), UBC Vancouver (Canada) and Lund Universitet (Sweden) and holds a Dr.-Ing. (Ph.D.) degree in electrical engineering from TU Berlin (Germany).