ABSTRACT. Automotive systems, such as Scania trucks, are complex collections of software and hardware. A typical Scania truck has tens of Electronic Control Units (ECUs), with each ECU having one or more application modules—embedded software that interacts with and controls physical actuators and sensors. Scania trucks and their ECUs must adhere to rigorous requirements on functionality, safety, and security. Standards such as ISO 26262 provide general system-level requirements on safety and security, while ECU and application module requirements are company-internal individual documents in structured natural language. This is complemented by general coding standards for common module implementation languages, such as MISRA-C for C modules. For the last ten years, we have conducted research aimed at enabling automotive systems, such as Scania trucks and their ECUs, to demonstrably meet their requirements through formal reasoning. We have considered both sound decomposition of system level requirements, e.g., on braking, and lower-level formal specification and verification of application module C code. This extended abstract presents an overview of what we believe are the current key problems in achieving trustworthy automotive systems, based on our experience from case studies involving ECU software modules and their requirements in Scania trucks. Finally, we give an outlook on directions and next steps.

ABSTRACT. CoSApp, for Collaborative System Approach, is a Python library dedicated to the simulation and design of multi-disciplinary systems. It is primarily intended for engineers and system architects during the early stage of industrial product design. The API of CoSApp is focused on simplicity and explicit declaration of design problems. A very flexible mechanism of solver assembly allows users to construct complex, customized simulation workflows. This presentation focuses on a key feature of the framework, namely the simulation of multimode systems with event-driven mode transitions. This feature allows one to model systems that undergo discontinuities (contact problems, threashold effects, etc.), as well as possible dynamic reconfigurations. We will discuss the challenges of designing such systems, through real-life industrial examples.

ABSTRACT. The ∆Q Systems Development paradigm (∆QSD) is a novel industrially-derived systems development methodology for developing complex real-world distributed systems that directly employs statistical performance metrics from the outset of the system design process and throughout the entire software production life cycle. It uses a stochastic approach to specify system behaviour, using cumulative distribution functions to model both delay and failure together. Experience shows that this is a ‘sweet spot’ that gives good results with little computation requirements. Predictions are accurate when the system model correctly captures both independent and dependent parts. This paradigm has been developed by the Welsh company PNSol over a period of 20+ years, in collaboration with IOG (formerly IOHK), BT, Vodafone, Boeing, Space and Defence, as well as other major companies who focus on the development of reliable high-quality, high integrity, distributed software systems, with strong real-time requirements. This talk will be a brief ∆QSD overview with an emphasis on compositionality, lightweight formal semantics, and the ∆QSD challenges in systems engineering.

ABSTRACT. Automating semantic labelling for termination proofs is a combinatorially hard problem since the number of algebras grows prohibitively large even for small domains. We report on experiments with our tools Matchbox and MnM, comparing various model-finding strategies: exhaustive enumeration for bounded domain sizes within restricted search spaces, and semantic context-closure for fixed algebras.

ABSTRACT. It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence ending with a normal form can be simulated by the innermost reduction. In this paper, using this simulation property, we show that for a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. As a corollary, we establish that termination and innermost termination coincide for the class of right-linear overlay TRSs.

ABSTRACT. Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unification as reduction orders and reduction pairs. We also discuss the use of it as ground total reduction orders.

ABSTRACT. Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for termination analysis and complexity analysis of term rewrite systems. Finding such polynomial interpretations for a given set of term constraints involves solving a set of $\exists\forall$ inequalities over the natural numbers. Conventionally, the absolute positiveness criterion is used to reduce $\exists\forall$ inequalities to $\exists$ inequalities. This extended abstract reports on work in progress to go beyond absolute positiveness, allowing for finding non-linear polynomial interpretations that were outside the reach of existing techniques.

ABSTRACT. Graph neural networks (GNNs) are deep learning models for graph data that play a key role in machine learning on graphs. A GNN describes a distributed algorithm carrying out local computations at the vertices of the input graph. Typically, the parameters governing this algorithm are acquired through a data-driven learning process. After reviewing GNNs and their basic theory, in this talk, I will focus on the expressiveness of recurrent GNNs. We show that recurrent GNNs can emulate all graph algorithms that respect the natural message-passing invariance induced by the colour refinement (or Weisfeiler-Leman) algorithm. Furthermore, we show that by incorporating random initialisation, recurrent GNNs can emulate all graph algorithms. This emulation introduces only a polynomial overhead in both time and space. In particular, any polynomial-time graph algorithm can be simulated by a recurrent GNN with random initialisation running in polynomial time. (This is joint work with Eran Rosenbluth.)

ABSTRACT. This tutorial explores the landscape of sequent-based proof formalisms for modal logics, using Gödel-Löb provability logic (GL) as a running example. We survey four major paradigms--labeled sequents, nested (or tree) sequents, linear nested sequents, and Gentzen sequents--and discuss the various trade-offs of choosing one formalism over another, including sequent size, proof size, and suitability for counter-model extraction. The central theme of the tutorial is understanding how these formalisms relate by means of proof transformations, explaining how one can systematically "transition" between them: from graphs, to trees, to lines, and to points (i.e., standard Gentzen sequents). Along the way, we highlight what is lost or gained in each transition, such as invertibility of rules or proof compactness. We also touch on how the choice of formalism affects proof-search algorithms.

ABSTRACT. TBA

ABSTRACT. In 'The Art of Computer Programming', Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen’s graph: the minimum number of colors needed to color the squares of an $n \times n$ chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis much further by comparing thousands of encodings for the same problem, which allows us to identify additional factors that are important for solver performance. We obtain 1584 encodings for this problem by varying (a) the constraints that encode which color is assigned to each cell, (b) the constraints that forbid the same color appearing in a row, column, or diagonal line, and (c) the symmetry-breaking constraints. We find that the three most impactful encoding factors are (i) the choice of symmetry-breaking constraints, (ii) enabling so-called clique hints, and (iii) enforcing that each cell is assigned exactly one color through blocked clauses. Furthermore, while Knuth proposed clique hints as an advantage of the order encoding, we show in fact that they can be effectively employed for the one-hot encoding as well.

ABSTRACT. The last years have brought substantial advancements to parallel and distributed SAT solving, including distributed clause-sharing solving that scales to thousands of cores, distributed incremental SAT solving, scalable proof production, and flexible multi-tasking of many (incremental) SAT tasks. This talk discusses to which degree SMT solving can profit from this technology. I touch on prior works on parallel and distributed SMT solving, outline our recent work on massively parallel bit-precise verification (combining the sequential bit-blasting SMT solver Bitwuzla with the distributed SAT platform Mallob), and discuss potential future directions for parallelizing general SMT solving.

ABSTRACT. Parallel approaches to SMT solving are an appealing avenue for improving SMT performance, especially with the increased availability of high-performance computing and cloud computing resources. One such approach is partitioning, a divide-and-conquer technique which endeavors to break the problem down into easier subproblems which can be solved in parallel. Unfortunately, this vision has been challenging to realize in practice. Specific challenges include the difficulty of finding good partitioning formulas, the inability to share information among subproblems, and the instability problem in SMT, all of which can contribute to some subproblems requiring even more time than the original problem. In this paper, we present fixed first decisions, a new technique which addresses the latter two challenges: it enables sharing of information among different partitions, and it enables a collaborative partitioning mode which mitigates the impact of difficult subproblems. We implement our approach using SMT-D and cvc5 and evaluate the implementation on SMT-LIB benchmarks, showing that it demonstrates a significant speedup over prior partitioning approaches.

ABSTRACT. This work extends Brzozowski derivatives of regular expressions to alphabets equipped with similarity-based symbol matching. It proves that fuzzy derivatives preserve regularity, induce finitely many states over finite alphabets, correspond semantically to language derivatives, and can be simulated by ordinary derivative automata over a quotient alphabet. The theorems are formalized in Rocq.

ABSTRACT. Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of $\epsilon$-DP. Our method refutes $\epsilon$-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for $\epsilon$-DP refutation. To the best of our knowledge, our method is the first method for $\epsilon$-DP refutation to offer the following four desirable features: (1)~it is fully automated, (2)~it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3)~it provides soundness guarantees, and (4)~it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute $\epsilon$-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.

ABSTRACT. We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all programs that consist of a single loop, with a linear loop guard and a loop body composed of two linear commuting and diagonalizable updates. In each iteration of the loop, the update to be carried out is picked at random, according to a fixed probability. We show the decidability of UPAST for this class of programs, where the program's variables and inputs may range over various sub-semirings of the real numbers. In this way, we extend a line of research initiated by Tiwari in 2004 into the realm of randomized programs.

ABSTRACT. While termination of ordinary programs has been studied for decades, the analysis of probabilistic programs has become increasingly important. In the probabilistic setting, requiring all executions to be finite is often too restrictive. Instead, one studies almost-sure termination (AST) where every computation has to terminate with probability 1. Thus, infinite executions may still exist, but the probability of such an infinite execution is 0. In this talk, we consider term rewriting, a well-studied functional programming model based on pattern matching. More precisely, we consider probabilistic term rewrite systems (PTRSs), where the choice of the applied rule remains nondeterministic, but the result of applying a rule is determined probabilistically, similar to the semantics of a Markov decision process. In addition to developing automatic techniques for analyzing AST, one should investigate their limitations. There are multiple ways to assess the “difficulty” of a decision problem in computer science. For example, one may ask under which assumptions the problem becomes decidable. Such assumptions can be syntactic restrictions, e.g., considering only a specific class of PTRSs. Another way to assess the difficulty of an undecidable problem is to relate it to other undecidable problems. So one asks which undecidable problems would need to be decidable in order to decide AST for arbitrary PTRSs. This induces a hierarchy of undecidable problems, where problem A is “harder” than problem B if A remains undecidable even when equipped with an oracle for B. For example, universal termination remains undecidable even if the halting problem (termination on a given input) were decidable, and is therefore “harder”. Since similar decision problems for imperative probabilistic programs have already been placed in such hierarchies, we follow the first approach and restrict the structure of PTRSs so that AST becomes decidable. In the non-probabilistic setting, there is a well-known subclass of TRSs where termination is decidable: right-ground TRSs. A TRS is right-ground if all of its right-hand sides are ground terms, i.e., contain no variables. For example, the rule leq(x, x) → true is right-ground, but leq(s(x), s(y)) → leq(x, y) is not. If right-hand sides contain no variables, then one cannot pass arbitrary information through recursive calls. We show why the decision procedure for termination of right-ground TRSs does not generalize to the probabilistic setting. Consequently, we further restrict the subclass so that it can be related to a stochastic system with a known decision procedure for AST: stochastic context-free grammars. Stochastic context-free grammars (SCFGs) generalize context-free grammars by replacing nondeterministic choice with probabilistic choice. In this talk, we recapitulate SCFGs from and how to decide AST for them. Then, we show how to transform every PTRS P from a certain subclass into an SCFG G such that P is AST if andonly if G is AST. For this transformation, we require the PTRS to be: (RG) right-ground (as in the non-probabilistic decision procedure), (NO) non-overlapping (to remove additional nondeterminism in the rule selection), and (TR) tail-recursive (there are no nested defined symbols, as in context-free grammars). This yields the first decision procedure for AST of PTRSs that are RG, NO, and TR.

ABSTRACT. Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve due to their sophisticated algorithms and highly optimized data structures. Understanding these complex mechanics and evaluating the effectiveness of problem encodings is notoriously challenging for students and emerging researchers. To ease this learning process, we introduce the Interactive SAT Tracer (SAT-IT), an open-access web environment designed to make the foundations of SAT solving highly visible and interactive. SAT-IT offers a staged pedagogical progression: from naive backtracking to DPLL and full CDCL with the two-watched literals scheme. Users can clearly inspect fundamental data structures, search space trails, and solving statistics. The tool interactive search space exploration is boosted with literal-level breakpoints for targeted inspection, alongside versatile automatic solving modes that offer both continuous real-time execution and state-based subroutine automation. Combined with a powerful ``what-if'' capability for stepping backward to explore alternative decisions, an instance manager, and an extensible architecture ready to support additional algorithms, SAT-IT serves as a practical, granular lens for experimenting with SAT solving algorithms and analysing encodings efficiency.

ABSTRACT. Logic for Fun is an online tool aimed at teaching the skill of using first order logical notation to specify problems in such a way that a model of the encoding is a solution to the problem. Older versions of the tool have been in use for many years, but the latest (2026) offers increased functionality to improve both the user experience and the process of assessing students' work. In this demonstration, we give an overview of the site and illustrate the process of using it to solve problems.

ABSTRACT. We present LogicProof, an interactive web-based theorem prover designed for educational use. The system supports natural deduction and sequent calculus for propositional and first-order logic in both classical and constructive variants. It emphasizes a modern user experience through real-time feedback and interactive visualization of proof trees. We evaluated LogicProof in a study involving 35 students. The results suggest that the system improves understanding of formal proof construction and supports student engagement with logical concepts. Compared to traditional pen-and-paper approaches, students reported faster iteration, easier error correction, and greater confidence in the correctness of their solutions. These findings indicate that LogicProof can serve as a practical supplement to existing teaching methods, particularly in supporting the learning process and reducing barriers associated with formal proof construction.

ABSTRACT. Most state-of-the-art model checking algorithms for infinite state systems are based on Craig Interpolation. These algorithms are very powerful, but also highly sensitive to minor changes of the input or the underlying interpolating SMT solver. In recent years, we developed several non-interpolating model checking algorithms, with the goal of making infinite state model checking more robust and predictable. Their core ingredients are loop acceleration, which is useful for finding deep counterexamples, and recurrence analysis, which is the most important building block of our techniques for proving safety / satisfiability. In this talk, I will give an overview of these non-interpolating model checking algorithms, and highlight their strengths and weaknesses.

ABSTRACT. In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIB format, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions. This paper has already been published as a technical report on arXiv (https://arxiv.org/pdf/2511.21509) so we aim for a presentation-only paper.

ABSTRACT. 75 years after the birth of computing as a discipline with the founding of the Association for Computing Machinery, we seem to be witnessing a Kuhnian paradigm shift in computer science. The old paradigm of computer science as a science of formal models seems to be out, and a new paradigm of computer science as a data-driven discipline is in. I argue that the paradigm-shift paradigm has been overplayed. In reality, scientific paradigms glide rather than shift. Good old formal computer science is as important as ever. But there has been a paradigm shift in how computing research is being carried out. The center of gravity in computing research used to be in academia, where its goal was to contribute to the common good. Today this center of gravity moved to industry, where its goal is to maximize corporate profits.

ABSTRACT. Coding agents such as Claude Code, Codex and others are creating a new paradigm that will change programming in ways impossible to foresee. Recent experiences with coding agents indicate that they can easily generate logic programs in Prolog and ErgoAI, as well as lower-level Prolog system code. We conjecture about the implications of these experiences and suggest research pathways to explore the importance of logic programs can in an age of coding agents.

ABSTRACT. Automated theorem provers (ATPs) can disprove conjectures by saturating a set of clauses, but the resulting saturated sets are opaque certificates. In the unit equational fragment, a saturated set can in fact be read as a convergent rewrite system defining an explicit, possibly infinite, model — but this is not widely known, even amongst frequent users of ATPs. Moreover, ATPs do not emit these explicit certificates for infinite (counter-)models. We present such a certificate construction in full, implement it in Vampire and E, and apply it to the recent Equational Theories Project [5], where hundreds of implications do not admit finite countermodels. The resulting rewrite systems can be checked for confluence and termination by existing certified tools, yielding trustworthy countermodels.

ABSTRACT. Term and clause indexing are central technologies for efficient first-order theorem provers and similar reasoning systems. While there are a selection of basic technologies, most of them require an efficient mapping from function symbols (usually encoded as small integers) or other integer values to branches of a tree structure. With today's wide variety of application problems, both the range of possible values and the cardinality of each individual map vary wildly. We present a data structure that is designed to be efficient in time and space at all scales and key distributions. Experiments show very good scalability and a modest improvement over the old, already quite refined data structure in E.

ABSTRACT. We survey the area of proof complexity of model counting. Several proof systems for model counting have been suggested since 2019, most of which are inspired by solving approaches. The survey explains the different systems, static and line based, and discusses the simulation order of the systems and known separations. Many proof systems are based on Decision-DNNFs, which are suitably annotated. We also discuss how these proof systems relate to state-of-the-art #SAT solving approaches. In the end, we discuss future directions for the field.

ABSTRACT. Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that: (i)~with moderate adaptations, the conceptually quite different proof models of the dynamic system MICE and the static system of annotated Decision-DNNFs are equivalent and (ii)~they tightly characterise state-of-the-art #SAT solving. Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting. We also propose new strengthenings of these proof systems that might lead to stronger model counters.

ABSTRACT. First-Order Logic (FOL) is a powerful formalism that naturally captures a wide range of decision and optimization problems. Over the past two decades, automated reasoning tools such as SAT and Satisfiability Modulo Theories (SMT) solvers have advanced dramatically, making logic-based approaches practical for many applications in computer science and program analysis. Today, many program analysis techniques formulate their verification tasks as logical constraints and rely on SAT or SMT solvers to reason about them automatically. In this talk, we focus on a fragment of FOL known as Constrained Horn Clauses (CHCs) and on SPACER, a state-of-the-art CHC solver. CHCs arise naturally in many verification and synthesis applications, including the discovery and verification of inductive invariants, safety verification of finite- and infinite-state systems, model checking of pushdown systems and their extensions, modular verification of distributed and parameterized systems, type inference, and many others. A key advantage of the CHC-based approach is the separation of proof methodology from proof search. Verification tasks are first encoded as CHCs through the generation of Verification Conditions (VCs), while the responsibility for solving these conditions is delegated to a CHC solver. This separation enables a single framework to support multiple proof methodologies, programming languages, and verification tasks, while maintaining high performance and scalability.

ABSTRACT. Second-order quantifier elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the saturation-based SCAN algorithm. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding a witness for the second-order quantifiers that results in a logically equivalent first-order formula. In addition, we provide a prototype implementation of the proposed method.

ABSTRACT. Verified explanations offer a principled way to explain neural network decisions by grounding explainability in formally verified robustness, thereby addressing the inherently black-box nature of these models. We propose two complementary notions of verified explanations. The first is defined over the input space of neural networks, where we introduce hierarchical explanations, termed verifier-optimal robust explanations. These explanations explicitly account for the incompleteness of neural network verifiers, ensuring optimality with respect to the guarantees that can be formally established. The second notion is defined over the network’s internal (latent) representations, capturing explanations in terms of the model’s inner computations. We present novel efficient algorithms to compute both forms of explanations, and showcase their scalability and meaningfulness in practice.

ABSTRACT. Machine learning (ML) is increasingly adopted in space missions to enable on-board autonomy under strict constraints on power, compute, and communication. However, the deployment of ML in mission-critical satellite subsystems remains limited by the lack of rigorous verification and validation (V&V) approaches that can provide trust in model behavior under specified conditions. This work presents the study of the formal verification methods for satellite telemetry anomaly detection on the OPS-SAT mission benchmark. Specifically, we formally verify critical properties, scenarios, and robustness of the trained fully-connected neural network model using the pyNeVer and αβCrown libraries. We also discuss key benefits, challenges and limitations pertaining to the potential on-board deployment of formal verification methods in this use case. This integrated approach supports both pre-flight qualification and in-flight monitoring of ML components, aligning with emerging standards for ML assurance in aerospace systems.

ABSTRACT. Creating meaningful interpretations for black-box machine learning models involves balancing two often conflicting objectives: ac- curacy and explainability. Exploring the trade-off between these objec- tives is essential for developing trustworthy interpretations. While many techniques for multi-objective interpretation synthesis have been devel- oped, they typically lack formal guarantees on the Pareto-optimality of the results. Methods that do provide such guarantees, on the other hand, often face severe scalability limitations when exploring the Pareto- optimal space. To address this, we develop a framework based on local optimality guarantees that enables more scalable synthesis of interpre- tations. Specifically, we consider the problem of synthesizing a set of Pareto-optimal interpretations with local optimality guarantees, within the immediate neighborhood of each solution. Our approach begins with a multi-objective learning or search technique, such as Multi-Objective Monte Carlo Tree Search, to generate a best-effort set of Pareto-optimal candidates with respect to accuracy and explainability. We then verify local optimality for each candidate as a Boolean satisfiability problem, which we solve using a SAT solver. We demonstrate the efficacy of our approach on a set of benchmarks, comparing it against previous methods for exploring the Pareto-optimal front of interpretations. In particular, we show that our approach yields interpretations that closely match those synthesized by methods offering global guarantees. This work was accepted at ATVA 2025. We believe that our work and approach potentially has applications in autonomous space vehicles that use complex ML models.

ABSTRACT. We perform uncertainty propagation on an event manifold for Guidance & Control Networks (G&CNETs), aiming to enhance the certification tools for neural networks in this field. This work utilizes three previously solved optimal control problems with varying levels of dynamics nonlinearity and event manifold complexity. The G&CNETs are trained to represent the optimal control policies of a time-optimal interplanetary transfer, a mass-optimal landing on an asteroid and energy-optimal drone racing, respectively. For each of these problems, we describe analytically the terminal conditions on an event manifold with respect to initial state uncertainties. Crucially, this expansion does not depend on time but solely on the initial conditions of the system, thereby making it possible to study the robustness of the G&CNET at any specific stage of a mission defined by the event manifold. Once this analytical expression is found, we provide confidence bounds by applying the Cauchy-Hadamard theorem and perform uncertainty propagation using moment generating functions. While Monte Carlo-based (MC) methods can yield the results we present, this work is driven by the recognition that MC simulations alone may be insufficient for future certification of neural networks in guidance and control applications.

ABSTRACT. When does the order of elements "not matter" in a random sequence? The notion of exchangeability formalizes this idea as a symmetry property of a distribution. While seemingly abstract, exchangeability has been the subject of deep theoretical study and is a fundamental assumption in a variety of practical applications, enabling statistical hypothesis tests and conformal prediction. However, formal verification of exchangeability appears challenging, and has received little study. In this talk, I'll present some of our recent work on type systems for finite exchangeability. Following a common theme in programming languages, rather than tackling exchangeability directly, we focus on transformations that preserve this property. Inspired by research on bidirectional programming, we propose a new notion of equivariant lens and show that these morphisms preserve a generalization of exchangeability. By leveraging the rich categorical structure of these lenses, we develop two new type systems for building exchangeability preserving transformations and exchangeable distributions. Joint work with Vaibhav Mehta (Cornell).

ABSTRACT. TBD

ABSTRACT. TBD

ABSTRACT. Modern neural networks are powerful but opaque: they encode meaning in high-dimensional latent spaces that are hard to inspect. Interpretability research asks what these internal representations contain, and whether we can read, probe, and even steer them. In this talk, I'll give an accessible introduction to latent-space interpretability for a broad audience and connect it to my own work on the structure of learned representations. I'll show how human-meaningful concepts emerge across the layers of a network, and how concept regions tend to be approximately convex - structural regularities that offer a window into what these models have actually learned.

ABSTRACT. Accelerated by rapid advances in machine learning and AI, there has been tremendous success in the design of learning-enabled autonomous systems in areas such as autonomous driving and robotics. These exciting developments are accompanied by new fundamental challenges that arise regarding the safety and reliability of these increasingly complex systems due to imperfect learning, system unknowns, and uncertain environments. Statistical tools for uncertainty quantification have gained popularity due to their ability to deal with these challenges. However, their guarantees rely on i.i.d. data, an assumption that is violated when control actions change the underlying data distribution. In this talk, I will provide new insight to design safe controllers under distribution shifts using robust conformal prediction (CP). I will begin by advocating for the use of CP due to its simplicity, generality, and efficiency as opposed to existing optimization-based verification techniques. I will then provide an introduction to CP and summarize existing work that uses CP to design probabilistically safe controllers in dynamic environments. Subsequently, we will look into interactive settings where the system’s behavior may change the environment's behavior, and vice versa. This circular dependency creates an interaction-driven distribution shift that invalidates existing CP guarantees. To deal with this problem, we propose an iterative framework that episodically updates the controller while robustly maintaining safety guarantees by quantifying the potential impact of a controller update on the environment's behavior. We realize this via adversarially robust CP where we perform a regular CP step in each episode using observed data under the current controller, but then transfer safety guarantees across controller updates by analytically adjusting the CP result to account for distribution shifts. Lastly, I will show how these ideas extend to handling policy-induced distribution shifts that arise when using barrier/Lyapunov functions to control uncertain systems. Bio: Lars Lindemann is currently an Assistant Professor for Algorithmic Systems Theory in the Automatic Control Laboratory at ETH Zürich. From 2023 to 2025 he was an Assistant Professor in the Thomas Lord Department of Computer Science at the University of Southern California. From 2020 to 2022 he was a Postdoctoral Fellow in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. degree in Electrical Engineering from KTH Royal Institute of Technology in 2020. His research interests include systems and control theory, formal methods, machine learning, and autonomous systems. Professor Lindemann received the Outstanding Student Paper Award at the 58th IEEE Conference on Decision and Control and the Student Best Paper Award (as an advisor) at the 60th IEEE Conference on Decision and Control. He was finalist for the Best Paper Award (as an advisor) at the 2024 International Conference on Cyber-Physical Systems, the Best Paper Award at the 2022 Conference on Hybrid Systems: Computation and Control, and the Best Student Paper Award at the 2018 American Control Conference.

ABSTRACT. In an attempt to study how the Rocq prover can help teaching mathematics, we propose to exploit the ring and field tactics extensively to let students justify elementary steps in calculational proofs. These tactics manipulate formulas where they recognize a restricted set of operations and handle every value involving other functions as variables. As a result, they only work at the surface of formulas and their behavior can be puzzling, especially for beginners. We designed an extension where arguments of non-ring or non-field functions are simplified progressively. We will show how this extension makes declarative proof scripts closer to usual mathematical text. This extension is based on companion tactics, ring_simplify and field_simplify. It appears that field_simplify only performs half the simplification we expect. To improve on this, we propose implementing an extension where an external program is called to compute greatest common divisors of polynomials as an oracle and the result is checked in a traditional manner. This talk should interest any user of the Rocq prover interested in developing their own tactics combining some amount of reflexive computation, some amount of external untrusted computation, and some amount of meta-programming, in this case using Ltac and Rocq-Elpi. This is joint work with Thomas Portet, with contributions by Davide Fissore, Laurent Théry, and Enrico Tassi.

ABSTRACT. Intuitionistic modal logics with a possibility (diamond) connective have proliferated in the literature, motivated by different ideas in translational proof theory, structural proof theory, semantics, and applications. We can be comfortable with this zoo of options so long as we have tools to compare them. In work with Jim de Groot and Ian Shillito I have investigated birelational frames for Constructive K (CK) as a unified setting for the semantics of the various stronger logics that have been proposed. We have also developed a categorical duality result linking the algebraic and birelational semantics of CK, with the goal of developing results about the definability of classes of frames in this unified setting.

ABSTRACT. Graph protection problems have emerged as an important area in combinatorics and theoretical computer science, especially in the study of dynamic and online models [1]. The eternal graph framework captures situations where a solution must be maintained indefinitely under continuous adversarial actions. The classical vertex cover problem is well-studied; however, its eternal variants introduce new challenges due to the need for adaptability. In the Eternal Relaxed Vertex Cover (ERVC) problem, the defender is allowed to locally modify the solution by exchanging vertices in response to edge attacks. A set F is an eternal relaxed vertex cover (ERVC) if for every sequence of edges (e_i) there exists a sequence of vertex sets (F_i) such that: F_1 = F, for each i >= 1, F_{i+1} = (F_i \ {v_i}) U {u_i} where u_i is incident to e_i, and v_i is in F_i intersect N[u_i]. The minimum size of such a set is called the eternal relaxed vertex covering number, denoted by \tau_r^\infty(G). While eternal domination and related protection problems have been extensively studied [2], the ERVC problem remains largely unexplored on structured graph classes. In this work, we study ERVC on threshold graphs [3], exploiting their recursive structure and perfect elimination ordering properties. A graph is a threshold graph if it can be constructed from a single vertex by repeatedly adding either: an isolated vertex, or a dominating vertex. We present an efficient algorithm to compute the eternal relaxed vertex covering number for threshold graphs. Additionally, we establish bounds on the eternal relaxed vertex covering number \tau_r^\infty(G) in terms of classical graph parameters.

ABSTRACT. Colour Refinement is a combinatorial algorithm that computes a vertex colouring for an input graph to reveal its structural asymmetries. It has a precise correspondence with the 2- variable fragment of the counting logic C. This connection has yielded a deep understanding of the graphs and relational structures that can be defined in the logic. In this work, we shift the focus to definability of vertices. Those are vertices which can be “expressed” uniquely via a formula in the logic. They correspond to the vertices that receive a unique colour with respect to the algorithm. We show strong and tight lower bounds on vertex definability.

ABSTRACT. In this talk, I will discuss recent research in the area of graph isomorphism testing and beyond. After giving an introduction to the graph isomorphism problem, I will present the novel "Isomorphic Priors" computational model (Dorfman, Döring, Herold, Nanongkai, Neuen, Spoerhase, Wu). Solving a graph problem in this model involves two phases: (i) The preprocessing phase quickly analyzes a sequence of "prior graphs" along with (previously computed) exact optimal solutions. (ii) Subsequently, given a new graph H, a fast query phase must either (a) output the exact optimal solution, or (b) correctly report that H is not isomorphic to any of the prior graphs. I will discuss both positive and negative results for this computational model, and present open research directions. After that, I will address relaxations of graph isomorphism to capture similarity between graphs. I will present a recent additive approximation algorithm for graph edit distance on graphs of bounded VC dimension (Dahan, Grohe, Neuen, Novotny), and discuss several open problems in the realm of parameterized complexity.

ABSTRACT. LLM coding agents are already highly capable Lean copilots, but using them effectively on a large formalization requires more than a strong model. They may reprove existing Mathlib lemmas, miss feedback from Lean’s elaborator, introduce fragile local workarounds, or continue pursuing proof paths that have stopped making progress. In this talk I will describe `lean4-skills`, a toolkit for Lean coding agents that combines prompts, references, workflows, and tool-use guidance intended to make such agents easier to steer. The toolkit works at three levels. First, it includes Lean-specific prompting and reference material that records conventions, useful patterns to follow, and recurring pitfalls to avoid. Examples include searching before proving, carefully managing competing typeclass instances, and preferring established Mathlib idioms over ad hoc local alternatives. Second, it adds control-flow structure through slash commands, subagents, hooks, and scripts. These organize common tasks such as drafting formal statements, proving, reviewing, refactoring, golfing, and checkpointing into more explicit workflows, with bounded proof attempts and natural opportunities for human review. Third, it helps agents make systematic use of `lean-lsp-mcp`, which exposes both Mathlib search methods and Lean language-server information, allowing agents to inspect goal states, read diagnostics, use hover text, and test tactics analogously to the feedback loop available to humans in the Lean InfoView. I will discuss how I initially developed `lean4-skills` in tandem with a large AI-assisted formalization of de Finetti's theorem. The recurring difficulties that I encountered there, especially those involving conditional expectation, σ-algebra bookkeeping, avoiding elaboration timeouts, and Mathlib discovery, provided many of the example patterns and antipatterns that were later distilled into reusable guidance. The toolkit also includes a `learn` workflow for interactive teaching and Mathlib exploration. This helps keep the user involved when agents fill in more of the proof-writing, by making it easier to ask what the agent is doing, why a lemma applies, and how the surrounding Lean infrastructure is organized. It can also support informal mathematical learning, using Mathlib and the local development as checked sources of definitions and theorems, and using Lean to test formal versions of claims before explaining them informally. More broadly, improving AI assistance for Lean is not only a matter of using stronger models. It also requires shared practical knowledge about how Lean formalization proceeds: what to look up, how to interpret common errors, when to inspect the goal state, when to stop and replan, and which proof patterns tend to survive review. Through open projects like `lean4-skills`, the Lean community can benefit from treating this kind of agent-facing guidance as shared infrastructure rather than project-specific prompting notes. https://github.com/cameronfreer/lean4-skills Format: Long talk, 30 minutes

ABSTRACT. Program verification emerged in the late 1960s as a way to determine whether a program satisfies a given specification by translating the problem into a logical question. A decade later, model checking introduced the possibility of automating this verification process. Since the general verification problem is undecidable, early model-checking techniques focused on finite-state systems and propositional temporal properties, where automatic analysis is feasible.

ABSTRACT. Simulation and bisimulation play a central role in coalgebra and in program semantics. Bisimulation is a certain canonical notion of program (or system) equivalence, which can be formulated in different equivalent ways in base cases, while these ways need not remain equivalent under further generalizations. This is acknowledged and investigated in the literature. Contrastingly, simulation is a non-canonical notion of program in-equivalence (or approximation), subject to the same issue, but much less explored. This is a work in progress on exploring it.

ABSTRACT. The starting point of this paper is a recent formal verification by Nipkow and Rau of an abstract inductive but not directly executable (i.e.\ recursive) version of Earley's recognizer. The aim of that work was a particularly simple, abstract formalization and stepwise refinement towards executability. We continue this work and refine it to an executable implementation together with a proof of the running time: cubic if the $n$-th element of a list can be accessed in constant time, and quartic if access takes linear time. We present the running time analysis with the help of a simple Big $O$ formalization.

ABSTRACT. We develop a lattice-theoretic framework for query evaluation over incomplete databases under a group action on the space of possible worlds. Incomplete information is modeled as a space of possible worlds organized by the lattice of partitions. Queries and group actions induce two canonical operators on this lattice: a query refinement operator and a symmetry closure operator arising from stabilisers and their cores as normal subgroups. We study their interaction and characterize precise fixed-point conditions under which these operators are compatible in the sense of commuting on the partition lattice. This yields necessary and sufficient conditions for the existence of a decomposition of the valuation space into independent components, reducing query evaluation to componentwise computation. When these conditions fail, query and symmetry are intrinsically coupled and no such decomposition is possible.

ABSTRACT. The study of non-classical logics has long been intertwined with the investigation of algebraic structures that generalize Boolean algebras. Well-known examples include De Morgan algebras, Heyting algebras, Ockham algebras, and p-algebras, each of which gives rise to a distinct logical calculus. A recurring limitation in many of these frameworks is their reliance on a single negation operation or on negations that interact in a highly constrained manner. In this paper, we introduce and systematically study quad algebras, a new class of algebraic structures that accommodates multiple negation operations simultaneously. Quad algebras subsume both Boolean algebras and De Morgan algebras as special cases, thereby providing a strictly richer algebraic setting for investigating the interplay between different negation operators. We begin by establishing the fundamental algebraic theory of quad algebras, examining their lattice-theoretic properties and characterizing important subclasses. A central algebraic result shows that every quad algebra admits a natural ring structure induced by the Boolean negation present in the signature. Specifically, we prove that quad algebras are term-equivalent to a class of commutative rings in which every element satisfies the identity x⁴ = x. This generalizes the classical correspondence between Boolean algebras and Boolean rings (rings satisfying x² = x) established by Stone and places quad algebras within a broader ring-theoretic tradition. The identity x⁴ = x reflects the presence of a richer negation structure and yields a family of rings that properly extends the class of Boolean rings. On the logical side, we introduce a propositional calculus L_QA whose algebraic semantics is given by quad algebras, and we develop a corresponding four-valued semantics for it. The four truth values arise naturally from the structure of quad algebras and admit a transparent semantic interpretation in terms of the interaction between the two negation operators. We establish the soundness and completeness of L_QA with respect to this 4-valued semantics, thereby giving a precise logical meaning to the algebraic identity x⁴ = x. We further situate our work within the landscape of many-valued logic by comparing L_QA with Dunn’s four-valued semantics for the logic of first-degree entailment (FDE). While both systems employ four truth values and build on De Morgan-type structures, they differ in important respects: Dunn’s semantics is motivated by information-theoretic considerations and treats the four values as combinations of truth and falsity attributions, whereas the 4-valued semantics for L_QA arises from the interaction of two independent negation operators within the quad algebra framework. We identify the precise structural relationship between the two semantic frameworks and show how L_QA extends and departs from FDE in a logically meaningful way. Taken together, these results establish quad algebras as a coherent and novel contribution to the algebraic study of non-classical logics, providing a new setting in which multiple negations can be explored through both algebraic and semantic methods. Full proofs of all results presented here can be found in our published paper.

ABSTRACT. Reactive synthesis is a challenging problem for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this extended abstract, we report on current advances in tackling both sides of the problem with Large Reasoning Models (LRMs). On the algorithmic side, we present a neuro-symbolic approach that couples LRMs with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmark instances than last year's SYNTCOMP winner and extends to constructing parameterized systems. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language and introduce a dataset of natural-language specifications for evaluation. We demonstrate performance comparable to that of starting from formal specifications, establishing natural synthesis as a viable end-to-end workflow.

ABSTRACT. Strategy synthesis typically follows an all-or-nothing paradigm, returning unrealisable whenever a specification cannot be guaranteed in an uncertain environment. In this paper, we introduce optimal LTLf synthesis, where the goal is to realise as many objectives as possible from a given specification consisting of multiple objectives, especially for the case that they are not all jointly realisable. We first consider max-guarantee synthesis, which commits to a maximal set of objectives that we can a priori guarantee to realise. We then introduce max-observation synthesis, which maximises a posteriori realised objectives that may be incomparable on different executions. Finally, we present incremental max-observation synthesis, which further improves strategies by exploiting opportunities for stronger guarantees when they arise during an execution. Experimental results show that different variations of optimal synthesis scale broadly equally well, solving a large fraction of the benchmark instances within the given timeout, demonstrating the practical feasibility of the approach.

ABSTRACT. This paper describes the (new) TPTP format for representing interpretations. The sources and properties of interpretations, which influenced the design of the format, are discussed. The format for Tarskian, Herbrand, and Kripke interpretations is described. Tools for verification and visualization of the interpretations are described.

ABSTRACT. This paper describes the (new) TPTP format for writing clausal connection tableaux. The format builds on the existing infrastructure of the TPTP World, in particular the TPTP format for recording derivations. An ATP system that outputs tableaux in this format is described. Existing TPTP World tools for verifying and viewing derivations have been extended to verify and view tableaux in this format.

ABSTRACT. Automated theorem provers (ATPs) are powerful tools for formal reasoning, yet integrating them into larger software systems remains cumbersome: existing interfaces are typically script-based, tightly coupled, or limited in working across multiple backends in a uniform way. We present AtpClient, an Elixir library that provides a unified, extensible interface to ATP services across four backends, SystemOnTPTP, StarExec, Isabelle, and locally installed provers, using TPTP standards. The library acts as a truth-grounding service for host applications: it exposes a consistent API that abstracts over differences in communication protocols, result formats, and termination semantics, and normalizes the verdict of each backend into a single result type. Built on the BEAM virtual machine, it benefits from robust process isolation, fault-tolerant result polling, and uniform cancellation, making it well-suited to multi-prover experimentation and portfolio solving. We describe the architecture, discuss key design decisions, and reflect on challenges encountered when bridging the gap between ATP services and a functional runtime. We further show how the library is consumed by two downstream tools built on it without backend-specific tinkering: a Livebook Smart Cell that turns it into an interactive TPTP editor, and a Model Context Protocol server that exposes the backends to LLM-based agents. AtpClient is open source and available on Hex, the Elixir package registry.

ABSTRACT. We study the expressive power of graph transformers (GTs) and GPS-networks, under both soft-attention and average hard-attention, by providing exact logical characterizations. In the setting with real numbers, GPS-networks have the same expressive power as graded modal logic with the (non-counting) global modality (GML+G), relative to vertex properties definable in first-order logic (FO). With floating-point numbers, GPS-networks are equally expressive as graded modal logic with the counting global modality (GML+GC), and this characterization is absolute (not restricted to FO-definable properties). Analogous results hold for GTs in terms of propositional logic with the global modality (PL+G) and its counting variant (PL+GC). A key insight is that the transition from reals to floats swaps relative global counting (possible with reals, lost with floats and with FO) for absolute global counting (impossible with reals, gained with floats).

ABSTRACT. We provide an extended summary of results in our preprint [ 1 ] in which we study the expressive power of message-passing aggregate-combine-readout graph neural networks (ACR-GNNs). Particularly, we focus on the first-order (FO) properties expressible by this formalism. While a tight logical characterisation remains a difficult open question, we make two contributions towards answering it. First, we show that sum aggregation and readout suffice for GNNs to capture FO properties that cannot be expressed in the logic C2 on both directed and undirected graphs. This strengthens known results by Hauke and Wałęga [2] where aggregation and readout functions are specially crafted for the task. Second, we identify two natural ways of restoring characterisability (with regard to C2) for ACR-GNNs. One option is to limit local aggregation (without imposing restrictions on global readout), whilst the second is to run ACR-GNNs over graphs of bounded degree (but unbounded size). In both cases, the FO properties captured by GNNs are exactly those definable by a formula in graded modal logic with global counting modalities. Our results thus establish an innate lower- and upper-bound in terms of how far (fragments of) C2 can be taken to characterise GNNs, and imply that is indeed the unbounded interaction of aggregation and readout that pushes the logical expressive power of GNNs above C

ABSTRACT. Inferring culture media that enable specific metabolic functions is a challenging problem due to the vast combinatorial search space induced by all the possible subsets of compounds and reactions within a metabolic network. Existing scalable approaches based on flux optimization or combinatorial enumeration do not integrate prior biological knowledge to tailor the media to the cell physiological context. We introduce a method that solves culture media inference constrained by biological observation and knowledge as a combinatorial optimization problem, implemented using Answer Set Programming (ASP). This method combines four heuristics that progressively restrict the search space toward biologically supported solutions: (i) identify the target synthesis subnetwork achieving target compounds production, (ii) compute the parsimonious network merging the minimal reaction sets contextualized with the provided constraints, (iii) enumerate minimal media from this reduced search space, and (iv) detect and filter out the self activating internal compounds from the solution space, required for algorithmic reasons but not informative as environmental inputs. We evaluate this approach on different genome-scale metabolic networks and test varying biological constraints and heuristic combinations to assess the method's scalability. This method provides a knowledge-driven and scalable enumeration of minimal culture media, combining logical reasoning, minimality optimizations, as well as knowledge and topology-based constraints to address the combinatorial complexity of the reverse ecology problem.

ABSTRACT. The Chemical Reaction Networks (CRN) interpreted through the differential semantics, even when restricted to elementary reactions with mass action law kinetics, form a Turing-complete language. This means that any computable real function can thus be programmed, and in fact compiled, in an abstract CRN that will compute it with an arbitrarily high precision. In this computational framework, the information carriers are the molecular concentrations, the required precision is given as input, and the output concentration is guaranteed to satisfy the required precision. On the other hand, one can be interested in estimating the derivative of an unknown input signal or in reading the concentration value of an input molecular species. By nature, such problems can only be approximated with a finite precision. Hence, the computation framework proposed previously cannot be applied and we need to design and analyze custom CRNs to perform these tasks. In this paper, we present an analog-dyadic converter CRN which takes as input one molecular concentration (in $[0, 1]$ but not necessarily computable), and produces as output a sequence of ``on'' and ``off'' spikes corresponding to some extent to the sequence of bits in the dyadic representation of the input concentration. We provide a detailed analysis of the source of errors and their behavior when varying the reactions rate constants. We conclude by sketching a possible design for a reader module that takes as input an arbitrary concentration and a desired precision and outputs a dyadic encoding approximating the value of the concentration with the desired

ABSTRACT. Transcriptional networks represent one of the most extensively studied types of systems in synthetic biology. Although the completeness of transcriptional networks for digital logic is well-established, analog computation plays a crucial role in biological systems and offers significant potential for synthetic biology applications. While transcriptional circuits typically rely on cooperativity and highly nonlinear behavior of transcription factors to regulate protein production, they are often modeled with simple linear degradation terms. In contrast, general analog dynamics require both positive and negative nonlinear terms, seemingly necessitating control over not just transcriptional (i.e., production) regulation but also the degradation rates of transcription factors. Surprisingly, we prove that controlling transcription factor production (i.e., transcription rate) without explicitly controlling degradation is mathematically complete for analog computation, achieving equivalent capabilities to systems where both production and degradation are programmable. We demonstrate our approach on several examples including oscillatory and chaotic dynamics, analog sorting, memory, PID controller, and analog extremum seeking. Our result provides a systematic methodology for engineering novel analog dynamics using synthetic transcriptional networks without the added complexity of degradation control and informs our understanding of the capabilities of natural transcriptional circuits. We provide a compiler, in the form of a Python package that can take any system of polynomial ODEs and convert it to an equivalent transcriptional network implementing the system exactly, under appropriate conditions.

ABSTRACT. Aging and Alzheimer’s disease are complex multifactorial processes driven by interacting genetic and metabolic mechanisms, for which single-gene approaches often fail to capture system-level behaviour. Systems biology addresses this challenge by integrating omics data with genome-scale metabolic models (GSMMs) to identify candidate interventions. The Metabolic Transformation Algorithm (MTA) and its robust variant rMTA use constraint-based modelling to predict perturbations that shift a system from a disease-associated toward a healthier metabolic state. To move beyond single-gene prioritization, we applied EA-rMTA, an evolutionary extension of rMTA that searches the combinatorial knockout space by optimizing the robust Transformation Score. We evaluated the framework in two case studies: lifespan-extending unc-62 knockdown in Caenorhabditis elegans and early-onset Alzheimer’s disease (EOAD) in human cortex. In both settings, rMTA found biologically coherent targets and pathway-level signatures consistent with known hallmarks of aging and neurodegeneration. EA-rMTA further identified compact and interpretable multi-gene intervention strategies that outperformed single-gene deletions in shifting the metabolic state toward the desired phenotype. Together, these results show that evolutionary search extends metabolic transformation analysis beyond single-gene perturbations and enables the discovery of experimentally tractable combinatorial intervention hypotheses. More broadly, the framework provides a computational strategy for generating systems-level therapeutic hypotheses in aging, neurodegeneration, and other multifactorial disorders.

ABSTRACT. As is very well known, System F admits (strong) normalization, and it can be proved by combination of Tait's computability predicates and Girard's reducibility candidates. But this approach is not satisfactory for proof theorists who are interested in proof-theoretic ordinals of (fragments of) second-order arithmetic. A more satisfactory approach would be to prove normalization by employing inductive definitions, as it seems to give us some ordinal information on the complexity of normalization. Although it is currently limited to some parameter-free fragments of System F, it is here, we believe, that one finds a small link between lambda calculus and ordinal analysis. In this talk, we revisit some brilliant ideas in the development of lambda caluclus and ordinal analysis (up to 1980's) from a modern perspective. 1. The Joachimski-Matthes method (2003) for proving normalization theorems for the simply typed lambda calculus and its extensions based on inductive definitions instead of computability predicates. 2. The Buchholz method using the Omega rule (1981), which was originally proposed for ordinal analysis, but can also be combined with 1 to obtain a concise proof of normalization for parameter-free fragments of System F. 3. The Altenkirch-Coquand method for proving normalization of a parameter-free fragment (2001), which is based on computability predicates but avoids use of reducibility candidates. Interestingly, this can be construed as a semantic analogue of 2. By reviewing these ideas and extending them, we address the question of how and to what extent one can replace computability predicates and reducibility candidates by inductive definitions when proving normalization.

ABSTRACT. In this talk I will discuss higher-order (“nested”) Kripke models [1], a generalization of traditional Kripke models that is remarkably close to Kripke’s original idea – both mathematically and conceptually. Standard models are now 0-ary models, whereas n-ary models for n > 0 are models whose set of objects (“possible worlds”) contain only (n − 1)-ary models. The models for non-classical logics are introduced after the paradigmatic cases of intuitionistic modal logics IK and M K (a logic stronger than IK) are considered. The n-ary models (for n > 0) define a concept of “alternative” for any substantial interpretation of the (n − 1)-ary models. The key ideas behind the new semantics are the nesting of models, the use of particular worlds w as “designated points” for their own modal definitions, and the use of relations between models at each level n. We start by defining higher-order models as follows: Definition 1 Any Kripke model is a 0-ary model ⟨M, ≻, v⟩, where W is a set of objects, R a binary relation over W , and v a function assigning sets of atoms to elements of W. Definition 2 A n-ary model is a Kripke model ⟨M, ≻, v⟩, where W is a set of (n − 1)-ary models. In the case of IK and M K, 0-ary models are defined as the traditional intuitionistic propositional Kripke models [2, pg. 21], and modal models are defined using only 1-ary models. In order to notationally distinguish between 1-ary and 0-ary models in this abstract, we denote 1-ary models by ⟨M, ≻, f⟩ and 0-ary models K by ⟨W_K, ≤K , vK ⟩. We then move from the abstract definition of model to a concrete intuitionistic one as follows: Definition 3 A set of 0-ary models is homogeneous if its models are de- fined over the same frame (e.g same sets W and relation ≤), and partially homogeneous if it contains a model M such that every other model is de- fined over a generated subframe [3, pg. 28] of the frame of M . Definition 4 An 1-ary model is a model for IK if its set M is partially homogeneous, and a model for MK if it is homogeneous. When we consider n-ary models in general, in any model ⟨M, ≻, v⟩ of level n > 0, validity of □A or ♢A in a world w ∈ M (which is a (n − 1)-ary model) depends only on which formulas are valid in other models w′ of M such that w ≻ w′ whose frames coincide at least in part with that of w. In the case of 1-ary models for IK, this is achieved through the following clauses, where 1 is a 1-ary model, K one of its 0-ary models, and w ∈ WK : ⊨1,Kw □A ⇐⇒ for all w′ with w ≤K w′, if K ≻ K′ and w′ ∈ W_K′ then ⊨1,K′w′ A; ⊨1,Kw ♢A ⇐⇒ there is a K′ with K ≻ K′ such that w ∈ K′ and ⊨1,K′w A; A modal accessibility K ≻ K′ is vacuous whenever the intersection of the objects in the frames of K and K′ is empty. If the intersection is non- empty, something is necessary in a world w iff it is true in all occurrences of the same w or in the w ≤ w′ in other accessible models, and it is possible if it is true in the w of at least one accessible model. Intuitively, given any substantial interpretation of w and M, the defi- nitions consider only alternative versions of the same entities; for instance, if w is interpreted as a particular moment in time and M as a timeline, modal validity in w is defined by considering only what is or is not true in the same moment w in time (or future moments) but in the accessi- ble “alternative timelines”. The traditional interpretation of accessibility relations in Kripke models as establishing different “possible worlds” is now lifted to a higher level and applied to Kripke models themselves by considering differences in the interpretation of their shared structure. This perspective becomes clearer when we consider clauses for MK, which is the strongest possible intuitionistic modal logic obtainable by requiring birelational models to satisfy frame conditions [2, pg. 46][4]. The clauses only considers alternative versions of the same world: ⊨1,Kw □A ⇐⇒ for all K′ such that K ≻ K′, we have ⊨1,K′w A; ⊨1,Kw ♢A ⇐⇒ there is a K′ with K ≻ K′ such that ⊨1,K′w A; The only intuitionistic thing about semantics for MK is the use of intuitionistic 0-ary models, so if we were to use 0-ary models for some other logic we would obtain a (very strong) modal logic for it. Weaker logics can also be obtained, although in some cases (such as that of IK) the semantic clauses might require reference to the specific non-modal relations defined for objects of the models. It is also the case that imposing conditions on n-ary relations for any modal logic yields the semantics traditionally obtained through the same conditions (e.g. by requiring the 1-ary relation to be reflexive and transitive the semantics for IK becomes one for IS4). We are currently working with collaborators to show that, if models are not required to share any structure, the framework provides a semantics for the intuitionistic modal logic WK [5], and a simple modification yields one for CK [4]. We are also investigating new sequent calculi obtainable by reflecting the semantic structures of the new models. The relationship between the semantics and first-order intuitionistic structures is yet to be investigated. Our results indirectly show that a mapping into first-order intuitionistic logic is available by mapping 1-ary models into birelational models, but it is unclear what a “direct mapping” would look like. Although 1-ary validity in models for IK and MK is fully determined by validity in 0-ary models (in the sense that something is valid in a 1-ary model iff it is valid in all its 0-ary models), this needs not always be the case. The framework may be capable of providing Kripke-like semantics to Kripke-incomplete logics if n-ary validity is defined in a way that makes it irreducible to (n − 1)-ary validity. This might open the door to simple but conceptually interesting characterisations of an ever broader class of intuitionistic modal logics, including non-normal ones. Keywords: Intuitionistic Logic, Intuitionistic Semantics, Modal Semantics, Relational Semantics, Higher-order Kripke models. References: [1] Barroso-Nascimento, Victor. “Higher-order Kripke models for intuitionis- tic and non-classical modal logics”. ArXiV Preprint, 2025. Available at: https://arxiv.org/abs/2507.18798 [2] Simpson, Alex “The Proof Theory and Semantics of Intuitionistic Modal Logic”. Ph.D. thesis, 1994. [3] Chagrov, Alexander and Zakharyaschev, Michael. “Modal logic”. Oxford University Press, New York, 1997. [4] Bozic, Milan and Dosen, Kosta. “Models for normal intuitionistic modal logics”. Studia Logica, pgs. 43:217-245, 1984. [5] Wijesekera, Duminda “Constructive modal logics I”. Annals of Pure and Applied Logic, 50:271-301, 1990.

ABSTRACT. In a recent paper, de Groot and Shillito proved that iS4 is sound and complete with respect to all models ⟨W, ⪯, τ, V ⟩, where: ⟨W, ⪯, V ⟩ is a model for IPC, ⟨W, τ ⟩ is a topology, and all open sets of τ are upwards closed with respect to ⪯. Furthermore, they showed that completeness still holds even if we require ⪯ to be the specialisation order of τ . In this sense, iS4 is complete with respect to all topological models. We extend their result in two directions. First, we prove analogous topological completeness results for various logics related to iwK4, an intuitionistic version of the logic wK4 of weak transitive frames. In our setting, we interpret the □ modality via the coderivative operator—the dual of the Cantor derivative—instead of the interior operator. We can also omit the intuitionistic relation ⪯—as long as we interpret it as a coderivative specialisation order. Second, we prove completeness with respect to various classes of bimetric spaces. We do not have completeness if we restrict ourselves to models consisting of an intuitionistic relation and a metrizable topological space: in this setting the ordering ⪯ needs to be the equality relation and so the logic becomes classical.

ABSTRACT. We present a runtime-monitoring framework for vision-based autonomous systems in which a single trained encoder predicts a \emph{semantic basis} of past-time signal-temporal-logic (ptSTL) atoms, and any specification in a fixed fragment is then evaluated by a deterministic, monotone, $1$-Lipschitz decoder derived from the formula's parse tree. The compositional algebraic structure of the decoder lets a single conformal calibration pass certify the entire fragment simultaneously, with no per-formula retraining and no union bound over specifications. We prove that within monotone, $1$-Lipschitz reusable interfaces the semantic basis is the minimum sufficient prediction target. We also introduce a \emph{rolling} architecture that calibrates before temporal aggregation, trading certified tightness at long horizons for an easier per-step learning problem. On a pedestrian-crossroad benchmark and on real-world Waymo driving data, the two architectures cover complementary horizon regimes and decisively outperform a Bonferroni-corrected observer baseline.

ABSTRACT. We present an integrated framework that unifies runtime verification and model-based diagnosis within the stream specification language LOLA. By encoding system descriptions, component health states, and observations into a single stream-based formalism, the approach enables continuous, online fault localization directly alongside fault detection, without requiring separate toolchains. The framework supports both time-invariant and transient faults, and naturally accommodates nondeterministic observations.

ABSTRACT. The 2015 GEO-CAPE ROIC In-Flight Performance Experiment (GRIFEX) is a long-duration CubeSat whose telemetry began exhibiting recurring off-nominal behavior in 2020, late in the mission, motivating verification methods that can support both design-time reasoning and deployable runtime monitoring. Pacti is attractive for this setting because it performs compositional analysis over assume-guarantee contracts, but temporal behavior in Pacti is expressed only indirectly by stitching together scenarios. Mission-time Linear Temporal Logic (MLTL) provides the bounded temporal expressivity needed to state progression and recovery requirements directly, while R2U2 provides a realizable runtime-monitoring backend. We present BB-AGT, a bounded-behavior assume-guarantee translator that lifts named Pacti contracts into bounded future-time MLTL formulas, equips them with predicates such as active, holds, and viol, and lowers the result into machine-generated C2PO monitor specifications for R2U2. We evaluate this translation on a contract model of GRIFEX; on Pacti's Mars entry, descent, and landing scenario; and on a smaller habitat design example. In the GRIFEX study, the resulting model synthesizes one monitor set from 287 contracts and 275 formulas. In the Mars EDL study, BB-AGT turns an allocation-oriented contract model into 9 explicit bounded monitoring formulas and matching runtime monitors.

ABSTRACT. Synergic modeling is a paradigm in which system identity is grounded in coherence constraints over admissible trajectory spaces rather than in state transitions. A coherence constraint C=(φ, ψ) pairs a pointwise predicate φ that excludes instantaneously incoherent crossviewpoint state combinations with a trajectory predicate ψ that bounds their temporal evolution. Instantiated on an adaptive drone, we derive a catalogue of 20 LTL properties verified exhaustively in nuXmv, and show how the same C translates directly into a lightweight runtime monitor embedded in a MAPE-K loop. We claim a design/monitoring duality: a coherence constraint functions as a proof obligation at design time and as an observation specification at runtime, thus connecting formal verification and runtime assurance through a single compositional contract.

ABSTRACT. We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice \emph{dynamically}, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models (or ``languages'') supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lattice (consisting of only High and Low) in the original system.

ABSTRACT. We define a security-typed lambda-calculus with declassification, and develop an environmental bisimulation proof technique for secure information flow in this setting. Unlike traditional security typing that enforces full noninterference, our bisimulation allows proving conditional, intentionally weakened noninterference properties while correctly ``leaking'' (or publishing) part of the high-security information. Despite the long history of this research area and previous work on declassification, this is, to our knowledge, the first result of such a direct approach to the problem of proving noninterference in a higher-order language with declassification. Our technical development is based on novel treatment of \texttt{if}-branches whose conditions are of high secrecy.

ABSTRACT. Attestation means providing evidence that a remote target system is worthy of trust for some sensitive interaction. Although attestation is already used in network access control, security management, and trusted execution environments, it mainly concerns only a few system components. A clever adversary might manipulate these shallow attestations to mislead the relying party. Reliable attestations require layering. We construct attestations whose layers report evidence about successive components of the target system. Reliability also requires structuring the target system so only a limited set of components matters. We show how to structure an example system for reliable attestations despite a well-defined, relatively strong adversary. It is based on widely available hardware, such as Trusted Platform Modules, and software, such as Linux with SELinux. We isolate our principles in a few maxims that guide system development. We provide a cogent analysis of our mechanisms against our adversary model, as well as an empirical appraisal of the resulting system. The performance burden of our attestation is negligible, circa~1.3%. After our first example, we vary our application level, and then also its underlying hardware anchor to use confidential computing with AMD's SEV-SNP. The same maxims help us achieve trustworthy attestations. Keywords. Layered Attestation; Run-Time Attestation; Hardware-based attestation; Copland; Cross-Domain Solutions

ABSTRACT. Why3 relies on logical task transformations both for the translation of verification conditions to- wards external provers and for interactive proof. The kind of metalogical programming involved in these transformations is naturally expressed in higher-order logic programming languages such as λProlog. This paper presents Why3-Elpi, a tool that exposes a typed fragment of the Why3 API to λProlog using Elpi and lets users implement Why3 transformations in λProlog. This provides an environment where non-trivial transformations can be easily prototyped and experimented with, using a declarative and concise style.

ABSTRACT. WebAssembly is a stack-based imperative language widely used to develop safe and efficient Web applications. In this paper, we propose an automated static verification method for a subset of WebAssembly using a constrained Horn clauses (CHCs) satisfiability solver. Our main challenges are how to handle indirect function calls effectively and how to analyze huge panic handlers. A naïve approach to the former problem would be to model a function reference table as an array of functions' entry points, but it would suffer from having too many candidates for indirect calls, resulting in a large case analysis. We address the problem by utilizing type information and filtering candidates for each indirect function call. For the latter problem, a panic handler, which is a function that is called when an error occurs, can be very large and complex. We mitigate this problem by summarizing the panic handler using control-flow analysis. We confirmed the effectiveness of our approach through preliminary experiments.

ABSTRACT. A well-known folklore result about propositional logic is that transforming a formula in disjunctive or conjunctive normal form can lead to an exponential blowup of the formula size. We formalize this result in the form of two theorems in Isabelle/HOL and discuss the challenges we encountered.

ABSTRACT. We present initial work on formally verifying the core of the egg framework in Isabelle/HOL. The egg framework uses e-graphs to perform fast, extensible equality saturation. Congruence closure is a core technique in program analysis and program optimization, serving as a foundation for rewriting systems and enabling efficient reasoning in equational logic. Optimization techniques such as egg's deferred rebuilding mechanism, however, obscure the computation and thus reduce confidence in the results. In this work, we aim to provide a comprehensive, extensible formalization of egg's data structures and algorithms, with a focus on the correctness of deferred rebuilding. Ultimately, we seek to export a verified implementation to Standard ML, enabling trustworthy, executable equality saturation.

ABSTRACT. Standard logical foundations in theorem proving constrain the set of recursive functions that are directly expressible to avoid inconsistencies. However, this prevents us from expressing all Turing-complete computations via direct recursive definitions. We consider Grounded Arithmetic, a reasoning framework that avoids inconsistency from unconstrained recursive definitions by "dynamically type-checking'' terms. Using the formalization of GA in Isabelle/HOL, we prove three self-referential statements to be nonterminating computation: the Liar Paradox, the Truthteller sentence, and Curry's paradox. To do so, we model each statement in GA as a function taking a certain number of steps of computation, and metalogically derive a contradiction if these terms were to terminate. In turn, this allows us to show that these statements have no concrete value in our framework. Using our non-standard inference rules, terms with no concrete value cannot be used in a proof by contradiction, and thus are inert when reasoning about other computations. We then discuss the accessibility of our approach, and how it permits us to avoid common inconsistencies that would otherwise occur when removing constraints from direct recursive definitions in other formal systems.

ABSTRACT. Recent advances in expressiveness of the modal mu-calculus has prompted usage of a generalized Bekic principle with n variables for n>2. However, the only version of Bekic principle known to exist in mathematical literature is for n=2. Indeed, it is non-trivial to even state the principle precisely for more than 2 variables because of the recursive structure involved. This paper presents a precise mathematical statement and proof of the general Bekic principle for any positive n, as well as a mechanization of the proof in Isabelle. As an application, this result serves as a basis of a formal translation from sabotage game logic to recursive game logic, establishing equiexpressiveness to mu-calculus.

ABSTRACT. In social networks, individuals’ decisions are influenced by their local connections, leading to \emph{majority illusion}, where some perceive a local majority opinion that contradicts the global majority. This distortion, prevalent in binary choices such as voting or vaccination stances, can skew public perception, making its mitigation desirable. In our model, we view the network as a \red–\blue colored graph, where a vertex is under majority illusion if its neighborhood has a \red majority despite \blue being globally dominant, and anchoring means flipping selected \red vertices to \blue. Eliminating majority illusion necessitates structural edits to the graph representing the social network. Grandi et al.\ (AAAI 2023) studied edge additions/deletions to reduce illusion, but such changes disrupt natural connections, creating artificial links or removing genuine ones, which are visible and undesirable to users. Instead, we propose \emph{anchoring} vertices---discreetly changing the opinions of selected users (e.g., influencers)---to preserve the network’s structure and hide interventions, offering a practical alternative. Fioravantes et al.\ (AAMAS 2025) aimed to eliminate all illusions with minimum anchors, but this is often impractical. We consider a realistic setting with a budget limiting the number of anchors ($k$) and aim to maximize the number of users ($p$) freed from illusion. Formally, we introduce the 𝑘-ANCH-𝑝-MIE problem: determine whether there is a set $X \subseteq V$ of size at $k$ such that anchoring $X$ eliminates majority illusion for at least $p$ vertices. \textbf{Dichotomy.} We establish the dichotomy regarding the classical computational complexity of the problem: 𝑘-ANCH-𝑝-MIE is polynomial-time solvable for graphs with maximum degree $\Delta \leq 2$, but \NP-complete for $\Delta \geq 3$. \textbf{Tight Exact Algorithm.} We show that the 𝑘-ANCH-𝑝-MIE is \W[1]-hard when parameterized by $k+p$, even for bipartite graphs. Moreover, under the Exponential Time Hypothesis ($\ETH$), there is no $f(k,p)\cdot n^{o(k+\sqrt{p})}$-time algorithm where $n$ denote the number of vertices in the graph (for any computable function $f$), showing that the $n^{O(k)}$-time brute-force algorithm is asymptotically optimal. \textbf{Tight Approximation Results.} Finally, complementing our hardness results, for the natural maximization version of the problem--- where the goal is to anchor $k$ vertices to eliminate majority illusion from as many vertices as possible--- we establish a tight $(1-\frac{1}{e})$-approximation via a natural greedy algorithm matching the optimal threshold for submodular maximization. We also prove that this is essentially optimal: no polynomial-time algorithm, can achieve an $(1-\frac{1}{e}+\epsilon)$-approximation for any $\epsilon>0$ unless $\P=\NP$. Moreover, under \ETH, any algorithm achieving an $(1-\frac{1}{e}+\epsilon)$ approximation factor for any constant $\epsilon\in(0,1)$, must take runtime $\Omega_k(|S|^{k^{\Omega(1)}})$, where $S$ denote the set of vertices that can possibly be anchored in the input graph.

ABSTRACT. Pearl’s Causal Hierarchy (PCH) is a central framework for reasoning about probabilistic, interventional, and counterfactual statements, yet the satisfiability problem for PCH formulas is computationally intractable in almost all classical settings. We revisit this challenge through the lens of parameterized complexity and identify the first gateways to tractability. Our results include fixed-parameter and XP-algorithms for satisfiability in key probabilistic and counterfactual fragments, using parameters such as primal treewidth and the number of variables, together with matching hardness results that map the limits of tractability. Technically, we depart from the dynamic programming paradigm typically employed for treewidth-based algorithms and instead exploit structural characterizations of well-formed causal models, providing a new algorithmic toolkit for causal reasoning.

ABSTRACT. Every flow on a DAG can be decomposed into weighted paths. The Minimum Flow Decomposition (MFD) problem, which is strongly NP-hard, asks for a smallest set of weighted paths whose sum is equal to the flow. This problem is crucial in various fields, including transportation planning, network communication, and bioinformatics, which has driven the development of fast heuristic algorithms. In this talk, I will give an overview of current theoretical results of the problem, focusing on its relations to DAG parameters, such as minimum path covers, and its connections to structural theory of DAGs. I will also present algorithmic results and improvements on a practical ILP solver for MFD based on this theoretical work.

ABSTRACT. Anil Nerode is Goldwin Smith Professor of Mathematics and Computer Science at Cornell University. He is “a pioneer in mathematical logic, computability, automata theory, and the understanding of computable processes, both theoretical and practical for over half a century, whose work comes from a venerable and distinguished mathematical tradition combined with the newest developments in computing and technology.”

ABSTRACT. We posit that prior and ongoing work on hidden layer neuron analysis gives rise to a neurosymbolic approach to improved cyber-physical systems control via a runtime monitoring system that combines deep neural networks and formal reasoning over knowledge graphs. Such a system would continuously observe neuron activation states (interpreted via neuron labels as system perceptions), assess whether the system perceptions are compatible with actual sensor readings, and suppress system control actions that are deemed as likely mispredictions.

ABSTRACT. For the past two years, I have been the Diversity Manager of the Faculty of Mathematics and Computer Science at the University of Bremen. In this talk, I will give an insight into my everyday work: supporting students in difficult situations, identifying barriers faced by people from diverse backgrounds, and developing measures to make faculty life more inclusive. I will also speak about our outreach activities, current challenges, and the small and large steps we take to improve participation, belonging, and equal opportunities in our faculty.

ABSTRACT. When a certifying solver claims that a solution is optimal or that a problem is unsatisfiable, it demonstrates this convincingly by giving a proof log which can be checked by an independent (and ideally formally verified) proof checker. Such an approach should also be viable for enumeration problems (“I have listed all solutions explicitly”) and counting problems (“there are exactly 42 solutions”), but the currently most popular proof logging systems contain several vital features which are incompatible with this goal. We explain how the VeriPB system can be modified for enumeration and counting proofs whilst retaining as much as possible of its powerful “strengthening” and “deletion” features. We implement this extension both inside VeriPB’s user-friendly proof checker and elaborator and the formally verified CakePB backend, and use this to obtain formally verified enumerations of solutions for a range of constraint solving and graph problem instances.

ABSTRACT. Tensor networks and circuits are widely used data structures to represent pseudo-Boolean functions. These two formalisms have been studied primarily in separate communities, and this paper aims to establish equivalences between them. We show that some classes of tensor networks that are appealing in practice correspond to classes of circuits with specific properties that have been studied in knowledge compilation as tractable circuits. In particular, we prove that matrix product states (tensor trains) coincide with nondeterministic edge-valued decision diagrams and that tree tensor networks exactly correspond to structured-decomposable circuits. These correspondences enable direct transfer of structural and algorithmic results; for example, canonicity and tractability guarantees known for circuits yield analogous guarantees for the associated tensor networks, and vice versa.

ABSTRACT. Given a relational specification \varphi(X, Y_1, ... Y_n), functional synthesis concerns the construction of functions (or terms) F_1(X), ... F_n(X) such that \varphi(X, F_1, ... F_n) is semantically equivalent to \exists Y_1, ... Y_n \varphi(X, Y_1, ... Y_n). Such functions are also called Skolem functions, and their algorithmic synthesis has many applications, including in program synthesis, QBF-SAT certificate generation, circuit repair, reactive synthesis, planning and the like. The synthesis problem is intractable unless long-standing complexity-theoretic conjectures are falsified. Fortunately, polynomial-time synthesis algorithms can be designed if \varphi is represented in special normal forms. In this talk, we present some such normal forms when \varphi is a formula in propositional logic or in Presburger arithmetic. We show that normal forms originally studied in AI and formal verification, and others like Synthesis Negation Normal Form (SynNNF) and Subset And-Unrealizable Normal Form (SAUNF) lead to efficient functional synthesis in the Boolean setting. Then, we also discuss a new normal form, Presburger Synthesis Normal Form (or PSyNF)for Presburger specifications that allows us to efficiently extract Skolem functions as Presburger terms. We discuss properties of and relations between these normal forms, and show that every universal representation that admits polynomial-time synthesis is polynomially reducible to SAUNF (for Boolean functional synthesis), and to PSyNF (for Presburger functional synthesis with one output).

ABSTRACT. This talk highlights recent advances in the Global Benchmark Database (GBD), a unified infrastructure for benchmark and metadata management in NP-hard domains. These advances include canonical isomorphism-aware labeling, lightweight extensibility, and sustainable, data-driven benchmarking workflows for efficient comparative evaluation.

ABSTRACT. Solvers for NP-hard problems from areas such as automated reasoning or optimisation are complex systems in which many different components interact. The performance of these solvers is the result of an intricate interplay between implementation details, algorithmic concepts and heuristics. This, alongside the complexity of the problem instances to be solved, makes it challenging to assess the effect of a single idea on the overall performance of a given solver. It is therefore not only crucial, but also challenging to evaluate the performance impact of new ideas. Existing reliable evaluation methods require large sets of diverse benchmark instances and considerable amounts of computing resources. This makes empirical evaluation a bottleneck for solver development, as it is time-consuming and energy-intensive, often requiring several CPU years of computation to evaluate the impact of a single idea. In recent years, this bottleneck has led to the development of data-driven approaches that can dynamically select a smaller number of instances that provide sufficient statistical evidence to evaluate the relative performance of a given set of solvers. However, these methods are typically not easily accessible. In this work, we present a tool that implements these methods and makes them readily accessible to solver developers, thus enabling them to obtain swifter feedback on their ideas.

ABSTRACT. Benchmarking is a widely-used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in several competitions (such as the International Competition on Software Verification), and is used by several research groups worldwide to ensure reliable benchmarking.

ABSTRACT. The theory of arrays with select and store plays an important role in software verification and is therefore supported by virtually all state-of-the-art SMT solvers. There are many extensions, for instance by constant arrays, element-wise function applications, counting, or projections, that have been shown to preserve decidability. In recent work, a theory of arrays extended by constant arrays and sum predicates, called summation array logic (SAL), has been introduced and proven to be decidable in non-deterministic polynomial time. In SAL, it is possible to state assertions about the sum of all entries in a (finite or infinite) array of integers. This paper provides an eager approach to the satisfiability problem in SAL. The approach transforms a SAL formula to an equi-satisfiable formula in the theory of extensional arrays (extended with constant array operator), which can then be decided by an off-the-shelf SMT solver. The transformation produces a formula at most quadratic in the size of the input formula. Since there are no standard array benchmarks with sum constraints yet, the paper presents a new set of such benchmarks obtained by mutating existing SMT-LIB array benchmarks. The experiments show that the transformation-based decision procedure incurs only a relatively small overhead in terms of solving time.

ABSTRACT. Locality properties enable hierarchic and incremental satisfiability checking in theory extensions. In the context of Satisfiability Modulo Theories (SMT), locality reasoning provides an attractive way to obtain satisfiability procedures for various extensions of the theory of equality, including theories specifying data structures. We establish locality properties of expressive array theories that incorporate universal quantifiers and cardinality constraints.

ABSTRACT. Many verification tasks in computing require precise, unbounded relational reasoning. The cvc5 SMT solver provides some support for such tasks in the form of a relational solver that can automatically determine the satisfiability of sets of constraints over a simple set of relational operators. However, the current solver is quite limited in its ability to reason about more complicated concepts, such as transitive closure and cyclicity. In this paper, we propose extending the cvc5 relational solver with native support for reasoning about relational cyclicity. We propose two new predicates, acyclic and minimal, and we argue that these extensions will enable cvc5 to tackle more challenging tasks, such as reasoning about microarchitectural memory consistency models.

ABSTRACT. Proving termination or non-termination of lasso programs is a challenging problem in program verification. To unify state-of-the-art approaches under a common execution framework, we present PaSTTeL, a modular and generic parallel portfolio framework for termination and non-termination analysis of lasso programs. PaSTTeL is designed to: (1) facilitate the integration of new analysis algorithms into the portfolio, (2) execute registered strategies concurrently, and (3) act as a self-contained library component that can be seamlessly embedded into any external project requiring (non-)termination analysis. Initial experiments demonstrate that an instantiation of PaSTTeL performs competitively against state-of-the-art tools.

ABSTRACT. Linear-constrained loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open for linear-constrained loops over integers, rationals, and reals. We focus on loops over integers and show that they are tightly connected to generalized Collatz sequences – integer sequences generated by maps that are linear on each residue class modulo a fixed natural number. We prove that ter- mination of one-variable linear-constrained loops is decidable in polynomial time, provided a long-standing conjecture about generalized Collatz sequences holds. Conversely, we show that any decision procedure for one-variable loops would prove or refute specific instances of this conjecture, which remain open. Moreover, we show that if a one-variable loop has a cyclic trace, then it also has a cyclic trace of length at most two.

ABSTRACT. We consider linear single-path loops of the form while φ do x ← Ax + b where x is a vector of variables, the loop guard φ is a conjunction of linear inequations over the variables x, and the update of the loop is represented by the matrix A and the vector b. It is already known that termination of such loops is decidable. In this work, we consider loops where A has real eigenvalues, and prove that it is decidable whether the loop's runtime (for all inputs) is bounded by a constant if the variables range over R or Q. This is an important problem in automatic program verification, since safety of linear while-programs is decidable if all loops have constant runtime, and it is closely connected to the existence of multiphase-linear ranking functions, which are often used for termination and complexity analysis. To evaluate its practical applicability, we also present an implementation of our decision procedure.

ABSTRACT. Presentation of the results of termCOMP 2026

ABSTRACT. Real-life social interactions are complex and multifaceted, with different relationship types creating overlapping, interdependent networks. Understanding this complexity requires aggregating multiple individual social networks into a single, collective meta-network. Social networks possess many desirable properties. When each individual social network satisfies certain beneficial characteristics, it is natural to consider how the aggregation process can preserve these reserved properties. While with the cognitive and spatial limits of individual social networks, they always meet several deficiencies. We suggest a shift in how social network aggregation is understood. Instead of mere preservation, explore its potential as an active, corrective tool to eliminate these social network deficiencies. By synthesising diverse individual perspectives, we aim to use aggregation not only to reflect localised observations but also to uncover the true underlying social structures and to correct the inherent imperfections of individual networks. In this paper, we first represent social networks as undirected graphs $G = \langle A,E \rangle$ \cite{barabasi2014linked}. Building upon this graph-based approach, we formalise several properties inherent in social networks, including ``connectivity''\footnote{A social network is said to satisfy the property of connectivity if for every pair of distinct vertices \( u, v \in A \), there exists a path from \( u \) to \( v \).}, ``six degrees of separation''\footnote{A social network satisfies six degrees of separation if \(\forall \; a, b \in A \quad |P(a,b)| \leq 6\). Here $P(a, b)$ denotes the shortest path from $a$ to $b$.}, and ``weak ties''. Within our framework, when a social network lacks a desirable property or exhibits negative phenomena such as the ``majority illusion’’\footnote{The consensus among members of the local actor set regarding the existence of ties directly contradicts the global reality.}, we refer to these conditions as social network deficiencies. We employ the axiomatic method, rooted in social choice theory, to more thoroughly investigate the aggregation of social networks. Building on the framework of graph aggregation \cite{endriss2018graph}, our initial focus was on preserving desirable network properties. On the positive preservation side, we demonstrate that certain democratic aggregation rules, such as the nomination rule, preserve properties that strengthen network connections, such as connectivity, while others lead to impossibility results requiring oligarchic or dictatorial rules \cite{yi2026sna}. Despite these preservation results, a critical transition in our research was necessitated by the reality of observed social networks. Since we recognise that observed individual networks are inherently flawed due to epistemic limitations and cognitive boundaries, individual social networks frequently fail to exhibit the preferred structure and display several deficiencies. We pivot from standard preservation to a novel perspective. Can we use aggregation as a means to eliminate social network deficiencies? We reinterpret Condorcet's paradox within a social network context, treating aggregation as a corrective mechanism rather than a source of collective irrationality in preference aggregation. We demonstrate this corrective potential by aggregating a Condorcet-like profile of social networks. In classical social choice, Condorcet's paradox illustrates cyclic majorities and irrational outcomes. However, our network-theoretic reinterpretation yields a starkly contrasting result. We show that while the individual networks in the profile fail to satisfy triadic closure\footnote{A social network satisfies triadic closure if for any three distinct vertices $a,b,c\in A$, $(a,b),(b,c)\in E$ implies $(a,c)\in E$.}, the aggregated collective network successfully achieves it. This restatement provides a powerful proof of concept that aggregation can indeed eliminate structural defects. However, applying classic social choice axioms to eliminate network defects introduces severe theoretical limits. We establish a strong negative baseline: no aggregation rule that is both unanimous and grounded can eliminate a network deficiency if all individuals share the exact same flawed structure. To circumvent this negative baseline and develop a positive corrective framework, our ongoing research investigates two approaches of theoretical relaxation. The first is domain restrictions on profiles \cite{dietrich2010restrictdomains}. Rather than demanding a universal elimination of deficiencies across all conceivable profiles, we explore domain restrictions by imposing structural constraints on the individual input networks. Our goal is to find out under which profile or network conditions and constraints certain aggregation rules can effectively eliminate these social network deficiencies. Another consideration is about relaxing groundedness for structural inference. Similar to scholars who reject independence in judgment aggregation to avoid logical paradoxes\cite{list2002rejectindependent}, we challenge the groundedness axiom. Strict groundedness forces the collective networks to inherit individuals' local blind spots. However, an unobserved edge does not always mean there is no information transfer in a social network; it is sometimes just a limited viewpoint rather than a true disconnection. We relax this axiom to view aggregation as a process of uncovering the true social structure. This empowers the aggregation rule to perform structural inference, identifying ``latent ties'' (e.g., inferring an unobserved $(A,C)$ link from existing $(A,B)$ and $(B,C)$ guarantee the information transport between $A$ and $C$) and bridging these unobserved gaps to eliminate the social network deficiencies.

ABSTRACT. In this work, we argue that ignorance can be inherently understood as a hyperintensional notion. When faced with two logically or necessarily equivalent propositions, an agent may be ignorant of one while not of the other. To capture formally this intuition, we employ a topic-sensitive semantics, enabling the modeling of an agent's attitude toward the content of a proposition. Within this framework, we reevaluate three existing logical systems, usually characterized by standard Kripke semantics, to account for three forms of ignorance: ignorance whether, ignorance as unknown truth, and disbelieving ignorance. For each form, we present a sound and complete system. To highlight the advantage of this approach, we apply it to address the problem of logical omniscience rephrased in terms of ignorance. The resulting framework considers an agent's capacity to grasp the content of a proposition, bridging the gap between standard relational settings for ignorance representation and natural intuitions about the role of content in forming one's ignorance.

ABSTRACT. This work-in-progress project is motivated by enhancing our theoretical understanding of the information exchange that leads to belief polarization. We approach this subject with the aim of using modal logic to model agents that update their beliefs based on the bias they already have. We propose a direction that builds on known formalisms in doxastic and epistemic logic where we add an update operation to an agents' strength of evidence, which leads to a stronger belief. This abstract briefly discusses these ideas and outlines objectives of on-going work.

ABSTRACT. Probabilistic programs extend ordinary programs by the abilities to sample values from probability distributions and conditioning. They are ubiquitous in modern computing and appear, for example, in randomized algorithms, random sampling, statistical inference routines, cognitive science, and autonomous systems. A formal (denotational) program semantics associates each program with a function mapping (non-negative) measures over input states to measures over output states. A fundamental computational task in probabilistic programming is to infer a program's output (posterior) distribution from a given initial (prior) distribution. This problem is challenging, especially for expressive languages that feature loops or unbounded recursion. We aim to push the limits of exact automatic loop analysis. More formally, given a discrete probabilistic loop and a discrete initial distribution over program states, we want to automatically compute an exact representation of the output distribution. Due to standard undecidability results for while loops, there is no hope for a complete algorithmic solution for exact inference. Our goal is thus to provide heuristics covering reasonably many instances. To achieve this, we combine generating functions as a representation for (infinite-support) distributions with a seemingly less well-known characterization of a loop's output distribution through its occupation measure due to Sharir et al.

ABSTRACT. Unbounded demonic nondeterminism occurs when modelling C-like memory allocation and termination under weak fairness. This ongoing work considers the addition of unbounded demonic nondeterminism to weighted programming and the soundness of weakest precondition-like semantics.

ABSTRACT. Randomized algorithms depend on accurate sampling from probability distributions, as their correctness and performance hinge on the quality of the generated samples. However, even for common distributions like Binomial, exact sampling is computationally challenging, leading standard library implementations to rely on heuristics. These heuristics, while efficient, suffer from approximation and system representation errors, causing deviations from the ideal distribution. Although seemingly minor, such deviations can accumulate in downstream applications requiring large-scale sampling, potentially undermining algorithmic guarantees. In this work, we propose statistical distance as a robust metric for analyzing the quality of Binomial samplers, quantifying deviations from the ideal distribution. We derive rigorous bounds on the statistical distance for standard implementations and demonstrate the practical utility of our framework by enhancing APSEst, a DNF model counter, with improved reliability and error guarantees. To support practical adoption, we propose an interface extension that allows users to control and monitor statistical distance via explicit input/output parameters. Our findings emphasize the critical need for thorough and systematic error analysis in sampler design. As the first work to focus exclusively on Binomial samplers, our approach lays the groundwork for extending rigorous analysis to other common distributions, opening avenues for more robust and reliable randomized algorithms.

ABSTRACT. We present a practical acceleration of recent quasipolynomial-time progress measure algorithms for parity games. For this, we combine a novel Strahler-universal tree encoding with data-parallel (SIMD) computation. Our key contribution is showing that common instances admit very small structural parameters, enabling compact representations that fit into SIMD registers. This insight allows us to redesign the core lifting (i.e. successor computation) step into a parallel form, yielding significant empirical speedups over existing implementations. This work demonstrates that bridging algorithmic structure (Strahler measures) with hardware-aware optimization (SIMD) can materially improve parity game solving.

ABSTRACT. Reactive synthesis with non-integer discounted-sum objectives is solved by Bansal et al. (AAAI 2022) via the DSLow comparator automaton, which under-approximates the running sum and reduces the problem to a Büchi game on the product of the arena and comparator. Their construction allocates the full product upfront and explores it by BFS, incurring two costs: many product states are structurally unreachable (ghost states), and BFS defers winning states behind a wide shallow frontier. We propose (1) a lazy on-the-fly construction that materializes only reachable states, and (2) a priority-guided exploration keyed on U − c (distance to comparator saturation) with interleaved backward propagation. On the standard benchmarks, our approach constructs 74– 99% fewer states and discovers the first winning state up to 22× faster, with identical winning regions. Weight-specific asymmetric comparator bounds additionally cut the theoretical state space by 40–50% at no cost.

ABSTRACT. We study the synthesis of policies for stochastic systems acting on behalf of multiple principals with heterogeneous time preferences. We model this setting using asymmetrically-discounted Markov decision processes (MDPs), where each principal possesses an individual reward function and discount factor. The objective is to synthesize policies maximizing a utilitarian notion of social welfare, defined as the aggregate discounted payoff across all principals. Heterogeneous discounting fundamentally changes the structure of optimal policies: in contrast to classical discounted MDPs, welfare-optimal policies are generally not positional, even when all principals receive identical rewards. Nevertheless, we establish that optimal policies admit a simple structure: pure finite-memory counting strategies suffice and can be synthesized in polynomial time under mild assumptions on the spacing of discount factors. We further show that restricting synthesis to stationary strategies leads to computational intractability: deciding whether there exists a stationary strategy achieving a given welfare threshold is NP-hard, even for two principals with identical rewards. Our results highlight how heterogeneous temporal preferences introduce new synthesis challenges at the intersection of formal methods, multi-agent planning, and algorithmic game theory.

ABSTRACT. This talk is based on two joint works with Pete Austin, Nicolas Mazzocchi, and Patrick Totzke published in FOSSACS 2024 and CONCUR 2025. Temporal graphs are graphs where the edge relation changes over time. This model has been used to analyse dynamic networks and distributed systems in dynamic topologies. We consider temporal graphs where the edge availability relation is given by an existential Presburger formula with a free variable such that an edge e is available at time t if and only if the formula evaluated with the free variable assigned value t is true. This allows succinct encoding of temporal graphs, while also capturing (ultimately) periodic temporal graphs. In this talk, we will consider the complexity of solving games played on (succinct) temporal graphs. In particular, our results show that reachability and parity games on temporal graphs are PSPACE-complete. In fact, the PSPACE-hardness also holds on 1-player temporal graphs. We also consider games with explorability objective, where one player tries to visit all the vertices of a graph. Explorability is a well studied topic in temporal graphs. We show that the game version of the explorability problem is PSPACE-complete even when the temporal graph is presented as a sequence of static graphs.

ABSTRACT. Given rationals α and β, the sure-almost-sure problem for an objective φ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have φ-value at least α (i.e., sure α satisfaction), and with probability 1 the outcome has φ-value at least β (i.e., almost-sure β satisfaction). The sure-limit-sure problem asks if for all ε > 0, one can simultaneously ensure that all outcomes have φ-value at least α, and with probability at least 1 − ε the outcome has φ-value at least β. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this. In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that the average payoff of a finite window that slides over an infinite run be greater than a given threshold. We study two variants of window mean payoff; for both variants we show that sure-almost-sure problem and the sure-limit-sure problem are no harder than sure satisfaction and almost-sure satisfaction when considered separately for these objectives.

ABSTRACT. Signature-based abduction in description logics (DLs) seeks the weakest sufficient hypothesis, formulated over a designated signature, that together with a background ontology explains a given observation. When no informative hypothesis is expressible within the allowed signature, existing methods based on weak forgetting inevitably produce degenerate, inquiry-blocking results such as $A\sqsubseteq\bot$. We formalize \emph{definitorial abduction}, which returns a pair $\langle\mathcal{H},\mathcal{X}\rangle$: the hypothesis $\mathcal{H}$ respects the signature restriction, while a definitorial extension $\mathcal{X}$ introduces fresh concept names anchored to the original ontology through conservative definitorial axioms. Standard signature-based abduction is the special case $\mathcal{X}=\emptyset$. To realize definitorial abduction, we develop a sound, complete, and terminating Ackermann-style strong forgetting calculus for acyclic $\mathcal{ALCI}$ ontologies. The key technical contribution is the \emph{$\exists$-surfacing rule}, which resolves a fundamental incompleteness of the Ackermann framework when a concept name to be eliminated occurs under existential restrictions in both polarities. The unnamed concept names that this rule introduces are precisely the fresh symbols that definitorial abduction exploits. We implement our approach and evaluate it on 547 real-world ontologies: 20--29\% of instances require unnamed concept names, confirming the practical prevalence of cases where standard abduction degenerates; our prototype is 36\% faster on average than the only existing baseline.

ABSTRACT. We consider and extend results on basic path logic and the related ordered fragment of first-order logic, both of which originate from the functional translation of modal logic. Using saturation-based theorem proving methods, we solve uniform interpolation for the former and second-order quantifier elimination for the latter. Basic path logic is a subclass of the ∃∗ ∀∗ -fragment and has the remarkable property that binary resolution decides it. This decidability result and the consequence finding completeness of binary resolution allows us to observe that binary resolution also decides uniform interpolation and computes uniform interpolants for basic path logic. By introducing constant Skolemisation, we show that sentences of the ordered fragment can be mapped into basic path clauses, and this mapping preserves logical consequences in the ordered fragment. We characterise the search space of the SCAN algorithm on the ordered fragment by a variation of basic path logic and prove that SCAN terminates on this class, and therefore it decides second-order quantifier elimination for this class and the ordered fragment. Finally, we propose a method for extracting uniform interpolants in the ordered fragment from the output of SCAN.

ABSTRACT. We present a first draft of an algorithm to solve existential Boolean unification with predicates. The algorithm is based on Herbrand's theorem, the witness construction for quantifier-free Boolean unification and the formula instantiation problem.

ABSTRACT. Complex space systems, such as those deployed in orbital or deep-space environments, are increasingly reliant on the seamless integration of heterogeneous components operating in harsh, unpredictable conditions. While the necessary system requirements are usually extracted from multiple stakeholders, norms, and regulations in natural language, this approach often leads to dangerous ambiguities. Formal languages offer a rigorous means of expressing these requirements unambiguously, while enabling the detection of realizability issues and inconsistencies. In uncertain environments such as in space, stochastic modeling of subsystems is preferred to reason about the probability of a requirement holding or to estimate expected operational costs. In this talk, I present two tools for addressing these challenges: NASA’s FRET for eliciting deterministic and probabilistic requirements from structured natural language, and ULTIMATE for verifying stochastic world-models. We will end with a discussion on how these tools can be applied to complex space systems to bridge the gap between high-level requirements and rigorous, automated formal system verification.

ABSTRACT. The Plan Execution Interchange Language (PLEXIL) is an event-driven synchronous language developed by NASA to support autonomous spacecraft operations. Due to the safety- and mission-critical applications of PLEXIL, its semantics has been formalized and key properties of the language have been formally verified. Two of the properties explored in the formalization are operational determinism, which states that the only source of non-determinism in a PLEXIL execution is the external environment, and run-to-completion, which states that under well-defined assumptions, external events trigger a chain of internal computations that eventually terminate. This paper presents an overview of the formal semantics of the current version of the language, PLEXIL 6.

ABSTRACT. Observation planning is the task of scheduling the operations of a satellite constellation to take pictures of a set of regions of interest and sending these observations down to Earth. With large constellations, uncertain observation conditions, e.g. due to clouds, and limited availability of downstream capacity, it becomes increasingly hard to coordinate the operations. We address the setting where satellites have limited memory, and pictures need to be sent through the constellation to a satellite that can transmit them to a ground station. A key challenge in this problem is the highly dynamic environment, which requires a robust planning system that can quickly adapt to changes. We propose a framework based on facet reasoning, which, unlike traditional planners that provide a single fixed solution, allows for dynamic updates to the current solution without replanning from scratch. We show empirically that facets offer a scalable approach for constellation planning and illustrate the robustness in a case study.

ABSTRACT. Driven by the surmounting interest for dedicated infrastructure in cislunar space, this work considers the satellite constellation design for cislunar space situational awareness (CSSA). We propose a mixed-integer linear programming (MILP)-based formulation that simultaneously tackles the constellation design and sensor-tasking subproblems surrounding CSSA. Our approach generates constellation designs that provide coverage with considerations for the field of view of observers. We propose a time-expanded p-median problem (TE-p-MP) that considers the optimal placement of p space-based observers into discretized locations based on orbital slots along libration point orbits, simultaneously with observer pointing directions across discretized time. We further develop a Lagrangian method for the TE-p -MP, where a relaxed problem with an analytical solution is derived, and customized heuristics leveraging the orbital structure of candidate observer locations are devised. The performance of the proposed formulation is demonstrated with several case studies for CSSA constellations monitoring the cislunar Cone of Shame and a periodic time-varying transit window for low-energy transfers located in the Earth–Moon L2 neck region. The proposed problem formulation, along with the Lagrangian method, is demonstrated to enable a fast assessment of near-optimal CSSA constellations, equipping decision-makers with a critical technique for exploring the design trade space.

ABSTRACT. We propose a framework for compositional verification of higher-order effectful programs based on operational game semantics. Starting from a monadic evaluator for a programming language, the framework derives interactive models of open program components as monadic transducers indexed by games. Their composition is defined by a bidirectionnal synchronization process based on feedback loops, in the style of Geometry of Interaction, and expressed algebraically through a trace operator induced by monadic iteration. This provides a common structure for approximating both evaluation and composition, opening the way to abstract-interpretation techniques for computing or over-approximating the behaviour of composed components. The approach is illustrated by ongoing implementation work in the CAVOC project for OCaml modules.

ABSTRACT. Many verification techniques rely on lifting a system signature from a category of state spaces to a category of predicates, relations, metrics, or other proof objects. Codensity lifting provides a general method for constructing such liftings and has led to applications in fibrational bisimulation, quantitative reasoning, modal logics, and compositional verification. However, the literature often introduces new categorical machinery for each particular instance, making it difficult to identify the general structure that explains why these constructions work. This talk presents work in progress towards a 2-categorical account of codensity lifting. The aim is to separate the formal part of the construction from the application-specific verification data. From this perspective, several existing results on codensity lifting arise as instances of general fibrational and 2-categorical principles.

ABSTRACT. We present a parameterised algebraic theory for classically controlled quantum communication, together with two sound models -- a quantum-stream-based operational semantics and a monadic denotational semantics. The two models induce the same notion of program equivalence -- the denotational one is adequate and fully abstract with respect to the operational one. We view this as a first step towards equational verification of quantum communication protocols.

ABSTRACT. Neural networks hold great potential to act as approximate models of nonlinear dynamical systems, with the resulting neural approximations enabling verification and control of such systems. However, in safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system. To address this fundamental challenge, we propose a novel, adaptive, and parallelizable verification method based on certified first-order models. Our approach provides formal error bounds on the neural approximations of dynamical systems, allowing them to be safely employed as surrogates by interpreting the error bound as bounded disturbances acting on the approximated dynamics. We demonstrate the effectiveness and scalability of our method on a range of established benchmarks from the literature, showing that it significantly outperforms the state-of-the-art. Furthermore, we show that our framework can successfully address additional scenarios previously intractable for existing methods -- neural network compression and an autoencoder-based deep learning architecture for learning Koopman operators for the purpose of trajectory prediction.

ABSTRACT. The specification and verification of temporal properties is crucial to assess the safety of monitoring systems. Said systems need to ensure that certain properties are validated during its full operation time. The rich pattern-finding capabilities of deep learning are a strong incitation to implement such monitors as neural networks. However, neural networks verification historically focused on properties related to a single point in time. In this paper, we present a way to encode Linear Temporal Logic (LTL) properties in a neural network specification language. We derive from this encoding an automated translation to existing off-the-shelf provers. We apply our system to the verification of an industrial use case: a monitoring system for batch distillation. We were able to successfully specify and verify most of the properties in a small runtime.

ABSTRACT. Neural network controllers for autonomous decision-making are well-established in cyber-physical systems, yet their deployment in safety-critical healthcare settings remains largely unverified. This paper presents a methodology and case study for the formal verification of a neural network controller for antibiotic dosing, motivated by the challenge of systems that must be simultaneously adaptive and provably safe across unbounded time horizons. We construct a simplified yet clinically-interpretable model that tracks drug concentration, body temperature, and white blood cell count. Vancomycin is selected as a representative antibiotic, widely prescribed for severe infections yet carrying a narrow therapeutic window, where supratherapeutic concentrations risk nephrotoxicity and subtherapeutic dosing risks treatment failure. A supervised neural network controller is trained on synthetic clinician-style dosing data. We establish formal verification of input-output safety properties, specifically verifying a property of a neural network that implies an infinite-horizon proof that automated dosing never exceeds the supratherapeutic boundary. This system property is proven in Rocq using the Vehicle interactive theorem prover backend to integrate the different proof systems. The end result is a verification pipeline that allows for a wide variety of treatment approaches whilst maintaining safety for each specific patient.

ABSTRACT. We present our ongoing work on the veriFIRE project: a collaboration between industry and academia, aimed at applying verification to increase the reliability of a real-world, safety-critical system. The system we target is an airborne platform for wildfire detection, which incorporates two deep neural networks. We present an end-to-end methodology for verifying consistency properties of this system. Our approach encodes application-grounded requirements into solver-compatible queries for existing neural network verifiers. We study properties of interest over critical operational scenarios: (i) monotonicity of detector confidence as target intensity increases; and (ii) bounded detector response under physically plausible blur over the sensor. We instantiate these encodings using state-of-the-art neural network verification backends and evaluate them at scale on real background samples. For the first property, all verification queries are solved in under five minutes. For the second property, verification is substantially harder, highlighting key scalability challenges for richer, higher-dimensional specifications. Overall, the results demonstrate that meaningful, domain-specific guarantees can be obtained for industrial systems.

ABSTRACT. Translating human-written mathematical theorems and proofs from natural language (NL) into formal languages (FLs) like Lean 4 has long been a significant challenge for AI. Most state-of-the-art methods either focus on theorem-only NL-to-FL auto-formalization or on FL proof synthesis from FL theorems. In practice, auto-formalization of both theorem and proof still requires human intervention, as seen in AlphaProof’s silver-medal performance at the 2024 IMO, where problem statements were manually translated before automated proof synthesis. We present ProofBridge, a unified framework for automatically translating entire NL theorems and proofs into Lean 4. At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem+proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant FL examples to guide translation. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean’s type checker and semantic equivalence feedback to ensure both syntactic correctness and semantic fidelity. Experiments show substantial improvements in proof auto-formalization over strong baselines (including GPT-5, Gemini-2.5, Kimina-Prover, DeepSeek-Prover), with our retrieval-augmented approach yielding significant gains in semantic correctness (SC, via proving bi-directional equivalence) and type correctness (TC, via type-checking theorem+proof) across pass@k metrics on miniF2F-Test-PF, a dataset we curated. In particular, ProofBridge improves cross-modal retrieval quality by up to 3.28x Recall@1 over all-MiniLM-L6-v2, and achieves +31.14% SC and +1.64% TC (pass@32) compared to the baseline Kimina-Prover-RL-1.7B.

ABSTRACT. As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be ensured throughout their entire operation, necessitating infinite-time horizon verification. To verify the infinite-time horizon safety of NNCSs, recent approaches leverage Differential Dynamic Logic (dL). However, these dL-based guarantees rely on idealized, real-valued NN semantics and fail to account for roundoff errors introduced by finite-precision implementations. This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations --- in sensing, actuation, and computation --- into the safety verification. We model the problem as a hybrid game between a good Demon, responsible for control actions, and a bad Angel, introducing perturbations. This formulation enables formal proofs of robustness w.r.t. a given (bounded) perturbation. Leveraging this bound, we employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution. We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.

ABSTRACT. The rise in popularity and deployment of deep neural networks has resulted in an increased demand for trustworthy models, particularly in safety-critical applications. As a result, several solvers that formally verify properties of neural networks have been developed. However, state of the art solvers have combinatorially large configuration spaces. The task of selecting the best configuration for an instance or benchmark is non-trivial. Furthermore, current methods for algorithm selection and algorithm configuration are insufficient for large configuration spaces. We present REGENT, an automated selection tool for verification of neural network (VNN) solver configurations via Large Language Model (LLM) prompting. Our zero-shot selection method is a three stage LLM inference tool that takes as input a feature description of a VNN instance and outputs a solver configuration. In case of failure, feedback from the solver is passed back to the LLM, after which a new configuration is queried. Our reinforcement learning with optimization feedback (RLOF) method fine-tunes LLMs to output configurations that cause VNN solvers to improve on an optimization objective. We perform extensive empirical evaluations that show that the configurations selected by REGENT achieve comparable performance to hand-tuned configurations on a large set of competition grade test instances. When applying our fine-tuning approach, we show that LLMs can configure solvers to prove tighter bounds than those proven using hand-tuned configurations on up to 58% of the most challenging test instances. REGENT allows non-expert users of VNN solvers to automatically generate significantly better configurations, and therefore can save several human hours involved in hyperparameter-tuning.

ABSTRACT. At ITP 2025, I introduced Canonical, a type inhabitation solver for dependent type theory, and an associated Lean tactic. But, how do you go about implementing such an algorithm? How does Canonical tame the combinatorial explosion, and why does it need a new representation of types and terms? How can Canonical be complete in the face of undecidable unification? To answer these questions, I developed Canonical-min, a simplified implementation of the core algorithm in 185 lines of Lean code. In this talk, I'll show that type inhabitation is easy if you look at it from the right perspective. What makes Canonical-min so special is its deep integration of Lean's monadic functional programming paradigm. The most important part of Canonical-min, the type checker, appears simple at a mere 18 lines. However, under the continuation monad, it becomes the core solver component which defines the search tree, enforcing all typing and unification constraints. I hope that Canonical-min (and this talk) can help foster understanding of general proof automation in dependent type theory, can help serve as the basis for the development and extension of the technique, and can one day lead to the formal verification of the algorithm. I am requesting 30 minutes for my talk.

ABSTRACT. Detailed and rigorous specifications of programming languages are highly valuable, since they facilitate precise reasoning about program behaviours and language properties. However, many mainstream languages remain unspecified, or are only specified in prose, which can be ambiguous and error-prone. We argue that this is partly due to a lack of good tooling for creating programming language specifications. Ideally, such tools should make the creation of specifications easier by automatically generating boilerplate and detecting inconsistencies, while also producing useful artifacts such as parsers, documentation, and proof assistant definitions. Though existing tools such as [Ott](https://github.com/ott-lang/ott) and [Lem](https://github.com/rems-project/lem) address some of these needs, they all have notable limitations. This talk introduces a new specification tool, currently in development, built using Lean’s metaprogramming features. Our tool enables users to define syntax through grammars and semantics via judgments, which are then automatically transformed into Lean inductive types and LaTeX figures for documentation. It also provides automated support for handling the complexities of variable binding. By leveraging Lean's metaprogramming capabilities, we achieve a high degree of integration that eliminates external dependencies and provides real-time error reporting by Lean's editor integration. Finally, we will discuss our roadmap for an enhanced version of the tool. A primary focus is extensibility, both in terms of the tool's architecture and the specifications themselves. By incorporating modularity principles from prior proof assistant research, we aim to allow users to extend and combine specifications, a crucial requirement for modeling modular architectures such as RISC-V and MLIR. (Preferred length: 30 minutes, though this isn't a strong preference.)

ABSTRACT. Nonlinear real arithmetic is a fundamental theory for modeling real world systems, but it currently has very limited support in proof assistants due to the intricacy of its decision procedures. Existing Lean tactics can handle some nonlinear goals, but even in simpler cases, such as with univariate goals, it is often the case that no existing tactic alone can currently solve. We present a new tactic that addresses this gap for the univariate case by leveraging the SMT solver cvc5 through lean-smt. Our approach is based on Cylindrical Algebraic Decomposition (CAD), a classical decision procedure for the theory of real closed fields. In the univariate case, this procedure splits the real line in the intervals separated by the roots of the polynomials from the input and tries to find a solution to the problem in each one of them. We instrumented cvc5 so that, when it solves a univariate nonlinear problem using CAD, it produces a certificate that can be independently verified. The tactic uses this certificate to build a proof term for the original goal. This process relies on two key components: first, a computable library for real algebraic numbers (RANs) with support for comparing the magnitude of two RANs and computing the sign of a polynomial evaluated at a RAN. This library was necessary since our tactic requires these operations on roots of polynomials on a real variable, which can be represented as RANs. Second, a formalization of Sturm's theorem, which provides a method to count the real roots of a polynomial in any given interval, ensuring that all roots have been found by the solver. Together, these components allow us to verify that the solver's decomposition of the real line is correct and that the original constraints are unsatisfiable in each resulting interval. Beyond its use as a Lean tactic, this work also serves as an independent proof checker for cvc5 in this logical fragment. By reconstructing solver certificates in Lean's type theory, we can verify the correctness of cvc5's results without trusting its codebase, which comprises hundreds of thousands of lines of code. Since our tactic is built on top of lean-smt, it benefits from the broader infrastructure that lean-smt provides for interacting with cvc5. Goals that combine nonlinear real arithmetic with other theories for which cvc5 has support for producing proofs — such as uninterpreted functions and datatypes — can also be discharged. We will also discuss directions for extending this work to the multivariate case, where Cylindrical Algebraic Decomposition operates by projecting polynomials onto lower dimensions and lifting solutions back. We outline the main challenges that arise in reconstructing proofs for this setting and possible strategies for addressing them.

ABSTRACT. We present a new iteration of Sulfur, a Rocq library and plugin to deal with substitution automatically for languages with binders. Compared with previous work, out tool supports the definition of various judgments such as typing, in a compositional way, and derives a substitution lemma for them.

ABSTRACT. This paper presents a formalization in Rocq of an extension of our category theory library with a category with computable pushouts and pullbacks. This library already contains several instances of categories with pullbacks and pushouts, but computation is not possible in any of them. We implement a category of finite ordinals and functions and detail how computation was made possible and (relatively) efficient.

ABSTRACT. Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and ω-automata manipulation. While Spot is routinely used as a research and verification back-end, its rich visualization capabilities and Python interface also make it an attractive platform for teaching the connections between temporal logic formulas and the ω-automata that give them their semantics. This demonstration showcases two complementary, zero-install entry points into Spot that are suitable for educational settings: 1. a web application that lets students type LTL or PSL formulas and immediately see the resulting automaton, explore formula simplifications, compare formula equivalence/implication, and navigate Manna & Pnueli’s temporal hierarchy. 2. Jupyter notebooks that combine narrative explanations, live Python code, and inline automaton drawings, enabling students to experiment interactively and instructors to build assignments around concrete, executable examples. Additionally, we can discuss the use of the command-line tools of Spot to generate random examples suitable for preparing a series of exercises.

ABSTRACT. Often, the easiest way to learn something is to have to use it for a purpose. This purpose can be playful: In *Tempus fugit*, the player takes on the role of a magician who has to defeat enemies by casting spells. The applicability of spells and enemy attacks depends on the truth of formulas in linear temporal logic with past with respect to a trace that the player gradually builds. So whoever wants to save the realm from monsters has to learn to read logic formulas. This paper describes the small browser game and explains our design choices. We expose how game mechanics connect to linear temporal logic with past over finite traces, and how this can help players approach a daunting topic like formal logic. (Submitted to both Plenary demo and Shared-time demo category.)

ABSTRACT. The Weisfeiler--Leman (WL) algorithm was originally introduced as a refinement procedure for analysing graph symmetries and as a tool for graph isomorphism testing. It distinguishes a large class of graphs up to isomorphism. For the k-dimensional WL algorithm, its indistinguishability power coincides with that of the finite-variable fragment of first-order logic with counting quantifiers, C_k. We study indistinguishability from an algebraic perspective. We introduce a program algebra with counting capabilities and a local version of k-WL, and show that both coincide in expressive power with the guarded fragment of counting logic, GC_k.

ABSTRACT. We compare the expressive power of state space models (SSMs) and recurrent neural networks (RNNs) in two domains: over words and over temporal graphs. Building on recent logical characterisations of SSMs via fragments of pure-past linear temporal logic (pLTLf), we lift the analysis to the graph domain. Our main results show that graph SSMs (GSSMs) are at least as expressive as the product logic pLTLf x K, combining pure-past LTL with graded modal logic over the neighbourhood, while recursive temporal graph neural networks (recTGNNs) capture the strictly stronger logic μTLf x K, a mu-calculus-style product logic. This mirrors the situation for words: SSMs recognise pLTLf-definable, i.e. star-free properties, whereas RNNs can simulate arbitrary finite automata and therefore recognise all regular properties. The structural parallel reveals a fundamental architectural boundary: the ability to compute fixpoints over sequences of arbitrary length lies beyond SSMs in both domains.

ABSTRACT. I will give a personally biased overview of projects in the space of interest for FLoC where proof assistants were used as more than proof checkers, covering amongst others results around Hilbert's tenth problem, the fifth busy beaver value, and computability. I will complement this by some general observations how to write up results of research projects involving proof assistants, trying to start an interactive discussion on how this differs to writing papers in general. I hope that the discussions scales to other tool use such as SAT or SMT solvers, and that the talk also sheds light on the question what makes a good research paper.

ABSTRACT. We develop polytopological semantics for various constructive, intuitionistic, and Gödel-Dummett variations of K4 and S4. In our models, intuitionistic and modal operators are interpreted via various topologies over a single set, equipped with either the closure or derivative operators. We identify regularity conditions to ensure that spaces validate each of our target logics and prove that all the logics considered are sound and strongly complete with respect to their respective semantics.

ABSTRACT. Recently, Ramesh has introduced new categorical concepts, introspective theories and geminal categories, which formalize "self-internalizing" structures sharing the form of Löb's theorem ($\square A \vdash A$ implies $\vdash A$). We reorganize the theory of geminal categories in a self-contained manner by introducing "code structures on fibrations," which serve as a categorical abstraction of Gödel coding. This approach leads to a generalization and a significant simplification of the proof of Löb's theorem for geminal categories, yielding a categorical counterpart of the Gödel–Löb axiom ($\square (\square A \to A) \to \square A$). This formulation offers an accessible framework for Ramesh's ideas. Moreover, we analyze the relationships between geminal categories and existing modal calculi such as Kavvos' DGL. While establishing the formal relationship requires further investigation, the strong resemblance between them suggests that there might be common categorical structures underlying metamathematics (the second incompleteness theorem) and metaprogramming (intensional recursion), unifying meta- and object-level interactions in logic and computer science.

ABSTRACT. We study the non-constructivity of checking the most common soundness condition for cyclic proofs over a constructive foundation. In light of our results, we argue that the constructively favourable formulation of proofhood restricts to periodic branches rather than arbitrary branches.

ABSTRACT. We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both events come with different modalities. In the logical semantics, formulas are interpreted in a world of an epistemic model (an S5 Kripke model) given a history of prior announcements and receptions. Consequently, agents' knowledge depends on two kinds of uncertainty: agents not only consider several possible worlds but they also reason over different histories of epistemic actions (of possibly different length). From this, two notions of validity arise. On the one hand, standard validities are formulas thtrue in every state of every epistemic model when no prior sending and receiving events have happened. Always-validities, on the other hand, are formulas that are true in every state of every model, after any prior history of such events. A reduction-based axiomatisation AA for standard validities has been proposed in a prior work. Here, we present an axiomatisation AA* for always-validities which is an infinitary system. Interestingly, the single-agent case requires an adaptation of our axiomatisation. We present the logic and the method to axiomatise always-validities, and explain why the method for multiple agents needs to be adapted for a single agent.

ABSTRACT. Privilege escalations are complex attack paths through which a user gains unintended access to a resource. The user chains together multiple operations—each one legitimate and authorized in isolation, such as creating new users; updating, attaching, or detaching policies; or assuming roles—until these assemble into a path that reaches a privilege they were never meant to have. At Huawei Cloud, we developed an SMT-based bounded model checking procedure that detects escalation paths of up to 5 steps, directly from a customer's account. Unsurprisingly, for large customers with thousands of deeply intertwined entities, the state space explodes as the search goes deeper. To make this scale, we applied sound state-space reductions. The soundness proof comes down to simulation, a well-known abstract technique I never expected to use at industrial scale. Thanks to this work, Huawei Cloud customers can now find 5-step privilege escalations in sub-second runtimes.

ABSTRACT. Machine learning classifiers work by being given a dataset of instances described by feature values and class labels, and then learning to predict the label of a new instance. Some methods do this in an interpretable way, producing simple if-then rules that a person can read directly. A learned rule set of this kind may say that one feature pattern usually predicts one label, except when a more specific pattern predicts the opposite. People naturally read such outputs as defaults and exceptions, but a readable rule set is not automatically a defeasible theory: it may look defeasible without any formal guarantee that its predictions correspond to principled nonmonotonic reasoning. We identify a single syntactic condition on learned conjunctive rule sets, called strict global exception closure, under which the classifier is provably a KLM defeasible theory whose predictions agree with defeasible entailment under Rational Closure, Lexicographic Closure, and System W simultaneously.

ABSTRACT. Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this demo we showcase a new learning environment as a layer above the Lean proof assistant, specifically targeting high-school level proofs. Drawing inspiration from other adaptations of proof assistants for teaching, such as Lean-Verbose and Coq Waterproof, along with our own experience using proof assistants in higher education, we designed Yalep --- Yet Another Learning Environment for Proof --- a declarative controlled natural language, with a minimal number of syntactic constructions, which favors forward-chaining of facts. [Note: we also applied for a "Shared-time demo" with the same extended abstract, with a preference for a "Plenary demo" over a "Shared-time demo" if possible]

ABSTRACT. Dual submission for Plenary and shared-time demo ----- Waterproof Editor provides an educational environment specifically targeted to teaching with proof assistants or programming languages. It arose from Waterproof, educational software targeted at helping students acquire the skill of giving mathematical proofs. Its original features such as enabling rich formatting and providing clear input areas are now abstracted away in an npm package and can be used in different educational contexts. We invite interested parties to use this component in their educational software, and offer to assist with this.

ABSTRACT. As neural networks (NNs) become a critical part of our everyday lives, their unpredictability and opaqueness make their logical analysis both a challenging and a crucial problem. In this tutorial, we will explore Marabou, a tool for formally verifying deep neural networks (DNNs). Formal verification aims to determine whether a DNN satisfies a given logical property, providing rigorous guarantees about its behavior. The first part of the tutorial presents the theoretical foundations of DNN verification and an overview of Marabou’s core algorithms. The second part focuses on the practical aspects of verification: defining verification queries, specifying properties of interest, and using Marabou to verify them through its various heuristics and solving modes. Finally, time permitting, we will explore the proof-producing version of Marabou, discuss the importance of proof generation for trustworthy verification, and demonstrate how Marabou’s proofs can be independently checked. Participants are encouraged to install Marabou before the tutorial (https://github.com/NeuralNetworkVerification/Marabou) and follow along.

ABSTRACT. The heterogeneity of proof outputs produced by different state-of-the-art automated theorem proving systems presents a considerable challenge for their efficient and uniform verification. In this paper, a proof checker called Nörgler is introduced that builds upon and extends the established approach pioneered by GDV. It supports checking propositional, (untyped and typed) first-order, and higher-order refutations represented in TSTP. For increasing flexibility and performance, Nörgler can parallelize proof checking tasks and incorporate model finders (for rejecting proofs). We evaluate the efficiency of Nörgler's design and implementation, and show that it outperforms GDV in terms of success rate and verification time on a benchmark drawn from the TSTP solution library.

ABSTRACT. We introduce GenZ, a generic theorem prover for sequent calculi implemented in Haskell. Sequent calculus is a simple and versatile formalism, widely used to define proof systems for modal and non-classical logics. GenZ allows the user to specify a set of sequent rules, over which it performs proof search. This makes it possible to rapidly implement and test proof systems for a wide variety of logics, a useful feature for both research and teaching. To allow for efficient proof search, GenZ employs the zipper data structure. We illustrate our system by implementing eleven well-known sequent calculi for classical and intuitionistic propositional logics, as well as for several modal logics from the S5 cube, and evaluate it on formulas from the LWB and ILTP benchmark suites.

ABSTRACT. The fuzzy logical system FP(\L) extends \L ukasiewicz logic by replacing propositional variables with basic modal formulas of the form $P\phi$, expressing the fuzzy notion that a classical event $\phi$ is probable. In this work, we study the satisfiability problem for FP(\L) by presenting an algorithm and conducting an empirical evaluation over a controlled class of FP(\L)-satisfiability instances. Our experimental results reveal a clear phase transition behaviour and distinctive running-time patterns, shedding light on the computational properties of FP(\L)-satisfiability.

ABSTRACT. Autonomous robotic systems are increasingly being developed for safety-critical environments, where ensuring safe operation is essential. Robots are typically implemented using modular software frameworks, each with its own distinct requirements and verification artefacts. We are interested in a bottom-up, compositional approach to their specification using Assume Guarantee (AG) contracts in which the specifications of the individual modules are used to compute a system-wide property. In this ongoing work, we extend an existing compositional framework by incorporating a more expressive temporal logic (MTL) as the foundation of the top-level specification language and developing a corresponding calculus for node composition. We demonstrate one of the rules for node composition using an illustrative example and discuss the planned future extensions to this framework.

ABSTRACT. Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guarantees for limited types of systems or test the system as a monolith, but no general framework exists for compositional analysis of learning-enabled CPS using varied verification techniques over complex real-world environments. This paper introduces a verification theory and framework that aims to fill this gap, enabling the construction of sound, formally-checked assurance cases for CPS. Our framework supports: (1) environment modeling using the Scenic probabilistic programming language; (2) compositional system modeling with clear component interfaces, ranging from interpretable code to black boxes; (3) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (4) evidence generation through testing, formal proofs in proof assistants, and external assumptions; (5) sound combination of generated evidence using contract operators; and (6) automatic generation of assurance cases tracking the provenance of system-level guarantees. We implement our framework in a tool, ScenicProver, using Pacti and Lean 4 as contract/proof backends. We demonstrate its effectiveness through a case study on an automatic emergency braking system with sensor fusion. By leveraging manufacturer guarantees for sensors and focusing testing effort on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.

ABSTRACT. LLM coding assistants now generate substantial bodies of systems code in C and Rust (kernels, compilers, drivers) that arrive without specifica- tions and with safety contracts encoded implicitly at call sites rather than enforced at function boundaries. We propose agentic model checking, a ver- ification paradigm coupling LLM agents with a bounded model checking backend under the principle agents propose, solvers verify. Agents handle every task requiring semantic judgment (specification inference, check se- lection, counterexample classification, refinement proposal); a BMC back- end (CBMC for C, Kani for Rust) discharges every soundness-relevant de- cision. Verification is compositional at function granularity under assume- guarantee contracts, and refinements propagate across the call graph. We instantiate the paradigm in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in both languages and on five OSS-Fuzz-hardened libraries.

ABSTRACT. Sound program analysis promises to catch every instance of particular kinds of bugs in a program. In practice, though, it has never been able to fulfill that promise in a practical way, and despite some limited success in the form of bug finding tools used at large companies, it has never become part of the standard toolkit used by programmers. In this talk, I will argue that AI is about to change that. On the one hand, Language Models enable new forms of sound program analysis that get around many of the limitations of traditional program analysis tools. On the other hand, they also make the use of program analysis essential as coding tools enable attackers to turn a vulnerability into an exploit with the push of a button. The contents of this talk will be based on the work in collaboration with my student Michael Wang.

ABSTRACT. Decidability of intuitionistic S4 has been an open question since the problem was formulated by Simpson (1994). We thought to have settled the issue: our LICS'23 claimed that IS4 was decidable, and provided a proof-theoretic algorithm to calculate the truth value of formulas. However, some six months after publication, Agi Kurucz designed a clever yet simple IS4 formula which could not be decided by our algorithm. In this talk, we set the record straight by discussing the main ideas behind our LICS '23 paper, explore Kurucz's counterexample, and discuss ongoing work on solutions to the problem of showing decidability of IS4.

ABSTRACT. We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (‘tense’ modalities). We propose axiomatic, proof theoretic and model theoretic definitions of ‘second-order intuitionistic tense logic’, and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case.

ABSTRACT. We would like to present our ongoing research work on the first (bounded) value iteration algorithm for the quantitative analysis of stochastic parity games. While existing algorithms are based on strategy iteration, our algorithms operate directly on values, exploiting a lattice-theoretic characterization of winning probabilities together with structural properties of almost-sure winning states under parity objectives. We prove correctness and convergence of the proposed methods and demonstrate their practical effectiveness through an experimental evaluation. We believe that our proposed constructions along with their practical relevance demonstrated through experiments will be of interest to the audience.

ABSTRACT. In this paper, we propose Probabilistic Loop Acceleration, a novel approach for analyzing quantitative properties of iterative structures in probabilistic programs. Conventionally, the weakest pre-expectation of programs with iterative structures is formulated as a least fixed point, and checking bounds of these fixed points poses significant computational challenges. By concisely summarizing nested probabilistic loops, our proposed method reduces the complexity of fixed-point reasoning, thereby enhancing the practical effectiveness of template-based automated verification. Technically, we extend Quantitative Fixpoint Logic (QFL) with an expectation operator to define QFL(E), which allows us to rewrite some fixed points in terms of expectation expressions. Furthermore, we integrate this with a template-based method extending MuVal^QFL. We present an automated procedure that resolves the verification obligations expressed in QFL(E) by reducing them to Polynomial Quantified Entailment (PQE) constraints. The infinite sums arising from expectation computations are handled by decomposing them into a finite number of terms and an infinite sum of regular terms aggregated into a closed-form term.

ABSTRACT. We propose new supermartingale-based certificates for verifying almost sure satisfaction of $\omega$-regular properties: (1) \emph{generalised Streett supermartingales} (GSSMs) and their lexicographic extension (LexGSSMs), (2) \emph{distribution-valued Streett supermartingales} (DVSSMs), and (3) \emph{progress-measure supermartingales} (PMSMs) and their lexicographic extension (LexPMSMs). GSSMs, LexGSSMs, and DVSSMs are derived from least-fixed point characterisations of positive recurrence and null recurrence of Markov chains with respect to given Streett conditions; and PMSMs and LexPMSMs are probabilistic extensions of parity progress measures. We study the hierarchy among these certificates and existing certificates, namely Streett supermartingales, by comparing the classes of problems that can be verified by each type of certificates. Notably, we show that our certificates are strictly more powerful than Streett supermartingales. We also prove completeness of GSSMs for positive recurrence and of DVSSMs for null recurrence: DVSSMs are, in theory, the most powerful certificates in the sense that for any Markov chain that almost surely satisfies a given $\omega$-regular property, there exists a DVSSM certifying it. We provide a sound and relatively complete algorithm for synthesising LexPMSMs, the second most powerful certificates in the hierarchy. We have implemented a prototype tool based on this algorithm, and our experiments show that our tool can successfully synthesise certificates for various examples including those that cannot be certified by existing supermartingales.

ABSTRACT. In this talk, we present the first dependency pair framework for analyzing expected complexity and for proving positive or strong almost-sure termination (SAST) of innermost rewriting with probabilistic term rewrite systems (PTRSs). We implemented our framework in the tool AProVE and demonstrate its power compared to existing techniques for proving SAST.

ABSTRACT. We show that there is a simple syntactically-defined subclass of higher-order benchmarks in the termination problem database for which rewriting according to Nipkow's higher-order rewrite systems (HRSs) and rewriting according to a beta-first strategy in the semantics of TermComp's higher-order category coincide. This lays the formal foundation for an HRS (sub)category in TermComp which would allow more tools to compete against each other.

ABSTRACT. We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Gödel's system T. For terms that can be typed in this system, we define the Global Trace Condition (GTC), adapting the concept from Brotherston and Simpson's Cyclic Proofs, and show that any infinite reduction of a well-typed term satisfying the GTC is strongly convergent. As a corollary, we obtain the proof that any closed term of type Nat reduces to some numeral through any reduction by levels. We argue that the Church-Rosser theorem holds in the limit for our calculus and that the normal forms of closed terms of type N (nat) are unique numerals.

ABSTRACT. Presentation of the results of termCOMP 2026

ABSTRACT. Competitions are usually evaluated in terms of stand-alone performance, i.e. how much better a submission performs than others determines the winner. This does not tell us how much a submission complements the state of the art -- is it able to solve something that nothing else can solve, even though that may be only a small part of the overall benchmark? In this talk, I will present the results of a Shapley Value analysis to FLoC competitions, which does evaluate the contribution to the overall state of the art.

ABSTRACT. Iterative heuristic optimisation algorithms probabilistically search for good or near-optimal solutions under a limited evaluation budget, typically measured by the number of objective function evaluations. They are often applied when little or nothing is assumed about the objective function, for example, when derivatives are unavailable, evaluations are expensive or the landscape is accessible only through black-box queries. Many established algorithms exist [2], but they are understood to different degrees: for some, the role of individual operators and parameters has been studied extensively, whereas for others, the mechanisms underlying observed empirical behaviour remain comparatively less thoroughly understood from a theoretical perspective despite demonstrated practical success. Furthermore, algorithm performance can depend strongly on the exact configuration of operators and parameter settings. This ties with the No Free Lunch theorem, which states that without assumptions about problem structure, no optimisation algorithm performs universally better than any other according to any reasonable performance measure. Consequently, there is no universally best algorithm, and performance must generally be assessed empirically on finite sets of functions and under finite evaluation budgets. An algorithm may be viewed as a well-defined sequence of logical operations designed to solve a particular problem. Modular algorithms [6, 19] make this perspective explicit by allowing individual operators to be specified independently, thereby creating a combinatorial design space of configurations within a single algorithm family. This design space can be further extended through an algorithm’s parameters, including integer, continuous and categorical parameters. Such frameworks make it possible to investigate which operators and parameterisations are responsible for observed behavioural or performance differences. In recent years, the field of heuristic optimisation has seen an unfortunate proliferation of supposedly “novel” metaheuristics inspired by natural phenomena, ranging from animal behaviour to physical processes². These algorithms have received substantial criticism for lacking genuine algorithmic novelty and relying heavily on metaphorical descriptions [17]. They are often developed in an unstructured manner, with limited evidence regarding parameter effects or the distinct contribution of newly introduced operators [13, 8, 18, 5, 11, 1, 4]. Harmony Search (HS) [9] represents one such example and is commonly described through a musical metaphor involving harmony memory, harmony memory consideration, pitch adjustment and random selection. Previous work [20, 21] demonstrated that HS is a simplified special case from a broader well-established class of algorithms known as Evolution Strategies (ES) [16, 14, 15]. However, this result is not constructive and does not identify the specific ES configuration reproduced by HS. Establishing such correspondence is nontrivial because the parameterisations of the two algorithms cannot be mapped directly onto one another. Therefore, understanding the relationship between HS and ES requires an empirical procedure capable of identifying ES configurations whose behaviour most closely matches that of HS under controlled benchmarking conditions. Therefore, using established benchmarking practices [3] together with automated algorithm configuration techniques [12, 6], we investigate how to identify ES configurations and parameterisations that approximate different aspects of HS behaviour across benchmark functions, dimensionalities and evaluation budgets. To enable this analysis, we introduce a novel Modular Evolution Strategies (modES) framework for specifying ES algorithms through configurable operators and parameterisations. Performance evaluation is conducted using IOHprofiler [7], and experiments are performed on the BBOB benchmarking suite [10]. This case study highlights the role of computational benchmarking as more than a tool for ranking optimisation algorithms. Benchmarking may also provide a systematic basis for studying behavioural equivalence, identifying algorithmic redundancy and evaluating claims of novelty. By grounding comparisons between HS and ES within a reproducible modular framework, this work aims to make questions of algorithmic novelty, redundancy and behavioural similarity experimentally testable.

ABSTRACT. In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIB format, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions. In this talk we will explore what SV-LIB is and how benchmarks for it can be easily generated from higher-level languages like C.

ABSTRACT. We verify the `extendedGCD` implementation in Go's standard library (`crypto/internal/fips140/bigmod`), which plays a crucial role in the generation of RSA key pairs. Even though the Go implementation is supposedly a direct port from BoringSSL's implementation, we uncovered two deviations that each break the algorithm's invariants: (1) the Go implementation deviates in the way coefficients are updated, and (2) it permits a larger input domain. We address both deviations; the first by fixing the Go implementation, which results in an on average 24% speedup, and the second deviation by porting an existing proof for BoringSSL and extending it to cover the larger input domain. We prove correctness and termination of the fixed Go implementation using Gobra, a deductive program verifier for Go. Where necessary, we used Lean to prove key lemmata on non-linear arithmetic, which we import into Gobra. Our verification effort reveals three key insights: subtle bugs can slip into even well-reviewed code with surprising ease; formal verification is a powerful tool for uncovering them; and AI agents can facilitate the verification process by iteratively refining invariants and lemmata based on Gobra's error messages.

ABSTRACT. The FS-FS hybrid signature scheme by Bindel and Hale (2023) combines two Fiat-Shamir components through a single shared challenge. Its EUF-CMA security is stated as a theorem in that work-in-progress, but no proof is provided. We report an EasyCrypt mechanisation of the FS-FS security argument in the Random Oracle Model (ROM), defined over abstract Fiat-Shamir components and instantiated with Schnorr, with ongoing work toward broader instantiations and the QROM. The formalisation yields two distinct insights. First, the second-preimage resistance assumption appearing in the original theorem statement is subsumed by the standard ROM guessing bound. Second, establishing the reduction in EasyCrypt requires two additional proof obligations: a logging invariant for the guessing branch and a tracker invariant for the collision-resistance reduction. Together, these obligations reveal proof-structural complexity introduced by the shared challenge that is absent from single-component Fiat-Shamir signatures.

ABSTRACT. The EasyCrypt proof assistant has been used to successfully formalize security proofs for a wide variety of cryptographic primitives. However, attempts at formalizing objects with interactivity, such as protocols, have fared much worse. In this paper, we investigate (some of) the reasons for this difficulty by formalizing a simple interactive key agreement protocol. From a first complete but exploratory proof, to a failed attempt at a structured proof, and to what we believe is an ``essential'' proof, we identify which proof features contribute most to the complexity of formalization in pRHL. In particular, we argue that difficulties in formalizing the security of interactive protocols in the computational model arise from the fact that such proofs rely on both state and temporal invariants---the former to support cryptographic reasoning, and the latter to support reasoning about the protocol's structure. We believe that this observation can help build new reasoning tools that can bridge the gap that currently exists between primitive-focused tools and protocol-focused tools.

ABSTRACT. Implementations of cryptographic primitives need to be both unquestionably secure and highly performant. The second requirement often leads library writers to craft hand-optimized assembly code, which significantly complicates the use of formal methods to satisfy the first requirement. We propose that decompilation techniques can be used to lift cryptographic code written in assembly to Jasmin, a language designed for high-assurance cryptography, and machine-checked for conformance against verified reference implementations, potentially offering comparable guarantees; and evaluate the viability of our approach with case studies drawn from mainstream cryptographic libraries.

ABSTRACT. Modern reachability analysis techniques are highly effective when applied to software safety verification. However, they still struggle with certain classes of problems, particularly the verification of programs with complex control flow and deep nested loops. In this talk, I will present Cycle Summarization-based Reachability Analysis (CSRA), a new Constrained Horn Clause (CHC)-based approach for reachability analysis of nested-loop software. Our technique relies on the generation and refinement of cycle summaries within the CHC system. CSRA analyzes cycles in a modular manner, constructing summaries and cycle unrollings. Cycle summaries in our approach are used both to prove safety and detect potential safety violations. This enables more efficient exploration of nested loops. The prototype of CSRA is implemented within the Golem CHC solver. An empirical comparison with other reachability analysis techniques demonstrates that our approach is highly competitive in both proving safety and constructing counterexamples.

ABSTRACT. Program safety verification with bit-precise semantics can naturally be encoded as Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors (T_B). Alternatively, bit-precise semantics can be encoded as CHCs modulo the theory of Integer Arithmetic (T_I) by modeling modular and bit-wise behavior using arithmetic constraints. However, neither approach consistently yields an efficient verification procedure: reasoning directly in T_B often limits the generalization capabilities of CHC solvers, whereas bit-precise T_I encodings produce complex arithmetic constraints that are expensive to process, especially in the presence of bit-wise operations. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo T_B through modular reasoning in T_B and T_I. Given a CHC set modulo T_B, Mosaic partitions the input into a bit-vector fragment and an integer fragment, and exchanges information between them through sound theory transformations. This avoids committing the entire CHC set to a single theory, allowing different CHCs to be handled in different background theories. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms both pure bit-vector and fully arithmetic CHC-solving approaches, often scaling to substantially larger bit-widths.

ABSTRACT. Data-centric AI, exemplified by the rapid advancement of deep learning and large language models, has fueled discussions of Artificial General Intelligence. However, for scientific discovery and high-stakes decision-making, purely data-driven methods face significant limitations. These include opaque behavior with limited interpretability, restricted use of prior knowledge, and brittle performance outside the training distribution. Furthermore, these models often struggle with heavy data requirements and complex multi-objective trade-offs. I discuss a knowledge-centric AI agenda designed to overcome these hurdles. This approach combines first-principles reasoning with data-driven learning, integrating prior scientific knowledge with data to produce interpretable and informed recommendations. I will discuss recent work in computational sustainability, highlighting how this framework facilitates discovery, prediction, and decision-making in high-stakes environments.

ABSTRACT. What do query processing, deep learning and quantum computing have in common? They can be formulated and generalized as dealing with linear operators over spaces such as free (semi)modules and Hilbert spaces, with associated classical algebras such as Boolean, associative and tensor algebras. The algebras have universal equational properties that can be exploited at run time by judicious simplification. Part of the trick is resisting the temptation to normalize data to a normal form, but employing symbolic operators that not only delay evaluation (as in lazy evaluation), but act differently depending on the context in which they occur at run time. The challenge then is when and how much to simplify, which data structures to use, and how to analyze the algorithmic consequences. We illustrate this methodology by applying it to * relational first-order logic based query evaluation, where we show that it is easy to program worst-case optimal joins on in-memory data that are secure against algorithmic complexity attacks, require few lines of code in Python or Haskell and perform quite well compared to even highly advanced and mature query compilers and database systems; * automatic differentiation (AD), where it leads to a DSL for compactly representing linear operators and computing their adjoints for reverse-mode AD. We will hint at other applications that we have developed in this fashion, from quantum circuit simulation to greenwashing-proof virtual energy sourcing. And we will encourage participants to think of more cases where this may be a (potentially revisionist) way of formulating their underlying methodology

ABSTRACT. Trustworthy AI in the legal domain can be achieved using reasoning-based expert systems. Furthermore, usability and performance of such systems can be improved by using generative AI and adding a human-verification step of generative AI's output-preserving trustworthiness. In addition, the common pitfall of automation bias can be avoided if verification becomes unavoidable and avoidance becomes equivalent to output refutation. We describe a system that demonstrates these claims in practice. By grounding its reasoning in a manually-created Datalog knowledge base with schematic natural-language translations, using an LLM to bridge the gap between natural language case descriptions and Datalog facts, and requiring each generated fact to be human-verified, the system achieves greater usability without compromising on trustworthiness.

ABSTRACT. Abstract: Human-AI Communication for Deontic Reasoning Devops (CODORD) intends to create new, automated techniques for humans to author knowledge about deontics (obligations, permissions, and prohibitions) into an expressively flexible logical language by using natural language (i.e., English). CODORD has the potential to enable automated deontic reasoning with high assurance (i.e., verifiability/explainability and correctness) to assess compliance with orders, regulations, laws, operational policies, and ethics.

ABSTRACT. Explainable artificial intelligence (XAI) is widely regarded as a mainstay of trustworthy AI. Recent years have witnessed massive efforts towards delivering reliable XAI solutions. Most of these efforts are based on non-symbolic methods of AI, and will invariably produce erroneous results. Thus, even if the predictions of a machine learning model could somehow be trusted, the lack of reliable explanations would render those predictions unworthy of trust. This talk provides a brief introduction to the field of logic-based XAI, a rigorous alternative to the still widely-used but highly problematic non-symbolic methods. The talk will also briefly dissect some of the more problematic shortcomings of non-symbolic XAI.

ABSTRACT. Satisfiability Modulo Theories (SMT) is used extensively across automated reasoning problems. Often, however, what we want is to answer quantitative queries, especially when reasoning over stochastic systems. In such cases we need to solve #SMT queries, and the precise counting question depends on the underlying theory. For bitvectors, it may be a simple or projected model count (1); for real arithmetic, it becomes volume computation (2). For hybrid discrete-continuous formulas, we may instead want a projected count over the discrete variables (3). In the presence of uninterpreted functions, we may ask how many interpretations of a function are possible (4). In this talk we discuss a line of work in which we design a tailored algorithm for each of these problems, and we present a series of tools that we are working to combine into a single framework, a #SMT toolbox, that handles all four under one umbrella.

ABSTRACT. Answer Set Programming (ASP) is a mature and widely used framework for modeling and solving problems in AI, knowledge representation and reasoning, and combinatorial search. Counting answer sets is of growing importance for analyzing search spaces, navigating ASP programs, and enabling probabilistic reasoning. While Truszczýnski established a complete hierarchy for the computational complexity of ASP decision and reasoning problems (skeptical and credulous), a corresponding systematic treatment of counting problems has been missing so far. We close this gap by providing an almost complete characterisation of the counting complexity landscape for ASP.

ABSTRACT. A lot of researchers struggle with finding their “next big idea,” and can get stuck waiting around until they see the whole path before starting anything new. In this talk, I’ll reflect on my own research journey (which started with automata theory and ended up spanning synthesis, networks, personalized education, and LLMs) and how many of the directions that shaped my work emerged not from following a fixed master plan, but from pursuing small ideas that gradually changed where I thought I was going. My goal is to share a perspective on how research directions actually develop in practice—and why consistently exploring and working through interesting questions often matters more than trying to predict the final destination from the start.

ABSTRACT. Microbial communities play a central role in many bioprocesses with key applications in food fermentation, waste treatment, human and animal well-being, plant protection or metabolite transformation in industrial bioprocesses. However, the metabolic microbial interactions driving the community dynamics remain difficult to characterize because of their complexity and their temporal variability. Recent advances in sequencing and analytical technologies now provide time-resolved multi-omics data at the community scale providing key insights into the mechanisms shaping the community dynamics. However, integrating these heterogeneous data in an interpretable way to decipher species-specific metabolic activity and microbial interactions remains a major challenge in the study of microbial communities. We introduce the community metabolic flux inference (comFI) method, a mathematical framework for inferring the metabolic fluxes of individual microorganisms from community-level longitudinal data. The method formulates flux estimation as a biology-informed constrained inference problem that combines observed microbial abundances and extracellular metabolite exchange data, with metabolic constraints encoded in a metabolic model and transcriptomic-based lasso regularization terms. We evaluated comFI on synthetic datasets generated from dynamic models of microbial communities involving three Escherichia coli mutant strains. The comFI method showed a very good reconstruction accuracy for exchange fluxes, intracellular metabolic fluxes distribution, metabolic pathway activation patterns and strain contribution. We also applied the method to experimental cheese fermentation data involving three bacteria (Lactococcus lactis, Lactobacillus plantarum, and Propionibacterium freudenreichii), combining abundance measurements, targeted metabolomics and metatranscriptomics data. The comFI framework enabled to recover previously identified interaction patterns, and to reconstruct latent intracellular flux states for individual microorganisms alongside with their respective metabolic contributions within the community, consistently with the omics data and known physiology. All together, we demonstrate that comFI provides a practical framework for recovering the metabolic activity of individual microorganisms from community-scale multi-omics time-resolved data.

ABSTRACT. Gene Regulatory Networks (GRNs) constitute a useful abstraction of complex molecular mechanisms responsible for cell behaviors, cell differentiation, and various diseases. Advances in high-throughput transcriptomics, such as single cell RNA sequencing data, have enabled unprecedented access to large-scale gene expression data. However, the manual reconstruction of GRNs from such data and literature is a hard task, and the automatic reconstruction by GRN inference algorithms remains a major challenge to analyze and validate. Previous work revealed that the performances of GRN inference algorithms vary significantly according to network topology, degree distribution and motif preponderance. The analysis of sensitivity to those properties requires the generation of synthetic GRNs of various forms, and expression data obtained by simulation. Since the seminal works of Barabási and Albert on the scale-free power-law distribution of connectivity degrees in GRNs, and of Alon and Milo on the particular distributions and significance of small network motifs, various random graph models have been developed to try to capture those particular features. In this paper, we show that a relaxed version of the directed configuration model (RDCM) does allow us to generate random GRNs fitting the graph properties and motif distributions of several large GRNs of the literature: Human-TRRUST, h-ESC,m-ESC,m-DC,and to a lessere xtent Yeast and E. coli, thanks to the variance of the results, and despite the discrepancies previously observed in terms of the mean in that random graph model. This is shown with GRNgen, a Python package which takes as input the number of nodes with for each node its in-degree and out-degree, the average path length, diameter, number of arcs and 7 important motif counts, and generates as output a set of random GRNs ranked by their fit to the input properties. We present our results for the generation of 1,000 samples for each of our reference GRNs, and provide elements of comparison with other generators.

ABSTRACT. Discovering reliable cause-and-effect relationships in real-world med- ical data is an open challenge. Classical Causal Discovery (CD) algorithms used to solve this task rely on strict assumptions that are rarely met in complex real- world scenarios with limited expert knowledge - the functional form of the causal relationships, the data distribution, the causal sufficiency. Thus, the reliability of CD algorithms can significantly drop, compromising the interpretability of the results and the trustworthiness of downstream decision-making. To overcome these limitations, we introduce the concept of consensus causal model to com- bine various CD algorithms and enhance their accuracy. Our consensus model can be efficiently constructed from a set of heterogeneous causal graph objects through a homogenisation step, ensuring semantic compatibility with the original edge definitions and enabling meaningful information exchange. To showcase the proposed method, we analyze a lung cancer dataset combining patient-level in- formation such as smoking habits and age, and we study their effect on the onset and development of the disease, the tumor stage, and cellular pathway mutations. By applying multiple classical CD algorithms, we observe significant structural inconsistencies and heterogeneity across individual graphs. We demonstrate that the consensus causal model, unlike the individual models, effectively aggregates the strengths of each algorithm while mitigating their uncertainties. The result- ing model reveals biologically validated causal relationships between risk factors, mutations, and pathways that isolated algorithms fail to capture, thereby under- scoring the value of consensus causal modelling as a robust alternative to single- model selection for causal discovery.

ABSTRACT. In this talk, we discuss a research program aimed at establishing systematic connections among the first-order correspondents of Sahlqvist/inductive formulas/inequalities across various relational semantic settings. We will focus on modal reduction principles, and the relational settings we will discuss include crisp and many-valued Kripke frames, and crisp and many-valued polarity-based frames (aka enriched formal contexts). Building on unified correspondence theory, we will discuss a theoretical environment which makes it possible to: (a) compare and inter-relate the various frame correspondents (in different relational settings) of any given Sahlqvist modal reduction principle; (b) recognize when first-order sentences in the frame-correspondence languages of different types of relational structures encode the same “modal content”; (c) meaningfully transfer and represent well known relational properties such as reflexivity, transitivity, symmetry, seriality, confluence, density, across different semantic contexts; (d) transfer notions and results such as the van Benthem theorem and the Goldblatt-Thomason theorem across different semantic contexts. These results can be understood as a first step in a research program aimed at making correspondence theory not just (methodologically) unified, but also (effectively) parametric.

ABSTRACT. In the present paper, we develop the correspondence theory for $\GBLe$, which can be viewed as the intuitionistic counterpart of {\L}ukasiewicz logic. Our methodology follows \cite{britz2025correspondencetheorymanyvaluedmodal}. We adopt algorithmic correspondence theory method, identify the class of inductive formulas, and develop an algorithm for computing the many-valued first-order correspondents of given inductive formulas. The key step is to find the interpretations of nominals and conominals (whose interpretations are the counterparts of singletons and their complements) in $\GBLe$ which can be translated into many-valued predicate logic.

ABSTRACT. The Global Trajectory Optimization Competition (GTOC) is an international challenge in space mission design that formulates realistic, large-scale optimization problems and evaluates solutions through transparent mathematical scoring rules. This talk presents the structure and philosophy of GTOC using the 12th edition (GTOC12) as a case study. GTOC12 focused on asteroid mining, with the objective of maximizing the total mass of resources returned to Earth. Participants were required to design trajectories for multiple spacecraft performing asteroid rendezvous, resource extraction, and return missions under low-thrust propulsion constraints. The problem combined continuous optimal control with discrete combinatorial decision-making, including spacecraft allocation, target selection, sequencing, and timing. GTOC12 illustrates how future mission design integrates astrodynamics, optimization, and systems-level planning.

ABSTRACT. Space logistics and mission planning are becoming increasingly critical as humankind expands its presence in space. While simulation and analysis tools such as SpaceNet have been widely used to explore feasible architectures, their limited optimization capabilities make it difficult to fully avoid the cost of extensive trade space exploration. This paper presents a new open-source optimization toolbox for space mission planning, developed to automatically formulate and solve or find feasible solutions to mixed-integer nonlinear programs (MINLPs) that integrate discreteness of mission profiles and nonlinearity of systems design. The toolbox is designed for accessibility: users specify mission requirements and parameters, after which the corresponding optimization problem is generated and addressed by a solution approach of the user's choice, including state-of-the-art solvers and built-in heuristic algorithms. Current capabilities include integrated space mission planning and spacecraft design, support for both commercial and open-source mixed-integer solver options, and initial visualization of optimized network flows. The planned extensions focus on interactive visualization, expanded mission domains beyond the Earth–Moon system, and surface logistics integration. This rigorous yet accessible optimization toolbox aims to enable more efficient and optimal mission design processes to support future space exploration.

ABSTRACT. There are a number of types of space mission concepts that feature a single spacecraft visiting multiple targets through its mission. Such “tour” missions are commonly modelled as travelling-salesman problems (TSPs). However, the typical TSP modelling methods are complicated by the fact that the “customers” – the satellites that require servicing, for example – are in orbit, rather than stationary. Previous works resolve this issue either by representing entire orbits as single nodes in the salesman’s – for example, the servicer satellite’s - route, or by expanding orbits into multiple discrete time steps. Both of these methods therefore lose some fidelity in the time dimension, and consequently must make worst-case assumptions about the time-dependent cost of moving between nodes in order to maintain the feasibility of solutions. These worst-case assumptions can be inherently avoided by maintaining the time dimension of the problem as a continuous quantity, as opposed to constructing discrete time windows. Therefore, this paper constructs the Keplerian travelling salesman problem as a time-dependent travelling salesman problem and implements a dynamic programming approach to finding orbital tour schedules with exact, continuous time solutions. We present preliminary results and make comparisons with a state-of-the-art integer programming method.

ABSTRACT. Target selection for large-scale space survey missions requires selecting a scientifically valuable subset from a much larger pool of available targets. This represents a high-stakes combinatorial optimisation problem, since the final sample directly shapes the scientific return of the mission. Current operational approaches mainly rely on heuristic stratified sampling over low-dimensional parameter subspaces. While this paradigm captures key quantities of interest to astronomers, it becomes increasingly limited as the dimensionality and complexity of the planetary feature space grow. More importantly, there is currently no formal evaluation framework for comparing target-selection strategies against scientifically grounded criteria, leaving mission planners without principled tools for assessing representativeness or survey leverage. This problem is particularly relevant for ESA's Ariel mission, which aims to observe approximately 1,000 exoplanets selected from a much larger Mission Candidate Sample (MCS). Ariel will therefore be used in this work as a case study for developing and evaluating target-selection strategies. We propose a multi-objective subset selection framework that formalises target selection as the simultaneous optimisation of three core objectives: distributional similarity to the full candidate catalogue, quantified via the Wasserstein distance; internal subset diversity, maximised over the planetary feature space; and scheduling practicality, subject to mission lifetime and transit window constraints. A key contribution is the evaluation protocol itself, a fair, metric-grounded benchmarking arena for comparing arbitrary selection strategies, which the community currently lacks.

ABSTRACT. We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., internally-controlled) variables. Our framework is a semantic generalization of Cousot and Cousot’s abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné’s decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. The talk concludes with open challenges in dealing with angelic non-determinism, pointer-manipulating programs, and going beyond termination to program properties expressed in Computational Tree Logic (CTL) or Alternating-Time Temporal Logic (ATL).

ABSTRACT. Algebraic effects are a way to describe and reason about computational effects in a modular way, via the algebraic theories from universal algebra. A current challenge is to extend these ideas to concurrent programming. In this talk, I will present recent work on modelling dynamic thread creation, inspired by POSIX fork, using an algebraic theory. The main result characterizes this algebraic theory in terms of labelled partial orders, leading to a semantics where concurrent programs denote partial orders. The algebraic theory provides sound and complete equational reasoning principles for equality of such partial orders. This is joint work with Ohad Kammar, Jack Liell-Cock, Sam Lindley, and Sam Staton.

ABSTRACT. The Mathlib Initiative launched in September 2025. Our mission is to support the growth and maintenance Lean's Mathlib library, as well as the broader ecosystem and community. I will explain how the Mathlib Initiative came to be and how we are working to achieve these goals.

ABSTRACT. We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice. This paper was originally presented at POPL 2026.

ABSTRACT. The Rocq-prover is a functional programming language and logical system based on fixpoints and pattern-matching. To be consistent, Rocq only accepts functions that terminate. This is enforced by a syntactic check named the “guard con- dition”, that ensures that every recursive call is performed on a smaller term than the original one. Despite its critical role, the guard condition is little understood: there is no mathematical justification for it, nor formal specification of it. Moreover, its implementation consist in about 2000 lines of intricate OCaml code, that even experts struggle to under- stand. This lack of understanding has led to inconsistency bugs due to both implementation and theoretical issues, and prevents any further modifications. With this work, we provide the first formal specification of the guard condition as it should be implemented. We fur- ther build knowledge on guard conditions by introducing its different features one by one, and discussing their motiva- tions, limitations and related historical bugs. Based on this specification, we provide a reimplementation of the guard condition in MetaRocq.

ABSTRACT. We present Camltac, a Rocq plugin that allows OCaml to be written directly within Rocq scripts. Camltac blurs the line between Rocq plugins and tactics, letting users leverage the expressivity, performance, and rich ecosystem of OCaml to write tactics and meta-programs, without compromising on simplicity and convenience.

ABSTRACT. Formal languages with term-forming operators (tfos) are very useful in several fields. However, a syntactical analysis of such devices requires significant changes in the toolkit of proof theory. In this paper we discuss the problems connected with construction of cut-free sequent calculi for languages with tfos. As a case study we are analysing Quine’s Virtual Theory of Classes (VTC), a neutral basis for proof theoretic development of theories of sets like ZFC or NBG, based on the application of set abstracts.

ABSTRACT. Cut elimination procedures for deep inference calculi such as BV and its extensions have traditionally required intricate reasoning about rewriting proofs into normal form. I will present another way, based on ideas from the rewriting-free Normalisation by Evaluation (NbE) technique for lambda-calculi. NbE works by constructing a model from the syntax of normal (or cut free) proofs and evaluating proofs containing cut into that model. A reification procedure then reads out the normalised (cut free) proof from the interpretation. I will show that this technique works for BV and its extensions with additives and exponential. This is joint work with Wen Kokke.

ABSTRACT. Drinfeld modules are a central object of study in the arithmetic of function fields. In this talk, I will present an ongoing project, joint with María Inés de Frutos Fernández, to formalize Drinfeld modules in Lean. In order to formalize the general definition of Drinfeld modules, we first needed to formalize a substantial amount of missing number-theoretic prerequisites. In this presentation, I will discuss the formalization hurdles encountered along the way, how they were solved, and the API design decisions required to build this foundational mathematics. Specific technical highlights of this work include: * The definition and development of `SkewMonoidAlgebra` and `SkewPolynomial`. * Formalizing fundamental results about function fields, including Ostrowski's theorem for $K(t)$. Beyond the specific case of Drinfeld modules, I will highlight how this project has served as a broader driver for library development, resulting in over 50 merged pull requests to `mathlib` to date. I will share insights from this journey that are applicable to anyone structuring large mathematical formalizations and developing comprehensive APIs in Lean 4.

ABSTRACT. We present a Lean library that uses effective transversality for certified root finding in multivariate polynomial systems. We formalize dyadic intervals, interval arithmetic, and a Newton-like method called the Krawczyk method, establishing their key correctness properties. Building on this foundation, we implement a recursive branch-and-bound algorithm that subdivides an initial interval vector to either isolate regions containing unique roots or certify the absence of roots. Finally, we introduce custom syntax and a tactic that automatically searches for suitable parameters to certify the existence, uniqueness, or non-existence of roots. (Short talk)

ABSTRACT. Meta-programming is the art of writing programs that produce or manipulate other programs. This allows programmers to automate error-prone or repetitive tasks, and exploit domain-specific knowledge to customize the generated code. Unfortunately, writing safe meta-programs remains very challenging and sometimes frustrating, as traditionally errors in the generated code are only detected when running it, but not at the time when code is generated. Moreover, while there is ad-hoc support for meta-programming in type theories, there is no proper foundation for it. This talk revisits Cocon, a framework for certified meta-programming. Cocon, a Martin-Loef dependent type theory for defining logics and proofs that allows us to represent domain-specific languages (DSL) within the logical framework LF and in addition write recursive programs and proofs about those DSLs. In particular, we can embed into LF STLC or System F, etc. and then write programs about those encodings using Cocon itself. This means Cocon is a target for compiling meta-programming systems -- from compiling meta-programming with STLC or System F to compiling meta-programming in CoC. We then motivate the design of DeLAM, a dependent type theory that support meta-programming by distinguishing between the code that is being generated, the type of that code, and the program that is actually generating the code. I will also highlight more recent research directions that aim to support meta-programming and intensional code analysis.

ABSTRACT. Identifying implicitly defined variables in a propositional formula and extracting their explicit definitions is useful for Boolean functional synthesis and related problems. This typically involves one SAT call per variable and constructing an interpolant from the resulting resolution proof. We propose extracting an entire set of n definitions from a single resolution refutation. A modification of a standard interpolation system computes interpolants under partial assignments, one per target variable. A single pass of the refutation then produces a multi-output circuit of size O(nm) for a proof of length m. Preliminary experiments on Boolean functional synthesis benchmarks show that the joint refutation is produced at least as fast as the per-variable sequence of proofs, but the multi-output circuits are typically larger. Closing this circuit-size gap is the main open question.

ABSTRACT. Boolean Functional Synthesis (BFnS) is the problem of synthesizing a Boolean function from a Boolean specification that describes a relation between input and output variables. Due to the many applications of BFnS, such as in circuit design, QBF solving, and reactive synthesis, efforts are continuously made to explore and better study BFnS. In this work we deepen our understanding of BFnS by analyzing underlying graph structures of BFnS instances. This is motivated by a chain of works on SAT instances, where analysis of graph features, such as graph modularity, is used to explore the performance of SAT solvers on industrial SAT instances. We first show that unlike instances that are random, industrial BFnS instances admit high modularity, even more than is common in SAT. Observing that, we construct a novel BFnS random instance generator with controlled modularity, which we use to study the effect of modularity on performance of state-of-the-art BFnS solvers. Finally we white-box these solvers to determine how the structure of generated instances changes iteratively through the solving process. Our findings indicate that instances modularity has a direct effect on the various solvers performance and their behavior.

ABSTRACT. Quantum circuit synthesis is the task of decomposing a given quantum operator into a sequence of elementary quantum gates. Since the finite target gate set cannot exactly implement any given operator, approximation is often necessary. Model counting, or #SAT, has recently been demonstrated as a promising new approach for tackling core problems in quantum circuit analysis. In this work, we show for the first time that the universal quantum circuit synthesis problem can be reduced to maximum model counting. We formulate a #SAT encoding for exact and approximate depth-optimal quantum circuit synthesis into the Clifford+T gate set. We evaluate our method with an open-source implementation that uses the maximum model counter d4Max as a backend. For this purpose, we extended d4Max with support for complex and negative weights to represent amplitudes. Experimental results show that existing classical tools have potential for the quantum circuit synthesis problem. https://arxiv.org/pdf/2508.00416

ABSTRACT. Neural networks are susceptible to adversarial examples---inputs with subtle perturbations that trigger erroneous outputs and potentially catastrophic failures. Neural network verification addresses this by formally checking whether given postconditions are entailed by specific preconditions. Most state-of-the-art verifiers rely on abstract interpretation to overapproximate neuron bounds layer by layer, utilizing branch-and-bound methods to achieve completeness. However, a significant gap exists between theoretical soundness and practical implementation: standard floating-point arithmetic introduces rounding errors that accumulate during computation, potentially leading to unsound verification results. While the continuous constraint solving community has long addressed numerical inaccuracies by accounting for floating-point rounding errors, this rigorous treatment is not yet widespread in neural network verification. Our preliminary experimental results demonstrate that unsoundness issues manifest in several state-of-the-art neural network verifiers. To bridge this gap, we propose JET, a GPU-based sound continuous constraint solver. JET integrates sound floating-point interval arithmetic with constraint propagation and a search method, providing a framework that guarantees numerical soundness while leveraging the parallel performance on GPU.

ABSTRACT. We present IsaGrad, a formalisation of reverse automatic differentiation (RAD) over mutable computational graphs using the Imperative HOL library of Isabelle, and verify its functional correctness using separation logic. We use IsaGrad as the differentiation engine for two machine learning case studies: training a multi-layer perceptron and a recurrent neural network. Leveraging Isabelle's code generation, we extract imperative-style Haskell programs where the training process is backed by our verified algorithm. To our knowledge, our implementation is the first of its kind to prove the functional correctness of an imperative, heap-based RAD algorithm. Beyond showcasing Imperative HOL’s expressiveness, this work demonstrates how formal verification increases confidence in computational graphs used for gradient-based optimisation, including neural network training.

ABSTRACT. We investigate the proof-theoretic structure of incorrect/incomplete proofs, that is, derivations containing syntactic errors or incomplete inferential steps that nonetheless preserve partial semantic validity. Building on Hilbert’s epsilon calculus, we formalize how such derivations can be corrected through semantic projection and weakest preconditions, leading to valid Herbrand disjunctions. We show that the epsilon calculus provides a natural framework for analyzing tolerance of falsity in proofs and for identifying conditions under which an incorrect proof can be semantically repaired. This approach extends Hilbert’s program beyond correctness, toward a logic of error and recovery. Moreover we show that the extended first epsilon theorem is false-tolerant.

ABSTRACT. The classical natural deduction system $\mathbf{NK}$ can be obtained from the intuitionistic system $\mathbf{NJ}$ by adding a double negation elimination inference rule ($DNE$). On the other hand, the intuitionistic and classical sequent calculi $\mathbf{LJ}$ and $\mathbf{LK}$ are differentiated by the number of formulae that can be contained in the right-hand side of a sequent. In an $\mathbf{LJ}$-derivation, the right-hand side of a sequent can contain at most one formula; $\mathbf{LK}$ is obtained by lifting this restriction, giving it the property of right multiplicity. This distinction between $\mathbf{LJ}$ and $\mathbf{LK}$ is notably different from the distinction between $\mathbf{NJ}$ and $\mathbf{NK}$: the first is purely structural, and the second involves the explicit addition of a classical inference pattern. We demonstrate how the same classical strength, in terms of what can be derived, emerges from $DNE$ and right multiplicity in $\mathbf{NK}$ and $\mathbf{LK}$, respectively. In particular, we show that the classical strength of $\mathbf{LK}$ arises from right multiplicity through its interactions with the negation and implication rules in a way that is formally analogous to how $DNE$ interacts with the equivalent rules in $\mathbf{NK}$.

ABSTRACT. The notion of proof is central to both mathematical logic and computer-assisted reasoning, traditionally understood as a sequence of locally verifiable inference steps. While this formal view enables automation and verification, it often obscures the structural insights underlying mathematical arguments. Proof analysis aims to recover this structure, with cut-elimination and Herbrand’s theorem playing a key role in extracting computational content from proofs. However, these classical tools face limitations in the presence of induction, where proofs implicitly represent infinite reasoning. To address this, proof schemata provide finite representations of infinite families of proofs, enabling schematic cut-elimination methods such as CERES and the extraction of Herbrand systems. In parallel, cyclic proofs offer an alternative framework for inductive reasoning using globally justified cycles instead of explicit induction rules. This work investigates the relationship between these two formalisms. We present a translation from a restricted class of cyclic proofs in the system CLKID^omega into proof schemata, enabling the direct application of schematic analysis techniques. Under suitable restrictions on quantification and inductive definitions, this translation facilitates the extraction of Herbrand systems from cyclic proofs. The approach is illustrated using the 2-Hydra example, demonstrating that proof schemata can capture inductive arguments beyond Peano Arithmetic. At the same time, we show that proof schemata and Peano Arithmetic are incomparable in expressive power.

ABSTRACT. While neural networks are the cornerstone of modern machine learning, our understanding of the computational complexity of training them remains far from complete. To address this gap, in this talk we will survey recent advancements in both the classical and parameterized complexity of Neural Network Training (NNT). Specifically, we will examine the computational task of finding a set of weights and biases that optimally matches given training data within a specified network architecture. Beyond classical models, the talk will also highlight recent NNT developments for graph neural networks and quantized neural networks.

ABSTRACT. Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of $\omega$-regular properties (and therefore linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for $\omega$-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an $\omega$-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.

ABSTRACT. Neural networks (NN) are often represented using the Open Neural Network Exchange (ONNX) format that provides a rich set of operators. This richness implies that many tools support only a subset of ONNX operators and, consequently, a subset of NNs. However, some of these operators can be expressed equivalently as combinations of simpler, already supported, operators. In this work, we present an extension of CAISAR---a platform for verification of NN that uses external solvers---that automatically transforms these redundant operators into simpler ones before calling existing solvers, thus extending the range of these solvers. This work focuses on the argmax operator, proposing a transformation, proving its correctness, and presenting experimental results.

ABSTRACT. Safety analysis of neural-network controllers for cyber-physical systems requires combining closed-loop dynamical reasoning with formal neural-network verification. Standard invariant-based workflows typically compute the maximal controlled-invariant set before controller checking, although a violating execution may be detectable for an invariant inner-approximation. This paper proposes an incremental workflow for checking controller safe-set preservation. Starting from an initial inner-approximation, the method interleaves invariant refinement with verification, reuses proof results, checks only the newly added region between successive iterates, and supports early termination with a counterexample. If no violation is found, the verified domain grows progressively with each refinement step. Case studies on adaptive-cruise and lane-keeping neural controllers show that interleaving reduces time to counterexample in unsafe cases, lowers runtime in safe cases, and proof reuse becomes more beneficial as verification cost increases.

ABSTRACT. Markov Decision Processes (MDPs) are a powerful modeling paradigm for sequential decision-making problems, e.g., robot navigation and game playing. Decades of research have produced highly efficient algorithms for solving MDPs. A common limitation, however, is that the solutions (policies) are typically represented as large lookup tables that map agents' actions to thousands or even millions of states. In this work, we present a fast approach to optimizing (fixed-size) decision tree policies for MDPs, which are easier for human experts to analyze and for specialized tools to verify. Previous work tackled this problem using computationally intensive techniques, such as integer programming or abstraction refinement. While our method, Lipa, which combines branch-and-bound with smart heuristics, can often find high-quality policies orders of magnitude faster and prove optimality where previous methods fail. We evaluate Lipa on 21 discounted-return and model-checking benchmark MDPs of varying sizes and demonstrate consistent, significant improvement over the state of the art.

ABSTRACT. Counterfactual explanations (CEs) provide a simple, yet powerful interpretive approach to understanding neural network behavior, envisioning hypothetical scenarios by systematically altering input features and analyzing the resulting changes in model predictions. However, CEs are useful only if they are robust, i.e., they remain consistent and meaningful even when adversarially perturbed. While prior work has explored the development of generators for robust CEs, checking the robustness of CEs produced for DNNs has not been explored within the verification context, nor has it been studied under adversarial training. We present a systematic study utilizing adversarial training to fortify the underlying neural network, observing its effect on the formal robustness of DNNs with respect to CEs using α, β-CROWN, a state-of-the-art NNV. Our experiments across multiple datasets, network architectures, and CE generators indicate that adversarial training has a positive impact on the number of formally verified robust CEs. We also measure the impact of adversarial training on other desirable properties of CEs, such as plausibility and proximity. While plausibility does not change, there is a trade-off with proximity when using a gradient-based CE generator.

ABSTRACT. The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000 students worldwide over the last decade. We cover the good, the bad, and the ugly: what worked well, what didn't work, and what added friction to development and maintenance over time. These insights motivate a bottom-up redesign of the Carnap framework, which is the topic of the paper's second part. Briefly, the new design combines a new high-performance verifier kernel (mm0-zig) targeting Mario Carneiro's metamath zero format, and the Aufbau Bytecode Compiler, (abc), a new proof compiler that can serve as a backend for richly interactive proof-authoring experiences on the web.

ABSTRACT. Introductory courses in the formal foundations of computer science are often attended by large numbers of students from diverse backgrounds. In this talk, we will outline how this challenge can be addressed using web-based, interactive exercises provided by Iltis (https://iltis.rub.de/), a modern educational support system covering the foundations of logic, formal languages, and (parts of) complexity theory. We will give a brief introduction to Iltis and outline the research challenges and opportunities for theoretical computer science that arise in the development of such a system. This talk is based on an article that appeared in the Educational Column of the EATCS Bulletin and previous talks on the subject. We attached the article and previous slides.

ABSTRACT. The LTL Tutor is a misconception-based tutor that improves understanding of LTL. It integrates knowledge of and tooling for LTL, several years of user-studies, and concepts from education research into a seamless package.

ABSTRACT. First-Order Logic (FOL) theorem provers excel at symbolic reasoning but may struggle at tasks requiring complex integer arithmetic combined with irregular conditional rules. This limitation is most acute in temporal reasoning, where standard ontologies model time relationally rather than arithmetically. We present a novel “Universal System” that bridges this gap through a complete axiomatization of Gregorian calendar arithmetic implemented in the TPTP language. Our modular architecture comprises four interlocking engines: a Time Engine for minute-level rollovers, a Date Engine for Gregorian leap-year logic, a Scheduler Engine utilizing Zeller’s Congruence for weekday calculations, and a novel Integer Trap mechanism that forces arithmetic evaluation within the theorem prover. We demonstrate that this formalization enables the Vampire theorem prover to solve complex scheduling queries–such as finding “the 2nd Thursday of November 2025”–entirely within First-Order Logic, without recourse to external computational modules. Our evaluation on a comprehensive suite of 220 diverse temporal reasoning problems shows 100% accuracy, verified against Python’s datetime library for ±10,000 days (27.4 years)—the extent of Python’s BCE date support. The system demonstrates empirically O(1) constant-time performance (bounded by ≤ 30 major accelerator jumps) with coefficients of variation under 2% across six orders of magnitude, executing queries spanning ±1,000,000 days (2,738 years) in 456–473ms with identical performance characteristics. This includes leap year edge cases, complex scheduling constraints, and calculations extending from 714 BCE to 4762 CE

ABSTRACT. We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multiple LLM-based coding agents. Rather than relying on static central planning, we implement a simulated bounty-based marketplace in which agents dynamically propose new lemmas (formal statements), attach bounties to them, and compete to discharge these proof obligations and claim the bounties. The agents interact directly with the interactive proof system: they can invoke tactics, inspect proof states and goals, analyze tactic successes and failures, and iteratively refine their proof scripts. In addition to constructing proofs, agents may introduce new formal definitions and intermediate lemmas to structure the development. All accepted proofs are ultimately checked and verified by the underlying proof assistant. This setting explores collaborative, decentralized proof search and theory building, and the use of market-inspired mechanisms to scale autoformalization in ITP.

ABSTRACT. Large language models have recently enabled autoformalization, directly translating informal mathematical arguments into machine-checkable proofs. However, the resulting autoformalized proofs tend to be too low-level, cluttered, and opaque, making them hard to understand and maintain. We present an approach to understandable autoformalization that targets a controlled sublanguage of mathematical English that the experimental proof assistant Felix can parse and whose meaning it can verify. Starting from informal textbook LaTeX, our tools produce controlled natural language texts whose statements resemble conventional mathematical writing while being mechanically verifiable. To keep the formal development high-level, we combine the controlled language with automated theorem provers to discharge ``human-sized'' proof steps. This shifts routine reasoning to automation while preserving a readable proof structure. The resulting formalizations are intended to be understandable as mathematical texts, even for readers unfamiliar with Felix, and to serve as a bridge between informal exposition and machine-checked mathematics. As a case study, we present our autoformalization of Munkres's Topology, which is the most comprehensive formalization in a Naproche-like proof assistant yet in terms of total lines of code, and a demonstration that natural theorem proving can scale beyond chapter-sized formalizations.

ABSTRACT. Exploring cyber-physical system (CPS) architectures that satisfy a set of heterogeneous requirements while minimizing a cost metric is computationally challenging, due to the exponential growth of the design space with the number of architecture parameters and to the interdependencies between architectural choices and system properties. We present architecture exploration methodologies that leverage assumeguarantee (A/G) contracts for decomposition at every stage of the exploration pipeline: specification (via viewpoint and satisfiability modulo convex programming (SMC) contracts), synthesis (via mixed integer linear programming (MILP) or binary integer programming (BIP)), verification (via refinement and convex programming (CP) checks), and pruning (via subgraph isomorphism and certificates from irreducible infeasible sets (IISs) and counterexamples). Experiments on a reconfigurable production line and an aircraft electrical power distribution network show one to two orders of magnitude acceleration over comparable approaches, enabling tractable design on instances where prior methods time out.

ABSTRACT. Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. In this talk, we present Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their proof calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using different program logics. Combined theories allow program combination via regular programs, which yields heterogeneous control structures that allow us to reason about intertwined cross-language behavior.

ABSTRACT. This extended abstract summarizes recent results towards a computable and compositional semantics for hybrid systems.

ABSTRACT. Concurrency entails nondeterminism and interference: a program can have more than one possible run and the executions of different processes may conflict in unpredictable ways. A modular contract-based approach is essential for deductive verification to be manageable. However, specifying contracts for concurrent programs poses many challenges. Our approach to address these challenges for single-threaded cooperative scheduling is the following: 1) we specify concurrent behaviors with "context-aware trace contracts" (CATs for short) which allow the specification of internal non-functional behaviors of a procedure as well as the context of its execution; 2) we define a specification abstraction paradigm to reduce the specification effort and specify a single contract (Big CAT) for each procedure, rather than specifying each possible relevant scheduling choice; 3) we restrict program execution to "linear concurrency", i.e. concurrency without interleaving of tasks, to achieve modular verification at the granularity of procedure. We designed a sound deductive system to verify (Big) CATs for concurrent programs. We proved that program correctness entails the absence of interleaving and deadlock-freedom.

ABSTRACT. Complex engineered systems span hardware, software, control, planning, and operations. Their difficulty lies in coupling: a sensor changes the feasible estimator, a battery changes the feasible mission, and a planner changes which robot architecture is worth building. This presentation proposes monotone co-design as a formal, compositional language for these trade-offs. Starting from the classical functionality--resource interface, we explain how local feasibility relations compose, how Pareto queries avoid full Cartesian-product enumeration, how linear design problems yield scalable exact algorithms, and how distributional uncertainty and online learning extend the framework to risky, adaptive, and black-box subsystems. We close with applications in robotics, mobility, and heterogeneous multi-agent systems.

ABSTRACT. Neural networks are a fundamental aspect of modern artificial intelligence, playing a key role in various important machine learning architectures including transformers and graph neural networks. Recently, logical characterisations have been used to study the expressive power of many machine learning architectures, but logical characterisations of plain neural networks have received less attention. In this paper, we provide fuzzy logic characterisations of rational-weight ReLU-activated neural networks via two well-established fuzzy logics: Rational Pavelka Logic RPL (and extensions thereof) and (fragments of) LΠ½. The activation values of the neural networks are allowed to be arbitrary real numbers. We also provide fuzzy logic characterisations of a generalised polynomial ring over ℚ in countably many variables where the use of the ReLU-function is permitted.

ABSTRACT. This paper presents an overview of a line of research on representing neural networks in Łukasiewicz logic and applying this representation to formal property verification. The approach relies on the correspondence between neural network computations and rational McNaughton functions, enabling the translation of certain neural architectures into logical formulas. We summarize previously published results on the logical representation of ReLU–TId neural networks and on the encoding of reachability and robustness properties in Łukasiewicz logic.

ABSTRACT. Neural networks can be used as powerful predictors, but they are opaque. This is a serious drawback when they are used in areas such as medical diagnosis, where decisions must be auditable. In this paper, we present a pipeline that turns a trained neural network into a small set of human-readable logical rules, and then rebuilds those compiled rules back into a neural-symbolic network with fixed rules for interpretable prediction. Starting from a standard feed-forward classifier, we extract rule-based specifications using an existing symbolic knowledge extraction tool, and recompile them into a differentiable logic model in which logical operations such as conjunction, disjunction, and numerical inequalities are realised as smooth layers. Rulesets extracted in this way are typically large and contain redundancies. We therefore introduce a selection procedure that combines systematic rule removal with a contribution measure based on Shapley values adapted from cooperative game theory, allowing us to identify the rules that genuinely drive predictions. On a clinical classification task, the pipeline compresses the original network into just four rules while retaining 92% predictive accuracy, yielding a compact and interpretable approximation of the original model. Broader empirical validation across further domains is left to future work.

ABSTRACT. Probabilistic modeling libraries often require users to implement both forward transformations and their inverses in order to support transformed densities. This is tedious and error-prone, which motivates automatic program inversion. Standard invertible languages are unsatisfactory for modern probabilistic machine learning: reversible languages typically require every local operation to be invertible, while more expressive exact inference systems emphasize features such as higher-order functions and recursion and do not provide mechanized correctness guarantees for inversion by semi-inverses. We present a verified semi-inversion algorithm that treats inversion as search. Rather than insisting that every primitive be invertible, the algorithm searches for a computation path that reconstructs inputs from outputs by composing invertible, partially invertible, and non-invertible operations. We mechanize the algorithm and its soundness proof in Lean and show that it synthesizes inverses for representative normalizing-flow layers. We believe that our approach could enable more expressive exact probabilistic programming if integrated into existing exact inference systems and make it easier to develop new normalizing flows.

ABSTRACT. Recently, there is growing interest in the modeling and analysis of stochastic business processes. In procedural settings, most approaches rely on (Generalized) Stochastic Petri Nets, where firing delays follow negative exponential distributions due to their close connection to Continuous-Time Markov Chains. However, such distributions do not always adequately capture the uncertainties in real-world processes. In this work, we propose a stochastic, time-aware extension of BPMN in which uncertainty is modeled using Gaussian distributions. We capture uncertainty at two levels: the time required for an activity to complete and the choice among alternative activities. We translate the resulting models into a probabilistic programming representation that enables an analytical and differentiable approximation of the joint posterior distribution without sampling. This representation supports advanced probabilistic analyses of process behavior, including identifying factors influencing execution time, computing conditional activity completion times, and performing gradient-based optimization of probabilistic objectives.

ABSTRACT. In earlier work we introduced a modular framework for computing upper bounds on expected runtimes of randomized programs by combining upper bounds on expected runtime and size complexities of parts of the program. This approach relies only on bounds for expectations, thereby discarding crucial information on the shape of the underlying distributions. This limits the ways in which such bounds can be combined. Hence, our approach often required the consideration of bounds obtained from a classical analysis, where all probabilistic behavior is over-approximated into non-deterministic (non-probabilistic) choice. We now extend this framework by also computing bounds on higher moments. We show how to obtain such bounds for parts of the program by slightly adapting our notion of probabilistic linear ranking functions. This allows for combinations of bounds on expected time and size complexities using Hölder's inequality. So in this way, we can avoid over-approximations using classical bounds, which results in a substantially more powerful approach.

ABSTRACT. We show that existing tools for termination analysis are extremely well suited for LTL model checking of infinite state systems. To this end, we present a framework MoAT which uses the well-known automata-based approach and reduces the LTL model checking problem to deciding fair termination. To prove or disprove fair termination, it then calls the termination tools KoAT and LoAT in the backend. Our experiments show that in this way, MoAT is on par with existing state-of-the-art tools for LTL model checking of infinite state systems.

ABSTRACT. We present the theory underpinning a complexity analysis tool (currently under development) that aims to automate tedious parts of the analysis of complex algorithms originating in the field of automated reasoning. Examples are given by super-exponential quantifier elimination procedures in real and integer arithmetic. Our tool implements the following pipeline: 1. Together with the algorithm to be analysed, the user (an expert, e.g. the algorithm designer) can provide key metrics to track and lemmas to guide and improve the analysis. In pen-and-paper proofs, these correspond to the "non-tedious" and "creative" parts of the complexity analysis, that require human ingenuity. 2. The second step consists in the extraction of (generalised) recurrence equations. Here, we rely on a novel higher-order abstract interpretation technique, based on operator semantics. It enables (optimal) abstract compilation of symbolic programs into different kinds of purely numerical recursive representations, such as recurrence equations on interval-valued functions or numerical logic programs. 3. Finally, our tool solves the recurrence equations. We propose going beyond the direct use of computer algebra systems (CAS) by employing pre/postfixpoint-based techniques to discover and verify candidate bounds on the solutions. This approach, in turn, leverages recent progress in SMT solvers, and could benefit from techniques originating in termination-analysis research.

ABSTRACT. Hard subgraph-finding problems occur frequently across a wide range of applications, and there are many solvers dedicated to finding exact solutions for these problems. Unfortunately, the various communities that develop and use these algorithms do not share the strong history and careful blend of theory, engineering, science, and general paranoia that we've accumulated over the past thirty years in the constraint solving, Boolean satisfiability, and automated reasoning communities. This talk will share some of the horrors I have witnessed whilst working on solvers for problems like maximum common subgraph, subgraph isomorphism, and maximum (weighted) clique. Highlights will include buggy solvers, excessive parameter tuning, hard-coding parameters based upon instance filenames, badly-generated random benchmark sets, badly-generated non-random benchmark sets, reuse of good benchmark instances from other problems in a way that makes them bad, moving goalposts, multiplying other people's runtimes by mysterious scaling factors rather than re-running experiments, and entire systems built on top of not understanding the theory correctly. I will also talk about my ongoing efforts to fix these practices, and speculate as to why this has been a dismal failure.

ABSTRACT. Apart from continuously developing novel heuristics for MaxSAT local search solvers, substantial work has focused on maximizing the performance from choosing and tuning existing solvers. Most prior studies evaluate solvers primarily based on the solution quality obtained by the solvers at one or a small number of fixed time budgets. However, recent work has shown that anytime analysis can reveal significant differences in local search solvers across various problem instances and can also support algorithm configuration in discovering more effective parameter settings. While similar techniques have been widely explored in the domain of black-box optimization, we observe a notable gap in their application to constraint optimization and automated reasoning domains such as MaxSAT. In the talk, I plan to discuss both the opportunities and challenges of analyzing and exploiting anytime behavior in MaxSAT solvers, as well as potential extensions to broader pseudo-boolean optimization problems. In practice, I will start with examples of tuning the anytime performance of the MaxSAT solvers and extensions to dynamic algorithm selection.

ABSTRACT. High-performance SAT solvers are critical to many automated reasoning approaches today. However, most performance analysis and improvements to SAT solvers are software-centric, with a few exceptions. Thus, the potential for improving solver performance through hardware changes or hardware-aware programming remains largely untapped. To improve SAT solver performance through hardware-aware programming or hardware changes, the community needs better analysis of the impact of various hardware features and designs on SAT solving performance. To enable the collection and analysis of hardware performance metrics for SAT solving, we propose ArchSAT, a framework for collecting and analysing the effect of a variety of hardware metrics on SAT solving performance. We capture metrics from SAT solver runs that are relevant to hardware such as cache miss data, branch misprediction data, and overall runtime, using multiple profilers such as perf and Intel VTune. We also capture data relevant to SAT solving algorithms from the solver runs, such as time spent doing Boolean Constraint Propagation (BCP), number of removed clauses, and time spent doing inprocessing. ArchSAT then enables graphing these metrics against each other, enabling researchers to analyse how SAT solving behaviour correlates with hardware metrics. Overall, we believe ArchSAT will spur the development of hardware-aware techniques for SAT solving, and the discovery of benchmarks that illustrate solving patterns which are hard to run efficiently on current hardware. We hope it will also eventually spur the development of hardware accelerators for SAT solving (we intend to develop such accelerators as future work).

ABSTRACT. Benchmark selection is a crucial part of empirical evaluations in automated reasoning, and both in competitions and in papers it is crucial that benchmarks are selected in a fair and unbiased way. Moreover, given the costs of running large-scale empirical evaluations, it would be desirable to select benchmarks in such a way that their power to discriminate between solvers is maximized. Given the latter goal, it seems desirable to avoid selecting benchmarks that will just time out on all solvers, and prefer benchmarks that yield a mixture of lower running times, higher running times, and timeouts accross different solvers. This leads to the idea of letting a few reference solvers pick benchmarks in such a way that different running times are well represented among these benchmarks. However, choosing benchmarks in this way may inadvertly bias the benchmark selection in favor of the reference solvers, and hence this should not be done without carefully analyzing whether the method is statistically sound.

ABSTRACT. We introduce a new formalism for representing proofs in propositional logic called ``scroll nets''. Its fundamental construct is the scroll, a topological notation for implication proposed by C. S. Peirce at the end of the 19th century as the basis for his diagrammatic system of existential graphs (EGs). Scroll nets are derived from EGs by following the Curry-Howard methodology of internalizing inference rules inside judgments, just as terms in type theory internalize natural deduction rules. We focus on the intuitionistic implicative fragment of EGs, starting from an intuitive diagrammatic notation for scroll nets, and then distilling their combinatorial essence into an inductive definition. We also identify a notion of detour, as well as an equational theory inspired by cartesian monoidal categories that can be oriented to perform detour elimination. We illustrate how to simulate normalization in the simply typed $\lambda$-calculus, demonstrating both the logical and computational expressivity of our framework.

ABSTRACT. The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of non-associative categories as well as adjunctions between “bare” functors (reflexive graph morphisms) over such non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad ! (refining the necessity modality □) and a strong monad (written ◊). The starting point of our contribution is noti- cing that the completeness for a polarised syntax for ! and ◊ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads (Alten- kirch, Chapman and Uustalu, 2015; Arkor and McDermott, 2024): more precisely, comonads relative to ↓ (the positive shift functor) for ! and monads relative to ↑ (the negative shift functor) for ◊. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared in Jiang, Xue and New (2025) and Melliès (2025, 2026). Yet the syntax we present arose from proof-theoretic consideration in Munch-Maccagnoni (2009) and Curien, Fiore and Munch-Maccagnoni (CFMM 2016), without the link with relative (co)monads being noticed at the time. Our first remark and explanation is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the definition of adjunction between bare functors in this context, and estab- lish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model ! and ◊.

ABSTRACT. The traditional single-conclusion restriction in intuitionistic logic is often regarded as an external structural constraint that distinguishes it from classical multiple-conclusion systems. We explore here an alternative approach to capturing intuitionistic provability within a classical, multiple-conclusion framework by employing subexponentials. By extending Multiplicative-Additive Linear Logic (\mall) and full Linear Logic (\LL) with a linear subexponential ($!_l$), which does not allow for contraction and weakening, the systems \malll and \LLl are developed. A translation that systematically prepends the subexponential to subformulas enables hosting intuitionistic (single-conclusion) variants of MALL and LL in (multiple-conclusion) versions of \malll and \LLl. Specifically, a sequent is provable in the single-conclusion intuitionistic system if and only if its translation is provable in the corresponding multiple-conclusion subexponential system. This development demonstrates that the single-conclusion nature of intuitionistic logic can be viewed as an emergent property of specific logical connectives and subexponential constraints rather than an explicitly imposed constraint on the structure of sequents.

ABSTRACT. Frontrunning is a smart contract vulnerability that stems from the non-synchronous nature of blockchain transaction processing. Traditional approaches to detecting frontrunning in smart contracts rely on the notion of Transaction Order Dependence (TOD). A smart contract is considered to have TOD if the result of two contract calls may vary with their execution order. However, TOD does not serve as an accurate predictor for frontrunning vulnerabilities, as it disregards that honest users may purposefully limit contract calls to situations where reordering cannot be harmful. Following this observation, we develop the first frontrunning analysis tool that combines program analysis of a smart contract with protocol analysis for modeling honest user strategies.

ABSTRACT. Blockchain-based distributed consensus enables mutually mistrusting users to jointly realize decentralized services. Cryptocurrencies like Bitcoin or Ethereum use this technology to implement decentralized payment systems and computing platforms. These systems, however, suffer from scalability drawbacks: the underlying consensus mechanism inherently limits their throughput, causing long transaction processing times and transaction costs when scaling them up to large user numbers. A promising approach to mitigate these scalability issues are so-called off-chain protocols. In off-chain protocols, users exchange cryptographic information, which enables them to securely batch multiple transactions, such that their effect can be enforced with a small number of on-chain transactions that are processed by the consensus. Prominently, payment channels use such a mechanism to enable fast and cheap bilateral payments between users. While bringing practical benefits, off-chain protocols are hard to design securely: E.g., payment channel users only enjoy security guarantees if they meet channel-specific deadlines, and constantly monitor the blockchain to detect and punish misbehaviour of the channel counterparty. Small design flaws (e.g., a miscalculated deadline) can immediately result in the loss of user funds. Despite these complexities, so far, there exist no frameworks that help protocol designers in the secure design and verification of those protocols. To help this, we make the following contributions: (1) We present Renegade, an intermediate language for designing blockchain protocols - cryptographic protocols that involve blockchain interactions; (2) We present a compilation from Renegade protocols into blockchain protocols for Bitcoin. The compilation is general enough to be extended to many other cryptocurrencies as compilation targets; (3) We provide a computational soundness proof, showing that all behaviour of compiled protocols in a computational model of cryptography is captured by the symbolic Renegade protocol semantics; (4) We implement the Renegade semantics in the proof assistant Rocq, and conduct a case study, demonstrating Renegade’s utility in reasoning about state-of-the art payment channel protocols. The work presented in this paper is in progress.

ABSTRACT. The advent of quantum computers has initiated both research and standardization efforts toward the development of cryptographic primitives and communication protocols that remain secure against attackers equipped with quantum computers. Computer-aided verification has proven valuable in this context, as it helps identify flaws early and strengthens confidence in cryptographic systems. However, existing verification tools are typically designed for a specific attacker model (most often polynomial-time Turing machines in line with classical cryptographic assumptions) and therefore require adaptation to accurately capture the quantum setting. In this work, we present a novel post-quantum extension of Squirrel, a proof assistant that provides computational guarantees for cryptographic primitives and protocols. Our extension is fully embedded in the higher-order logic underlying Squirrel, allowing logical terms to directly represent quantum values. This design choice makes the extension generic, preserves compatibility with the latest features of Squirrel, and supports its long-term integration into the tool. We implement our approach within Squirrel and validate it through several case studies. In particular, we obtain post-quantum security guarantees for multiple KEM combiners, as well as for two hybrid key-exchange protocols.

ABSTRACT. Security proofs for cryptographic protocols are notably complex and error-prone, in particular in the computational model. Computer-aided cryptography aims at increasing the confidence in these proofs, by mechanising them and formally verifying them with automated tools. One such tool is the Squirrel proof assistant. In this paper, we use it to prove the Post-Compromise Security (PCS) of an asymmetric ratchet mechanism used to generate shared keys, such as the one featured in the Signal protocol. While Squirrel is convenient to study stateful protocols such as the ratchet, the analysis his is made particularly challenging by the fact that the usual notion of secrecy for Squirrel, i.e. real-or-random secrecy, is not well-suited to that protocol. We instead define predicates and a proof system for non-deducibility, a weaker notion of secrecy, which we found to be the notion needed to study the asymmetric ratchet. We establish the soundness of the proof system, implement it within the Squirrel prover, and use it to write a proof of PCS for the asymmetric ratchet, which is the first mechanised such proof.

ABSTRACT. For high-assurance software, source-level reasoning is insufficient: we need binary-level guarantees. Despite constrained Horn clause (CHC) solving being one of the most popular forms of automated verification, prior work has not evaluated the viability of CHC solving for binary analysis. To fill this gap, we assemble a pipeline that encodes binary analysis problems as CHCs in the SMT logic of quantifier-free bit vectors, and show that off-the-shelf CHC solvers achieve reasonable success on binaries compiled from 983 C invariant inference benchmarks: a portfolio solves 59.5% and 66.0% of the problems derived from the unoptimized and optimized binaries, respectively—roughly equal to the success rate of a leading C verifier on the source code (60.1%). Moreover, we show that binary analysis provides a valuable source of bit-vector CHC benchmarks (which are in short supply): binary-derived problems differ from existing benchmarks both structurally and in solver success rates and rankings. Augmenting CHC solving competitions with binary-derived benchmarks will encourage solver developers to improve bit-vector reasoning, in turn making CHC solving a more effective tool for binary analysis.

ABSTRACT. The CHC competition (CHC-COMP) compares state-of-the-art tools for CHC solving with respect to performance and effectiveness on a set of publicly available benchmarks. The winners among participating solvers are recognized by measuring the number of correctly solved benchmarks as well as the runtime. The results of CHC-COMP 2026 will be announced at the HCVS workshop.

ABSTRACT. We present an Isabelle/HOL mechanisation of rely-guarantee reasoning combined with separation logic, developed on the seL4 trace monad: an Aczel-style trace model that makes environment interference first-class. We follow Feng's local rely-guarantee (LRG) because its frame rule fits the seL4 Microkit framework we target: a static-architecture setting in which components, their memory-region mappings, and the communication channels between them are fixed at build time. The development so far has: (i) LRG's frame and hide rules, mechanised over the trace monad's primitives, sequential composition, and while loops; (ii) an n-ary parallel composition rule; and (iii) a three-component Microkit case study (a producer/filter/consumer pipeline over shared memory regions) composed by the n-ary parallel rule.

ABSTRACT. Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem by introducing the Abduction Prover for Isabelle/HOL. Given a challenging proof goal, the Abduction Prover constructs a proof script for the goal by identifying useful conjectures using abductive reasoning.

ABSTRACT. Large language models (LLMs) and proof assistants are in the early days of a fruitful marriage. LLM-based agents draft and mechanize, while the proof assistants patiently check the resulting proofs. We consider two aspects of safety when integrating agents with the Isabelle proof assistant. First, we survey different technological methods to isolating agents and restricting what they can do through Isabelle. Second, we discuss different agentic workflows and the degree of human intervention needed to assure the logical consistency of the resulting artifacts.

ABSTRACT. Model counting has a clear semantics in propositional logic, but its extension to SMT is less canonical. In this talk, we discuss two different interpretations of “#SMT”. In a strong sense, #SMT counts or measures the theory-level solution space, leading to problems such as volume computation, weighted model integration, and symbolic integration. In a weaker sense, the task is to count theory-consistent Boolean assignments over the atoms of the formula, yielding a Boolean-theory interface closer to AllSMT and T-#SAT. These two views correspond to different mathematical objects and algorithmic challenges. While theory-level counting depends on the measure induced by the background theory, predicate-space counting exposes the combinatorial structure of SMT formulas. The talk is intended as a perspective on the landscape of counting modulo theories, a direction that remains comparatively underexplored.

ABSTRACT. Weighted model integration (WMI) is a relatively recent formalism that has received significant interest as a technique for solving probabilistic inference tasks with complicated weight functions. Existing methods and tools are mostly focused on linear and polynomial functions and provide limited support for WMI of rational or radical functions, which naturally arise in several applications. In this work, we present a novel method for approximate WMI, which provides more effective support for the wide class of semi-algebraic functions that includes rational and radical functions, with literals defined over non-linear real arithmetic. Our algorithm leverages Farkas’ lemma and Handelman's theorem from real algebraic geometry to reduce WMI to solving a number of linear programming (LP) instances. The algorithm provides formal guarantees on the error bound of the obtained approximation and can reduce it to any user-defined value epsilon. Furthermore, our approach is perfectly parallelizable. Finally, we present extensive experimental results, demonstrating the superior performance of our method on a range of WMI tasks for rational and radical functions when compared to state-of-the-art tools for WMI, in terms of both applicability and tightness. This is a joint work with S. Akshay, Supratik Chakraborty, Soroush Farokhnia, Amir Goharshady, Harshit Jitendra Motwani, Đorđe Žikelić. This work was presented at IJCAI 2025.

ABSTRACT. The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as C2. This polynomial-time complexity is known to be retained when extending C2 by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from C2. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having k connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials.

ABSTRACT. Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical do- mains, and hence verifying properties on these models has been an active topic of study over the last decade. One such verification question is the problem of sensitivity, which asks, given a DTE, whether a small change in subset of features can lead to misclassification of the input. In this work, our focus is to build a quantitative notion of sensitivity, tailored to DTEs, by discretizing the input space of the model and enu- merating the regions which are susceptible to sensitivity. We propose a novel algorithmic technique that can perform this computation effi- ciently, within a certified error and confidence bound. Our approach is based on encoding the problem as an algebraic decision diagram (ADD), and further splitting it into subproblems that can be solved efficiently and make the computation compositional and scalable. We evaluate the performance of our technique over benchmarks of varying size in terms of number of trees and depth, comparing it against the performance of model counters over the same problem encoding. Experimental results show that our tool EnSensCount achieves significant speedup over other approaches and can scale well with the increasing sizes of the ensembles. This paper was accepted at CAV'26.