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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. The counting problem #2SAT is complete for #P under Turing (many-call) reductions, which dates back to the seminal work by Valiant from 1979. Arguably, this reduction is the opposite from being simple as it is a sophisticated chain of transformation from #SAT, via several variations of the problem of computing the permanent, to the task of counting matchings in graphs, and then finally to #2SAT. In contrast, we give a simple classroom reduction that makes only two calls instead of polynomially many calls that can be then merged into a single call with arithmetic postprocessing (AC0).

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. As machine learning models such as Random Forests are increasingly deployed in high-stakes environments, the need for formal and rigorous explainability has become paramount. Probabilistic abductive explanations offer a robust framework for this by identifying minimal feature subsets that guarantee a specific prediction with a high probability. However, computing these explanations is notoriously complex. A highly promising approach to solving this is transforming the explanation search into a propositional model counting problem. In this paper, we investigate the practical challenges and algorithmic nuances of this transformation. Specifically, we study the overarching impact of the domain theory formulation and closely examine the role of the majority voting constraint inherent to Random Forests. Because this majority rule acts as a critical cardinality constraint within the propositional logic framework, its representation significantly influences computational performance. We systematically explore various encoding techniques for this cardinality constraint and empirically analyze how different encodings impact the overall effectiveness and efficiency of the underlying model counter. By evaluating these design choices, this work provides critical insights into optimizing the translation of tree-ensemble explainability into tractable model counting instances, paving the way for more scalable formal explanation tools.

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. 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. 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. 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. 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. 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 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. 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. 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. 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. 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. 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. 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.

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. 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. 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. 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. Mathematicians and computer scientists are increasingly using proof assistants to formalize and check correctness of complex proofs. This is a non-trivial task in itself, however, with high demands on human expertise. Can we lower the bar by introducing automation for conjecturing helpful, interesting and novel lemmas? We present the first neuro-symbolic lemma conjecturing tool, LEMMANAID, designed to discover conjectures by drawing analogies between mathematical theories. LEMMANAID uses a fine-tuned LLM to generate lemma templates that describe the shape of a lemma, and symbolic methods to fill in the details. We compare LEMMANAID against the same LLM fine-tuned to generate complete lemma statements (a purely neural method), as well as a fully symbolic conjecturing method. LEMMANAID consistently outperforms both neural and symbolic methods on test sets from Isabelle's HOL library and from its Archive of Formal Proofs (AFP). Using DeepSeek-coder-6.7B as a backend, LEMMANAID discovers 50% (HOL) and 28% (AFP) of the gold standard reference lemmas, 8-13% more than the corresponding neural-only method. Ensembling two LEMMANAID versions with different prompting strategies further increases performance to 55% and 34% respectively. In a case study on the formalization of Octonions, LEMMANAID discovers 79% of the gold standard lemmas, compared to 62% for neural-only and 23% for the state of the art symbolic tool. Our result show that LEMMANAID is able to conjecture a significant number of interesting lemmas across a wide range of domains covering formalizations over complex concepts in both mathematics and computer science, going far beyond the basic concepts of standard benchmarks such as miniF2F, PutnamBench and ProofNet.

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. Predicting gene expression dynamics is challenging due to the complex regulatory interactions within high-dimensional datasets. We evaluate predictive models that integrate temporal patterns with gene–gene networks, comparing a state-of-the-art approach based on Protein-Protein Interaction (PPI) networks from STRING with models utilizing data-driven network inference. Our results show that inferred networks can enhance accuracy over static biological priors. However, simpler models treating genes independently often achieve comparable performance. This suggests that for the considered datasets, the added complexity of explicit gene–gene interactions does not always translate into superior predictive power, opening to further investigations on the most effective ways to represent and leverage biological connectivity in forecasting tasks.

ABSTRACT. Gliomas are the most common type of brain tumor in adults and are associated with poor prognosis and high mortality. Despite technological advances, their classification remains challenging in both clinical practice and research, highlighting the need for improved molecular subtyping to enhance diagnosis and treatment. In this study, we systematically evaluate the robustness of current glioma classification using a reproducible pipeline for unsupervised patient stratification. We apply multiple multi-view clustering methods, namely, CIMLR, intNMF, and moCluster, to cluster glioma patients based on transcriptomics and methylomics data. All methods consistently distinguished glioblastoma (GBM) from lower-grade gliomas, with survival analysis confirming poorer outcomes for GBM clusters, in line with clinical expectations. The best partition was obtained with CIMLR, closely aligning with the 2021 WHO classification of central nervous system tumors. In contrast, intNMF identified three clusters with distinct survival distributions, suggesting additional biological heterogeneity that warrants further investigation. To enhance robustness and better capture tumor complexity, we implemented consensus clustering to integrate results across methods. This integrative approach yielded well-defined groups with improved concordance to established glioma subtypes compared to individual methods. Notably, the consensus solution identified more clusters than the traditional classification, revealing deeper molecular characterization and providing a framework to refine glioma classification. Furthermore, we identified key molecular features supported by the literature, including both established and emerging biomarkers. Overall, our findings underscore the value of multi-omics integration and consensus clustering in refining glioma classification, supporting the discovery of novel biomarkers to improve diagnostics, prognostics, and patient outcomes.

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. (TBD)

ABSTRACT. Formal explainability of neural network classifiers increasingly relies on logical reasoning to obtain guarantees about model behaviour in regions of the continuous input space, not just at isolated sample points. Existing formal XAI techniques often yield explanations that constrain each feature independently and therefore cannot capture the rich dependencies among features that underlie non-trivial decision boundaries. This limitation leads to explanations that are either too weak to be informative or too local to provide insight beyond the queried sample. This work introduces space explanations, a logic-based notion of explanation that represents sufficient conditions for a neural network to predict a given class over a (potentially large and geometrically complex) subset of the feature space. A space explanation is a logical formula that is sound with respect to the classifier: every point satisfying the formula is guaranteed to be classified into the target class. Due to the generality of space explanations, they can approximate non-linear decision boundaries and express relationships among features. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. The framework supports several strategies that expose different uses of interpolation and unsatisfiable cores. A Generalize strategy computes interpolants using families of arithmetic interpolation algorithms. A Reduce strategy weakens and simplifies explanations by computing unsatisfiable cores; A Capture strategy focuses generalization on a chosen subset of features, keeping the remaining dimensions fixed and thereby isolating interpretable relationships between selected features while still leveraging interpolation for sound generalization. These strategies are implemented in the prototype tool SpEXplAIn, focusing on QF_LRA logic, on top of the interpolating solver OpenSMT2, and integrates multiple interpolation algorithms. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the interpolation-based explanations are more meaningful than those computed by state-of-the-art.

ABSTRACT. Modal logics are non-classical logics that extend classical logic with modal operators □ and ♢ respectively representing necessity and possibility. An implementation of model finding in quantified modal logics is given by the finite model finder MoMo for quantified mono-modal logics. While results of its evaluation prove the practicality of this method, challenges specific to the translational approach for model finding followed by MoMo can be observed. This extended abstract addresses them and discusses potential solutions to overcome them.

ABSTRACT. The interest in explanations in the context of AI research is often directly associated with the field of explainable AI (XAI), where one of the goals is to automatically generate explanations of the outputs of AI-based systems—in particular the outputs of machine learning systems [4]. Still, especially in relation to normative questions, there is an established line of research aimed at automating explanations of other phenomena; notably, AI-based systems have been used for generating explanations of legal outcomes [1]. We consider related research where explanatory dialogue games generated from argumentation frames are developed [2, 6], and we extend these approaches by (i) considering agent uncertainty, modeled via argumentation frames with preferences, which gives rise to a new type of locution, or speech act, in the dialogues and by (ii) considering the role of specific relations between norms in the case of explanations with deontic or normative components, as in [6], and thus also a new type of locution in the dialogues. Explanations, as they are considered here, can be defined as answers to “why-questions,” a definition taken from research in the humanities and social sciences [4]. From this research certain features have been identified as important for explanations to be understandable and useful to humans: “good” explanations are contrastive, selective, non-probabilistic and social. It is claimed in [1] that legal explanations naturally have each of these features, but it is not clear to what extent these features remain desirable for normative or deontic explanations (of which legal explanations are a subclass). This is because much of the research considered in [4] is concerned with explanations which are causal in nature, and there is reason to believe that normative explanations are not the same as, nor reducible to causal explanations [7]. In particular, theories of contrastive explanation make explicit reference to causal histories [3], and we want to address two types of explanations of normative issues which appeal, not to the causal history of some putative fact coming to be, but instead (i) to the relative quality of the evidence in favor of concluding that fact or (ii) to the relation between some norm(s) from which the fact would follow and other more basic norms or principles. Thus, we move toward explanations which are not strictly contrastive because the setting is no longer purely causal. In order order to allow for explanations of these types, we propose a framework like those discussed in [2, 6], with some additional features. First, we define the argumentation frames on which the dialogues are based. We consider argumentation frames which incorporate pref- erences over arguments because we want to consider agent uncertainty, and this is modeled via arguments that rest on premises of varying quality. Specifically, we use structured argumenta- tion frames where the logical content of each argument defines which arguments it attacks, and we make use of a preference ordering over the set of arguments based on a preference ordering over the potential argument premises, as, for example, in [5]. This captures how the strength of certain beliefs/evidence can affect the strength of arguments, and this doxastic component bears on deontic explanations despite its independent interest; for example, agents can explain disagreements about violations via appeal to individual beliefs about the facts or norms. We then consider a new locution in the dialogues based on these argumentation frames, whereby arguments can be defended from attacking arguments by appeal to the preference ordering. In natural language these new locutions represent statements like “while that would be a reason to reject my claim, it is not supported by the evidence,” and such locutions allow us to give explanatory meaning to the preferences included in the argumentation frame. A second modification to the methods of [2, 6] that we consider is to allow for locutions which question norms themselves; while in [6] it is possible to question obligations following from norms, there is no way to question norms directly. However, such “why-norm-questions” are common in ethical and legal discourse. In order to incorporate these questions into our dialogue games we consider two ideas for extensions to the underlying argumentation frames. The first idea is to include an additional knowledge base which encodes the relational structure between the norms; general norms like “thou shalt not lie” might be the normative grounding for more specific norms like “don’t say you are coming, if you are not going to come,” and the knowledge base would capture these inter-norm relations which could be exploited for explanation. The second proposal is to include an additional labeling on the norms, which encodes the principles or values on which each norm is based, e.g. honesty, fairness, etc. Then, agents could respond to “why-norm-questions” by providing these principles. We also consider requirements on these types of locutions which might make such dialogues more plausible; e.g. we could require that agents only question norms they do not rely on in their previously moved arguments. By including these novel locutions and encoding this extra information in the argumentation frame, we are able to explore the role of “why-norm-questions” in explanatory dialogues. In sum, although the push to include conceptual research on explanations introduces key desiderata for “good explanations” in the context of XAI, we have to carefully consider whether these apply equally to normative explanations. We argue that the requirement of contrastive explanations should be relaxed in order to support questions about the norms themselves, and that explanations of certain facts need not always appeal to counterarguments against alternatives, but may also be supported by arguments in favor of their evidential or doxastic grounds. Finally, we present and investigate extended argumentation frameworks which can support dialogue games with additional locutions for the proposed purposes. References: [1] Katie Atkinson, Trevor Bench-Capon, and Danushka Bollegala. “Explanation in AI and law: Past, present and future”. In: Artificial Intelligence 289 (2020). [2] Xiuyi Fan and Francesca Toni. “On Computing Explanations in Argumentation”. In: Pro- ceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. 2015, pp. 1496– 1502. [3] Tim Miller. “Contrastive explanation: a structural-model approach”. In: The Knowledge Engineering Review 36 (2021), e14. [4] Tim Miller. “Explanation in artificial intelligence: Insights from the social sciences”. In: Artificial Intelligence 267 (2019), pp. 1–38. [5] Sanjay Modgil and Henry Prakken. “A general account of argumentation with preferences”. In: Artificial Intelligence 195 (2013), pp. 361–397. [6] Kees van Berkel and Christian Straßer. “Towards Deontic Explanations Through Dia- logue”. In: ArgXAI-24: 2nd International Workshop on Argumentation for eXplainable AI. 2024. [7] Kate Vredenburgh. “The Right to Explanation”. In: The Journal of Political Philosophy 30.2 (2022), pp. 209–229.

ABSTRACT. Dynamic Epistemic Logic (DEL) extends epistemic logic by modelling how knowledge is revised through communication events, represented by dynamic modalities. Among the simplest and historically most influential systems of DEL is Public Announcement Logic (PAL). Unlike in epistemic logic, that models agents' knowledge through static sets of possible worlds, PAL focuses on how public communication updates agents' knowledge, through transformations of these structures. In PAL then, an announcement by A updates an epistemic model (S5 Kripke model) into a new model. While the semantics of PAL is inherently dynamic, with updates of epistemic models, its proof-theoretic side has been lacking a syntactic representation of such a dynamism for a long time. In a previous work, we introduced dynamic hypersequents to represent with purely syntactical means the inherent dynamism of PAL. Within this framework we proposed a calculus for the single-agent fragment of PAL. Building on this and on a method to represent agents' uncertainty in hypersequents, we now introduce indexed dynamic hypersequents and propose a hypersequent calculus for the full logic of public announcements. This calculus is sound and complete, and enjoys several important properties: in particular, all its structural rules, including the contraction rules as well as the cut-rule, are provably admissible.

ABSTRACT. The Compositional Learning-And-Reasoning for AI Complex Systems Engineering (CLARA) fundamental research program is designed to tightly integrate Automated Reasoning (AR) and Machine Learning (ML) components to create high-assurance AI — which is expected to scale even to complex systems of systems. Integrating the two different branches of AI will provide the speed and flexibility of ML with verifiability based on AR proofs that have strong logical explainability and computational tractability.

ABSTRACT. We propose a decoupled approach to synthesizing a word, letter by letter, that is in the conjunction of a given pair of regular objectives. A key application is multi-objective robotic path planning, where each letter corresponds to a robot action and the goal is to find a plan that satisfies both objectives. The traditional monolithic solution would construct the product automaton, and obtains a ``generator'' that outputs an accepting word. Instead, we synthesize two independent generators and compose them at runtime via an auction-based mechanism: at each time step, the generators bid for who chooses the next symbol. Advantages of this approach include design in parallel or by different vendors, and reusability, namely when an objective changes only the relevant generator is updated and the other is reused. We design, for the first time, a framework in which each generator is designed on a separate automaton, which enables specifying objectives as logical formulas. For cases in which a feasible solution is not found, we develop a successive refinement algorithm that searches for a pair of assumptions that regain feasibility. Weaker assumptions lead to increased modularity. Our algorithm is based on a novel automata-learning algorithm that can be of independent interest. We design proof-of-concept experiments where we implement our algorithm, and demonstrate the effectiveness.

ABSTRACT. History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomise and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is λ-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.

ABSTRACT. Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating according to the syntax of a programming language leads to a large search space, and hence slow synthesis, due in large part to semantic duplication. A synthesiser may have to evaluate—and reject—multiple semantically identical but syntactically different programs, wasting resources. To avoid this duplication, we present NSynC, a synthesis-by-semantics approach. By enumerating the semantics of the target language directly, we guarantee that each candidate program is semantically unique and that each evaluation of a candidate is meaningful. Specifically, we search the space of normal forms for the simply-typed lambda calculus with sums using a top-down, type-directed synthesis algorithm. Our preliminary results show a geomean speedup of 8.93x on a synthetic benchmark suite over the unrestricted algorithm.

ABSTRACT. Traditional type systems prevent basic errors but lack the expressiveness to handle logical errors or prove complex program properties. Refinement types address this by augmenting base types with decidable first-order logic constraints. However, writing them manually is difficult, which ultimately hinders their widespread adoption. Existing symbolic and data-driven inference approaches often struggle to scale to multi-function programs or rely heavily on manual annotations. In this work, we present a neurosymbolic approach for automated refinement type synthesis. Our methodology converts the refinement typing rules into a graphical representation and learns semantic representations via a Graph Neural Network (GNN). An autoregressive decoder model then synthesizes predicates, using Reinforcement Learning (RL) to navigate the search space while a type checker verifies candidates. However, a core challenge in this setting is the sparse-reward problem, where type checker feedback provides insufficient guidance for the RL agent. To address this, we introduce two main contributions. First, novel Behavioral Rewards utilizing subspecifications and semantic program slicing to provide partial rewards. Second, a data-driven, CEGAR-Guided Learning loop that refines reward signals based on incremental correctness. Together, these techniques generate denser rewards and accelerate convergence. Our implementation and initial evaluation demonstrates that the framework can synthesize semantically correct specifications for complex programs and properties.