ABSTRACT. Software is everywhere, and (almost) everything we do relies on software. But can we actually rely on software? Software bugs are just as old as software, and frequently cause major disruptions, such as the recent CrowdStrike’s outage due to a software update. I will argue that it should be possible to improve this situation by developing program verification tools that can be used efficiently to provide guarantees about programs in different programming languages, and for a wide range of properties. I will outline how we work towards this dream with the VerCors team. In particular, I will discuss some of the recent developments around VerCors on various use cases for program verification.

ABSTRACT. Signal Temporal Logic (STL) is a widely used formalism for specifying temporal properties of real-valued signals generated by cyber-physical systems (CPS). In mission- and safety-critical domains, requirement specifications often comprise large collections of STL formulas, leading to significant challenges in requirement engineering. Ensuring the consistency of such requirements---i.e., verifying that they are not mutually contradictory---can be achieved through tableau-based satisfiability checking methods.

In this paper, we show that an existing tree-shaped tableau method for discrete-time STL with bounded temporal operators is unsound and provide a novel, corrected version of which we prove soundness and completeness. Additionally we introduce STLSat, an efficient Rust implementation of our tableau, that enables users to automatically verify the logical consistency of STL requirement sets, synthesize satisfying example signals, and analyse equivalence and implication relations among formulas. STLSat extends this requirements engineering framework with unsatisfiable core extraction, allowing users to identify minimal inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced First-Order Logic (FOL) and Satisfiability Modulo Theories (SMT) encodings for STL, which allow it to act as a portfolio solver. Experimental evaluations on an extended benchmark suite demonstrate that STLSat matches or outperforms state-of-the-art tools in speed and scalability, while maintaining correctness.

ABSTRACT. Description Logics (DLs) are a family of formal languages used for representing and reasoning about structured knowledge in terms of concepts and their relationships. The expressive power of a DL depends on the constructors available for building complex concepts.

In this work, we investigate subsumption in the restricted description logic FL_⊥reg and the related fragments FL_reg, FL_⊥, and FL_0. These formalisms support value restrictions over role names, where the subscript reg indicates the use of regular expressions over roles.

Subsumption between two concept descriptions in FL_⊥reg and FL_reg is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. These results can be derived either from complexity bounds established for more expressive logics or from algorithms designed for harder reasoning problems.

We reprove the PSpace-completeness result and provide a new proof of ExpTime-completeness for FL_reg and FL_⊥reg with TBoxes via a novel reduction to parity pushdown games. Our algorithm relies only on the constructs available in these logics and may therefore be implemented more easily.

ABSTRACT. First-order logic extended with Henkin quantifiers is not recursively enumerable, even for the simplest Henkin quantifier that is not definable in first-order logic. Despite this, such quantifiers arise naturally in the analysis of partially ordered quantification, motivating partial proof systems suitable for automated reasoning. We present a tableau-based proof system with unification for first-order logic extended by the simplest Henkin quantifier. The system is derived from a second-order function calculus but avoids second-order unification by internalizing dependency structure via side-variable and weak regularity constraints.

ABSTRACT. Substructural logics are defined by dropping some of the structural properties of intuitionistic logic such as commutativity (exchange), contraction, or weakening. Substructural logics with contraction and without weakening can have very high complexity: in particular, FLec, the Full Lambek calculus with exchange and contraction, is complete for the Ackermannian complexity class. Here, `Full' refers to the presence of additive (lattice) connectives; these are used to simulate zero tests in the lower bounding argument. Indeed, Schmitz (2016) showed that its multiplicative fragment Lec has much lower complexity: provability and deduction are 2EXPTIME-complete. In this paper, we investigate the effect of adding the standard modal rules K, 4, and T to this multiplicative setting.

We show that provability in Lec+K and Lec+4 remains in 2EXPTIME by extending Schmitz’s expansive BVASS argument. We also obtain Ackermannian lower bounds for Lec+K deducibility, by constructing a reduction from an expansive counter machine; the main point here is that the K rule can be used to simulate zero tests. Some of these results hold even in the presence of the T rule. Combined with known results, this yields a tight classification: Lec+K(+T) and Lec+4 provability is 2EXPTIME-complete, Lec+K(+T) deducibility is Ackermannian-complete.

ABSTRACT. We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping theorem (OST) in the form of a specific novel precondition. This precondition requires the existence of a dominating function for the martingale expression, which is uniformly integrable; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the run-time of a linear loop, then we can automatically synthesize polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to be continuous and have unbounded support, which is a novel contribution to the field. We implemented and evaluated our method to symbolically compute upper and lower bounds for moments of program variables upon termination.

ABSTRACT. Transition-based generalized Büchi automata (TGBAs) can be substantially more compact than equivalent Büchi automata and they are produced or processed by most state-of-the-art ω-automata tools. Research on complementation algorithms for ω-automata focuses mainly on standard Büchi automata, with a few recent exceptions. We present a complementation construction applicable directly to TGBAs based on the idea of “simple and optimal” Büchi automata complementation by Allred and Ultes-Nitsche. We also provide an upper bound on the size of the complement. The bound is asymptotically better than the upper bounds of other complementation approaches applicable to TGBA. Experimental evaluation shows that on complex TGBAs, our complementation clearly outperforms the complementation processes available in modern tools including Spot and Kofola.

ABSTRACT. Reactive systems interact with their environment and have to satisfy their specifications in all environments also in settings with partial visibility. Researchers have extensively studied settings in which assignments to some input signals are hidden throughout the interaction. We introduce and study {\em blinking synthesis} -- synthesis in settings in which the assignment to all input signals is hidden in some rounds of the interaction. Blinking synthesis is relevant for systems with sensor failures, communication disruptions, or scheduling constraints.

The input to the blinking synthesis problem includes, in addition to a specification language $L_\spec$ over the input and output signals, also a hiding language $L_\H$, describing behaviors that trigger hiding of input signals. The goal is to generate a system that satisfies $L_\spec$ in all environments that hide the assignment to input signals whenever the computation so far is in $L_\H$.

We show that while for LTL specifications the problem is 2EXPTIME-complete, a careful and parameterized analysis reveals it is harder than LTL synthesis: blinking synthesis of EXPTIME-complete for specifications given by deterministic automata and when one of its parameters, namely $L_\spec$ or $L_\H$, is fixed. We study cases where the hiding language $L_\H$ can be synthesized too, aiming to either reduce sensing costs or maintain privacy of the environment.

ABSTRACT. Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZKUNSAT, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZKUNSAT demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability.

Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZKUNSAT without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZKUNSAT on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.

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. Model-theoretic semantics comes with a computational counterpart: to check validity is to search for a countermodel, and tableaux, resolution, and satisfiability solvers make the semantics something one can run. Proof-theoretic semantics --- the younger paradigm in which meaning is given by inferential role rather than by denotation --- has no established counterpart. This paper proposes one: logic programming. We show that Sandqvist's base-extension semantics for intuitionistic propositional logic is executable in a precise sense. Bases are logic programs, and to each formula $\varphi$ we assign a goal $[[\varphi]]$ of a second-order hereditary Harrop language such that $\varphi$ is supported in a base $\mathcal{B}$ exactly when $[[\varphi]]$ is operationally derivable from $\mathcal{B}$ read as a program. The encoding is the Russell--Prawitz translation of the connectives with quantification restricted to atoms, and this restriction is not a limitation but the point: it is what the support clauses themselves demand. The correspondence is exact base by base, not merely at the level of validity, so that intuitionistic validity becomes the success of a single query against the empty program. Logic programming stands to proof-theoretic semantics as tableaux and satisfiability solvers stand to model-theoretic semantics.