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 formalism used to describe temporal properties of real-valued signals in cyber-physical systems.
In mission- and safety-critical domains, specifications often consist of large collections of STL formulas, making consistency checking and requirement analysis a major engineering bottleneck.
Tableau-based satisfiability procedures are a natural way to address this problem.
Two of the authors of this paper contributed to the only existing tree-shaped tableau for bounded discrete-time STL, but we have recently found out that the procedure can return incorrect verdicts for some STL formulas.
In this paper, we pinpoint the flaw in that procedure and present a new tree-shaped tableau that we prove to be sound and complete for bounded discrete-time STL.

On top of this theoretical foundation, we introduce STLSat, an open-source Rust tool that decides the satisfiability of STL formulas, synthesizes concrete witness signals, and extracts unsatisfiable cores with its tableau engine, allowing users to identify inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced first-order logic and satisfiability modulo theories encodings for STL, which allow it to act as a portfolio solver.

We evaluate STLSat on an extended benchmark suite (including STL and Mission-time Linear Temporal Logic formulas) that we release publicly. Across the whole benchmark, the portfolio solver matches or outperforms state-of-the-art tools while preserving 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. 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.