CyberSec Research

We present new results on finite satisfiability of logics with counting and arithmetic. This includes tight bounds on the complexity for two-variable logic with counting and cardinality comparisons between unary formulas, and also on logics with so-called local Presburger quantifiers. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.

We exhibit an adjunction between a category of abstract algebras of partial functions that we call difference-restriction algebras and a category of Hausdorff \'etale spaces. Difference-restriction algebras are those algebras isomorphic to a collection of partial functions closed under relative complement and domain restriction. Our adjunction generalises the adjunction between the category of generalised Boolean algebras and the category of Hausdorff spaces. We define the finitary compatible completion of a difference-restriction algebra and show that the monad induced by our adjunction yields the finitary compatible completion of any difference-restriction algebra. As a corollary, the adjunction restricts to a duality between the finitarily compatibly complete difference-restriction algebras and the locally compact zero-dimensional Hausdorff \'etale spaces, generalising the duality between generalised Boolean algebras and locally compact zero-dimensional Hausdorff spaces. We then extend these adjunction, duality, and completion results to difference-restriction algebras equipped with arbitrary additional compatibility preserving operators.

In order to develop solutions that perform actions as early as possible, analysis of distributed algorithms using epistemic logic has generally concentrated on ``full information protocols'', which may be inefficient with respect to space and computation time. The paper reconsiders the epistemic analysis of the problem of Simultaneous Byzantine Agreement with respect to weaker, but more practical, exchanges of information. The paper first clarifies some issues concerning both the specification of this problem and the knowledge based program characterizing its solution, concerning the distinction between the notions of ``nonfaulty'' and ``not yet failed'', on which there are variances in the literature. It is then shown that, when implemented relative to a given failure model and an information exchange protocol satisfying certain conditions, this knowledge based program yields a protocol that is optimal relative to solutions using the same information exchange. Conditions are also identified under which this implementation is also an optimum, but an example is provided that shows this does not hold in general.

AGI (Strong AI) aims to create intelligent robots that are quasi indistinguishable from the human mind. Like a child, the AGI robot would have to learn through input and experiences, constantly progressing and advancing its abilities over time. The AGI robot would require an intelligence more close to human's intelligence: it would have a self-aware consciousness that has the ability to solve problems, learn, and plan. Based on this approach an Intensional many-sorted First-order Logic (IFOL), as an extension of a standard FOL with Tarskian's semantics, is proposed in order to avoid the problems of standard 2-valued FOL with paradoxes (inconsistent formulae) and a necessity for robots to work with incomplete (unknown) knowledge as well. This is a more sophisticated version of IFOL with the same syntax but different semantics, able to deal with truth-ordering and knowledge-ordering as well, based on the well known Belnap's billatice with four truth-values that extend the set of classical two truth-values.

We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For this purpose, we introduce specifications with both passive and active quantification over traces. While passive trace quantifiers range over the traces that are observed, active trace quantifiers are instantiated with \emph{generator functions}, which are part of the specification. Generator functions enable the monitor to construct traces that may never be observed at runtime, such as the linearizations of a concurrent trace. As specification language, we extend hypernode logic with trace quantifiers over generator functions and interpret these hypernode formulas over possibly infinite domains. We present a corresponding monitoring algorithm, which we implemented and evaluated on a range of hyperproperties for concurrency and security applications. Our method enables, for the first time, the monitoring of asynchronous hyperproperties that contain alternating trace quantifiers.

The informal question of when two theorem proofs are "essentially the same" goes back to David Hilbert, who considered adding it (or something largely equivalent) to his famous list of open problems, but eventually decided to leave it out. Given that the notion of a formal proof is closely related to that of a (computer) program, i.e. a recursive function, it may be useful to ask the same question with regard to programs instead. Here we propose a minimalistic approach to this question within Recursion Theory, building heavily on the use of Kolmogorov Complexity.

Separation logic was conceived in order to make the verification of pointer programs scalable to large systems and it has proven extremely effective. The key idea is that programs typically access only small parts of memory, allowing for local reasoning. This idea is implemented in separation logic by extending first-order logic with separating connectives, which inspect local regions of memory. It turns that this approach not only applies to pointer programs, but also to programs involving other resource structures. Various theories have been put forward to extract and apply the ideas of separation logic more broadly. This resulted in algebraic abstractions of memory and many variants of separation logic for, e.g., concurrent programs and stochastic processes. However, none of the existing approaches formulate the combination of first-order logic with separating connectives in a theory that could immediately yield program logics for different resources. In this paper, we propose a framework based on the idea that separation logic can obtained by making first-order logic resource-aware. First-order logic can be understood in terms of categorical logic, specifically fibrations. Our contribution is to make these resource-aware by developing categorical logic internally in categories of sheaves, which is what we call sheafeology. The role of sheaves is to model views on resources, through which resources can be localised and combined, which enables the scalability promised by separation logic. We contribute constructions of an internal fibration in sheaf categories that models predicates on resources, and that admits first-order and separating connectives. Thereby, we attain a general framework of separation logic for generic resources, a claim we substantiate by instantiating our framework to various memory models and random variables.

This paper outlines a general formal framework for reasoning systems, intended to support future analysis of inference architectures across domains. We model reasoning systems as structured tuples comprising phenomena, explanation space, inference and generation maps, and a principle base. The formulation accommodates logical, algorithmic, and learning-based reasoning processes within a unified structural schema, while remaining agnostic to any specific reasoning algorithm or logic system. We survey basic internal criteria--including coherence, soundness, and completeness-and catalog typical failure modes such as contradiction, incompleteness, and non-convergence. The framework also admits dynamic behaviors like iterative refinement and principle evolution. The goal of this work is to establish a foundational structure for representing and comparing reasoning systems, particularly in contexts where internal failure, adaptation, or fragmentation may arise. No specific solution architecture is proposed; instead, we aim to support future theoretical and practical investigations into reasoning under structural constraint.

Causal reasoning is essential for understanding decision-making about the behaviour of complex `ecosystems' of systems that underpin modern society, with security -- including issues around correctness, safety, resilience, etc. -- typically providing critical examples. We present a theory of strategic reasoning about system modelling based on minimal structural assumptions and employing the methods of transition systems, supported by a modal logic of system states in the tradition of van Benthem, Hennessy, and Milner, and validated through equivalence theorems. Our framework introduces an intervention operator and a separating conjunction to capture actual causal relationships between component systems of the ecosystem, aligning naturally with Halpern and Pearl's counterfactual approach based on Structural Causal Models. We illustrate the applicability through examples of of decision-making about microservices in distributed systems. We discuss localized decision-making through a separating conjunction. This work unifies a formal, minimalistic notion of system behaviour with a Halpern--Pearl-compatible theory of counterfactual reasoning, providing a logical foundation for studying decision making about causality in complex interacting systems.

Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from the over-approximation methods that are used in traditional logics such as Hoare Logic or Separation Logic. Although the soundness of ISL has been established, its completeness remains unproven. In this study, we establish relative completeness by leveraging the expressiveness of the weakest postconditions; expressiveness is a factor that is critical to demonstrating relative completeness in Reverse Hoare Logic. In our ISL framework, we allow for infinite disjunctions in disjunctive normal forms, where each clause comprises finite symbolic heaps with existential quantifiers. To compute the weakest postconditions in ISL, we introduce a canonicalization that includes variable aliasing.

The growing integration of Artificial Intelligence (AI) into education has intensified the need for transparency and interpretability. While hackathons have long served as agile environments for rapid AI prototyping, few have directly addressed eXplainable AI (XAI) in real-world educational contexts. This paper presents a comprehensive analysis of the XAI Challenge 2025, a hackathon-style competition jointly organized by Ho Chi Minh City University of Technology (HCMUT) and the International Workshop on Trustworthiness and Reliability in Neurosymbolic AI (TRNS-AI), held as part of the International Joint Conference on Neural Networks (IJCNN 2025). The challenge tasked participants with building Question-Answering (QA) systems capable of answering student queries about university policies while generating clear, logic-based natural language explanations. To promote transparency and trustworthiness, solutions were required to use lightweight Large Language Models (LLMs) or hybrid LLM-symbolic systems. A high-quality dataset was provided, constructed via logic-based templates with Z3 validation and refined through expert student review to ensure alignment with real-world academic scenarios. We describe the challenge's motivation, structure, dataset construction, and evaluation protocol. Situating the competition within the broader evolution of AI hackathons, we argue that it represents a novel effort to bridge LLMs and symbolic reasoning in service of explainability. Our findings offer actionable insights for future XAI-centered educational systems and competitive research initiatives.

Transformers are the basis of modern large language models, but relatively little is known about their precise expressive power on graphs. We study the expressive power of graph transformers (GTs) by Dwivedi and Bresson (2020) and GPS-networks by Ramp\'asek et al. (2022), both under soft-attention and average hard-attention. Our study covers two scenarios: the theoretical setting with real numbers and the more practical case with floats. With reals, we show that in restriction to vertex properties definable in first-order logic (FO), GPS-networks have the same expressive power as graded modal logic (GML) with the global modality. With floats, GPS-networks turn out to be equally expressive as GML with the counting global modality. The latter result is absolute, not restricting to properties definable in a background logic. We also obtain similar characterizations for GTs in terms of propositional logic with the global modality (for reals) and the counting global modality (for floats).

Standpoint extensions of knowledge representation formalisms have been recently introduced as a means to incorporate multi-perspective modelling and reasoning through modal operators that attribute pieces of knowledge to specific entities or agents. In these extensions, the integration between conceptual modelling and perspective annotations can vary in strength, with monodic standpoint extensions offering a well-balanced approach. They allow for advanced modelling features, such as the expression of rigid concepts, while maintaining desirable reasoning complexity. We consider the extension of C2--the counting two-variable fragment of first-order logic--by monodic standpoints. At the heart of our work is a polynomial-time translation of formulas in this extended formalism into standard, standpoint-free C2, a result that relies on intricate model-theoretic arguments. Thanks to this translation, the satisfiability problem remains at the same complexity level: NExpTime-complete, as in plain C2. Since our formalism subsumes monodic S5 over C2, this result also marks a substantial advancement in the study of first-order modal logics. From a practical standpoint, this means that highly expressive description logics such as SHOIQBs and SROIQBs--which underpin the widely adopted OWL 1 and OWL 2 ontology languages standardised by the W3C--can be extended with monodic standpoints without increasing the standard reasoning complexity. We further prove that NExpTime-hardness arises even in significantly less expressive description logics, as long as they include both nominals and monodic standpoints. Moreover, we show that if the monodicity restriction is relaxed even slightly in the presence of inverse roles, functionality, and nominals, the satisfiability problem becomes undecidable.

We present a term rewriting system that models the dynamic aspects of the free cornering with protocol choice of a monoidal category, which has been proposed as a categorical model of process interaction. This term rewriting system is confluent and terminating in an appropriate sense. We use this machinery to prove a coherence theorem for the free cornering with protocol choice.

We propose a method to synthesize a parameterized infinite-state systems that can be instantiated for different parameter values. The specification is given in a parameterized temporal logic that allows for data variables as well as parameter variables that encode properties of the environment. Our synthesis method runs in a counterexample-guided loop consisting of four main steps: First, we use existing techniques to synthesize concrete systems for some small parameter instantiations. Second, we generalize the concrete systems into a parameterized program. Third, we create a proof candidate consisting of an invariant and a ranking function. Fourth, we check the proof candidate for consistency with the program. If the proof succeeds, the parameterized program is valid. Otherwise, we identify a parameter value for which the proof fails and add a new concrete instance to step one. To generalize programs and create proof candidates, we use a combination of anti-unification and syntax-guided synthesis to express syntactic differences between programs as functions of the parameters. We evaluate our approach on examples from the literature that have been extended with parameters as well as new problems.

We establish a correspondence between (fragments of) $\mathcal{TEL}^\bigcirc$, a temporal extension of the $\mathcal{EL}$ description logic with the LTL operator $\bigcirc^k$, and some specific kinds of formal grammars, in particular, conjunctive grammars (context-free grammars equipped with the operation of intersection). This connection implies that $\mathcal{TEL}^\bigcirc$ does not possess the property of ultimate periodicity of models, and further leads to undecidability of query answering in $\mathcal{TEL}^\bigcirc$, closing a question left open since the introduction of $\mathcal{TEL}^\bigcirc$. Moreover, it also allows to establish decidability of query answering for some new interesting fragments of $\mathcal{TEL}^\bigcirc$, and to reuse for this purpose existing tools and algorithms for conjunctive grammars.

Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for arbitrary programs. Some approaches have been proposed to synthesize loop invariants using symbolic techniques and more recently using neural approaches. These approaches are able to correctly synthesize loop invariants only for subsets of standard benchmarks. In this work, we investigate whether modern, reasoning-optimized large language models can do better. We integrate OpenAI's O1, O1-mini, and O3-mini into a tightly coupled generate-and-check pipeline with the Z3 SMT solver, using solver counterexamples to iteratively guide invariant refinement. We use Code2Inv benchmark, which provides C programs along with their formal preconditions and postconditions. On this benchmark of 133 tasks, our framework achieves 100% coverage (133 out of 133), outperforming the previous best of 107 out of 133, while requiring only 1-2 model proposals per instance and 14-55 seconds of wall-clock time. These results demonstrate that LLMs possess latent logical reasoning capabilities which can help automate loop invariant synthesis. While our experiments target C-specific programs, this approach should be generalizable to other imperative languages.

The Ordinal Folding Index (OFI) is a new, fully computable yard-stick that measures how many rounds of self-reference a statement, protocol or position must unfold before its truth or outcome stabilises. By turning this abstract 'fold-back' depth into a single ordinal number, OFI forges a direct link between areas that are usually studied in isolation: the closure stages of fixed-point logics, the time-to-win values of infinite parity games, and the ordinal progressions that calibrate the strength of formal theories. We prove that OFI refines all classical game-theoretic and logical metrics while remaining algorithmically enumerable, supply a polynomial-time approximation scheme on finite arenas, and show how the index coincides exactly with the length of the shortest winning strategy in the associated evaluation game. Alongside the theory we outline five open problems from the completeness of the computable-ordinal spectrum to the possibility of 'compressing' deep self-reference that chart a research programme at the intersection of computer-aided logic, algorithmic game theory and ordinal analysis. OFI thus invites game theorists and logicians alike to view infinite play, transfinite induction and reflective reasoning through a single, intuitive lens, opening common ground for techniques.