Abstract:  Formal methods offer a vast collection of techniques to analyze and ensure the correctness of software and hardware systems against a given specification. In fact, modern formal methods tools scale to industrial applications. Despite this significant success, privacy requirements are not considered in the design of these tools. For example, when using automated reasoning tools, the implicit requirement is that the formula to be proved is public. This raises an issue if the formula itself reveals information that is supposed to remain private to one party. To overcome this issue, we propose the concept of privacy-preserving automated reasoning.

We first consider the problem of privacy-preserving Boolean satisfiability. In this problem, two mutually distrustful parties each provides a Boolean formula. The goal is to decide whether their conjunction is satisfiable without revealing either formula to the other party. We present an algorithm to solve this problem. Our algorithm is an oblivious variant of the classic DPLL algorithm and can be integrated with existing secure two-party computation techniques.

We next turn to the problem where one party wants to prove to another party that their program satisfies a given specification without revealing the program. We split this problem into two subproblems: (1) proving that the program can be translated into a propositional formula without revealing either the program or the formula; (2) proving that the obtained formula entails the specification. To solve the latter subproblem, we developed a zero-knowledge protocol for proving the unsatisfiability of formulas in propositional logic (ZKUNSAT). Our protocol is based on a resolution proof of unsatisfiability. We encode verification of the resolution proof using polynomial equivalence checking, which enables us to use fast zero-knowledge protocols for polynomial satisfiability.

We will also outline Ou, the first programming framework that provides fully automated and optimal parallelization for zero-knowledge proofs. Zero-knowledge proofs are a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. The backend of Ou efficiently and automatically parallelizes ZKPs by formulating program parallelization as integer linear programming problems.

We will conclude by discussing future directions towards fully automated privacy-preserving program verification.

How to explore a DP-based state transition graph with A*, CP and LS?

Abstract:  Many planning problems may be solved with Dynamic Programming (DP) by decomposing the problem into subproblems which are recursively solved. These decompositions induce state transition graphs which are closely related to decision diagrams, and where optimal solutions correspond to best paths in the graphs. A* is a well known algorithm which extends Djikstra's algorithm with heuristics for guiding the path search. It is exact but not anytime. In other words, it computes a best path but it does not output sub-optimal paths while computing it.

In this talk, we will provide an overview of anytime extensions of A*, which compute a sequence of paths of increasing quality. We will also show how to combine them with Local Search (LS) in order to find better paths faster and with bounding and constraint propagation, in order to prune the graph. This will be illustrated using the Travelling Salesman Problem with Time Windows (TSPTW) as a running example. We will finish by presenting an experimental comparison with state-of-the-art approaches for solving the TSPTW and the time-dependent TSPTW.

Graph Learning for Planning

Abstract: State of the art methods for automated planning rely on heuristic state-space search. I will present recent work on graph representation learning to guide the search of automated planners. I will introduce graph neural network and other graph learning representations that exploit the relational structure of planning domains. They allow our planner GOOSE to learn heuristic cost estimates and state rankings from solutions to just a few small problems, and solve substantially larger problems than trained on. Perhaps surprisingly, our experimental results show that classical machine learning approaches vastly outperform deep learning ones in this context. Moreover, Greedy Best-First Search guided by our best learnt heuristics rivals with the state of the art model-based planner, Lama, on the problems of the latest International Planning Competition Learning track, leading to the possibility that learnt heuristics may replace existing model-based heuristics in the near future.

When Models Meet the Real World: Lessons from Applied AI Research

Abstract: In theory, there is no difference between theory and practice; in practice, there is." While the authorship of this famous quote remains debated, it resonates deeply, particularly in the context of applied AI.  When we move from the controlled environment of fundamental research to the complexities of real-world problems, especially with search and model-based AI approaches, the gap between expectation and reality can be vast. This talk will explore some of the challenges encountered when deploying models and search algorithms in practical settings. We'll delve into the lessons learned from bridging this gap, discussing the trade-offs, unexpected pitfalls, and unique rewards of applied research.

Bio: Mauro Vallati is a UKRI Future Leaders Fellow and ACM Distinguished Speaker on Artificial Intelligence (AI) for the UK. He is a Professor of AI at the University of Huddersfield, where he leads the Autonomous Intelligent Systems research center and the AI for Urban Traffic Control research team. Mauro has extensive experience in real-world applications of AI methods and techniques, spanning from healthcare to train dispatching. In 2014, he started working on AI applied to the field of urban traffic control, a line of research that led to numerous high-impact academic publications, patents filed in the United Kingdom, China, and the United States, as well as the deployment of the resulting techniques in urban areas of the United Kingdom.

Heuristic Search vs. Constraint Programming for Single Machine Scheduling

Abstract: In the scheduling literature, single-machine scheduling problems are defined to isolate challenging problem characteristics and investigate the boundary between P and NP-completeness. Typically, problems in the latter class are solved with mixed-integer linear programming, customized branch-and-bound, or dynamic programming. In this tutorial, I will use two recently proposed single-machine scheduling problems to introduce approaches to scheduling using domain-independent dynamic programming (DIDP) and constraint programming (CP). Inspired by AI planning, DIDP is a model-and-solve approach to combinatorial optimization problems that models problems as dynamic programs in a solver-independent modeling language and, currently, solves the models using heuristic search. CP is a well-developed approach to combinatorial optimization with a mature set of concepts for scheduling problems. My primary goals are to introduce the SoCS community to DIDP as a potential area for heuristic search research and to present the higher-level constructs that make CP a state-of-the-art approach to scheduling problems.

Bio: J. Christopher Beck is a Professor in the Department of Mechanical & Industrial Engineering at the University of Toronto. For over 25 years, Chris has explored intelligent problem solving in Artificial Intelligence and Operations Research through the frameworks of constraint programming, mixed integer programming, heuristic search, and, most recently, dynamic programming. He has published over 170 papers in international conferences and journals. He has served as the President of both the Executive Committee of the International Conference on Automated Planning and Scheduling and of the Association for Constraint Programming and is an Editor-in-Chief of the Journal of Artificial Intelligence Research. Chris was elected as a AAAI Fellow in 2025.

TBA