Program
Dinner is at 7pm: https://maps.app.goo.gl/vn8gMo2EBoDUvuWU6
Giuseppe De Giacomo Oxford University
Title: From Infinite to Finite Traces and Back
Abstract. Linear Temporal Logic (LTL) has a long-standing role in computer science and AI, thanks to its ability to express sophisticated temporal properties over infinite traces. More recently, finite-trace variants of LTL, such as LTL on Finite Traces (LTLf) and Pure Past LTL (PPLTL), have gained significant traction in sequential decision making in AI, where an autonomous agent typically loops through three finite phases: acquiring a goal, reasoning strategically to achieve it, and executing the resulting strategy (or plan). A key advantage of these finite-trace logics is their reducibility to regular automata, which can be determinized and converted into two-player games on graphs. This leads to unprecedented computational scalability and effectiveness. Can these advantages be extended back to infinite traces? In this talk, we provide a positive answer. By leveraging Manna and Pnueli's safety-progress hierarchy, we introduce infinite-trace extensions of LTLf and PPLTL that retain the full expressive power of LTL, while preserving the crucial property that the game arena for strategy extraction can still be derived from deterministic finite automata.
Bio. Giuseppe De Giacomo is a Professor of Computer Science in the Department of Computer Science at the University of Oxford. He has previously been a Professor in the Department of Computer, Control, and Management Engineering at the University of Rome "La Sapienza." His research spans theoretical, methodological, and practical aspects of Artificial Intelligence and Computer Science, most prominently in Knowledge Representation, Reasoning about Actions, Generalized Planning, Autonomous Agents, and Reactive Synthesis and Verification. He is a Fellow of AAAI, ACM, and EurAI. He received an ERC Advanced Grant for the project WhiteMech: White-box Self-Programming Mechanisms. He serves on the Board of EurAI and chairs the steering committee of the new annual EurAI summer school, ESSAI.
Serdar Tasiran AWS
Title: GenAI, Automated Reasoning, and Synthesis for Cloud Computing
Abstract. I will describe three use case scenarios that users building on web services encounter, encouraging researchers to explore methods that combine automated reasoning (formal methods) for program analysis with GenAI to make humans more effective in these settings. These scenarios are (i) building applications that use web service APIs, (ii) using infrastructure as code to manage deployment of cloud resource configurations, and (iii) migrating without disruption from on-premises computing using legacy programming languages to computing on the cloud with modern programming languages. The talk will focus mainly on the application challenges and highlight the domain constraints that we believe motivate the use of automated reasoning and program synthesis in conjunction with GenAI.
Bio. Serdar has been a Principal Applied Scientist at AWS since 2016 and is currently in the agentic AI organization. At Amazon, he has led teams in AWS Security, AWS Platform, the Simple Storage Service (S3), and automated reasoning for GenAI. He received his MS and PhD from the University of California at Berkeley in 1995 and 1998 respectively. Until 2003, he was a research scientist at the DEC/Compaq/HP Systems Research Center (SRC). 2003-2016, he was a professor at Koç University, Istanbul, Turkey. Serdar has had visiting appointments at the Univ. Paris VI, Univ. Paris VII, MIT, and EPFL. He was a Distinguished Research Fellow at Sabanci University, Istanbul, and is a member of the IFIP WG 2.3 Working Group on Programming Methodology.
Program
| 8:30-9:00 |
Breakfast |
| 9:00-10:00 |
Keynote: From Infinite to Finite Traces and Back Giuseppe De Giacomo, Oxford University |
| 10:00-10:30 |
Parameterized Infinite-State Reactive Synthesis Benedikt Maderbacher and Roderick Bloem |
| 10:30-11:00 |
Coffee break |
| 11:00-11:30 |
Program Synthesis And Non-monotonic Reasoning (Extended Abstract) Kedar Namjoshi |
| 11:30-12:00 |
Composing Reinforcement Learning Policies, with Formal Guarantees Florent Delgrange, Guy Avni, Anna Lukina, Christian Schilling, Ann Nowe and Guillermo Perez |
| 12:00-14:00 |
Lunch (provided) |
| 14:00-15:00 |
Keynote: GenAI, Automated Reasoning, and Synthesis for Cloud Computing Serdar Tasiran, AWS |
| 15:00-15:30 |
Towards a Standard Benchmark Format for Synthesis of Infinite-State Reactive Systems Philippe Heim and Rayna Dimitrova |
| 15:30-16:00 |
Coffee break |
| 16:00-16:30 |
Generating Implementations of Data Type Operations Anthony Hunt and Emil Sekerinski |
| 16:30-17:00 |
Synthesis of Safety Controllers with Plant Prophecies Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak and Anne-Kathrin Schmuck |
| 17:00-17:30 |
SYNTCOMP Results |