arXiv subjects

Joost-Pieter Katoen

Publications and source records attributed to Joost-Pieter Katoen.

At least 19 recordsLinked to original sources

arXiv2026

Multiobjective Preexpectation Reasoning for Probabilistic Programs

Probabilistic programs with nondeterminism model planning problems in which a strategy typically resolves the nondeterminism to meet a specification. We study the multiobjective setting, meeting several specifications at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that solve nondeterminism probabilistically. We prove the transformer and synthesis rules sound against an operational Markov decision process (MDP) semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using two case studies.

cs.PL↗

arXiv2026

A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)

This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (IVL) together with a real-valued logic. Our IVL provides a programming-language-style for expressing verification conditions whose validity implies the correctness of a program under investigation. As our focus is on verifying quantitative properties such as bounds on expected outcomes, expected run-times, or termination probabilities, off-the-shelf IVLs based on Boolean first-order logic do not suffice. Instead, a paradigm shift from the standard Boolean to a real-valued domain is required. Our IVL features quantitative generalizations of standard verification constructs such as assume- and assert-statements. Verification conditions are generated by a weakest-precondition-style semantics, based on our real-valued logic. We show that our verification infrastructure supports natural encodings of numerous verification techniques from the literature. With our SMT-based implementation, we automatically verify a variety of benchmarks. To the best of our knowledge, this establishes the first deductive verification infrastructure for expectation-based reasoning about probabilistic programs.

cs.PL↗

arXiv2026

Towards a Deductive Verification Infrastructure for Weighted Programming

Weighted programs extend guarded commands with trace weights drawn from a semiring, or more generally a monoid-module. Varying this algebra gives one programmatic syntax for a variety of quantitative and symbolic models. Weakest-preweighting semantics provides a compositional basis for reasoning about those programs. We present a deductive verification framework based on a weighted assertion language and an intermediate verification language. Its weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally. We prove sound translations of core commands and reusable encodings for various proof rules applying to procedure calls and loops. To facilitate automation, we prove soundness of a quantifier elimination procedure for our assertion language. A prototype in the Caesar verifier checks case studies for probabilistic queueing costs, recursive database provenance with cyclic dependencies, clearance bounds for networks of arbitrary size, and formal-language reasoning about lock-freedom of a compare-and-swap counter.

cs.PL↗

arXiv2026

Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

cs.LO↗

arXiv2026

Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams

Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these quantitative expectations. Their automation has been successful in analysing a variety of discrete probabilistic programs. Key routines in that automation require reasoning about (partially unrolled) loops, however, the logical representation of weakest pre-expectations on such unrollings often explodes. In this paper, we develop typed extended decision diagrams (TEDDs), inspired by various extensions to binary decision diagrams. We demonstrate computing WPs represented as TEDDs, SMT-based pruning to further shrink their representation, and we lift some proof rules to operate on TEDDs. Finally, we demonstrate that TEDDs boost the scalability of deductive probabilistic program verification by orders of magnitudes over the state of the art.

cs.PL↗

arXiv2026

Caesar: A Deductive Verifier for Probabilistic Programs

Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL allows users to express a probabilistic program, its specifications, and proof rules in a programming-language style, so that new proof rules can be easily integrated into the verifier. Caesar translates HeyVL programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes a backend based on probabilistic model checking for a subset of HeyVL. We report on the results of five years of development of Caesar, highlighting its main features and architecture. In particular, we describe recent improvements such as additional proof rules, a model-checking backend, and better diagnostics.

cs.PL↗

arXiv2026

Adversarial Robustness of Time-Series Classification for Crystal Collimator Alignment

In this paper, we analyze and improve the adversarial robustness of a convolutional neural network (CNN) that assists crystal-collimator alignment at CERN's Large Hadron Collider (LHC) by classifying a beam-loss monitor (BLM) time series during crystal rotation. We formalize a local robustness property for this classifier under an adversarial threat model based on real-world plausibility. Building on established parameterized input-transformation patterns used for transformation- and semantic-perturbation robustness, we instantiate a preprocessing-aware wrapper for our deployed time-series pipeline: we encode time-series normalization, padding constraints, and structured perturbations as a lightweight differentiable wrapper in front of the CNN, so that existing gradient-based robustness frameworks can operate on the deployed pipeline. For formal verification, data-dependent preprocessing such as per-window z-normalization introduces nonlinear operators that require verifier-specific abstractions. We therefore focus on attack-based robustness estimates and pipeline-checked validity by benchmarking robustness with the frameworks Foolbox and ART. Adversarial fine-tuning of the resulting CNN improves robust accuracy by up to 18.6 % without degrading clean accuracy. Finally, we extend robustness on time-series data beyond single windows to sequence-level robustness for sliding-window classification, introduce adversarial sequences as counterexamples to a temporal robustness requirement over full scans, and observe attack-induced misclassifications that persist across adjacent windows.

cs.CR↗

arXiv2026

Compositional Reasoning for Probabilistic Automata with Uncertainty

This paper develops an assume-guarantee (AG) framework for the compositional verification of probabilistic automata (PAs) with uncertain transition probabilities. We study parametric probabilistic automata (pPAs), where probabilities are given by polynomial functions over a finite set of real-valued parameters and robust probabilistic automata (rPAs)-a generalisation of interval probabilistic automata (iPAs)-where transition probabilities range over potentially uncountable uncertainty sets. Towards pPAs, an existing AG framework for PAs is lifted to the parametric setting. We establish asymmetric, circular, and interleaving proof rules to enable compositional verification of a broad class of multi-objective queries, encompassing probabilistic reachability properties and parametric expected total rewards. In addition, we introduce a dedicated AG rule for compositional reasoning about parameter monotonicity. For convex rPAs and iPAs with history-dependent (memory-full) nature, we establish sound AG rules via a reduction to infinite PAs. We further show that AG reasoning can not straightforwardly be applied to non-convex rPAs, memoryless (once-and-for-all) nature semantics, and the common interval-arithmetic relaxation of parallel composition. Finally, we develop a simulation-based AG style for pPAs: we define strong simulation and robust-strong simulation relations for pPAs and derive their corresponding proof rules.

cs.LO↗

arXiv2026

Probabilistic Model Checking Taken by Storm

This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and a rich Python-based ecosystem, which makes it easy to integrate in various workflows. This tutorial focuses on Markov decision processes (MDP), which are popular in a variety of fields. It demonstrates the basic workflow, from Python-based modeling, model checking with a variety of properties, to the extraction of policies. Further, it showcases the support for recent topics that focus on different types of uncertainty, such as interval MDP and POMDP, and the ability to quickly implement simple algorithms on top of existing data structures.

cs.SE↗

arXiv2026

Verifying Sampling Algorithms via Distributional Invariants

This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saad et al.'s Fast Loaded Dice Roller. These algorithms have previously resisted formal veri cation due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.

cs.LO↗

arXiv2026

Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)

We present a one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs. The first ingredient is to add a reward-statement to the language. We then define a program transformation applying a monotone function to the cumulative reward of the program. The key idea is that this transformation uses incremental differences in the reward. This simple, elegant approach enables to express e.g., higher moments, threshold probabilities of rewards, the expected excess over a budget, and moment-generating functions. All these objectives can now be analyzed using a single existing approach: probabilistic wp-reasoning. We automated verification using the Caesar deductive verifier and report on the application of the transformation to some examples.

cs.PL↗

arXiv2026

Verification of Robust Multi-Agent Systems

Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, however, transition probabilities are only estimated from data and may therefore be partially unknown or subject to perturbations. In this paper, we study the verification of robust strategies in stochastic multi-agent systems with imperfect information, in which coalitions must satisfy a temporal specification while dealing with uncertain system transitions, partial observation, and adversarial agents. By focusing on bounded-memory strategies, we introduce a robust variant of the model-checking problem for a probabilistic, observation-based extension of Alternating-time Temporal Logic. We characterize the complexity of this problem under different notions of perturbation, thereby clarifying the computational cost of robustness in stochastic multi-agent verification and supporting the use of bounded-memory strategies in uncertain environments.

cs.LO↗

arXiv2026

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)

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. While most of the existing literature focuses on statistical approximation, in this paper we address the problem of mathematically exact inference. To achieve this for programs with loops, we rely on a relatively underexplored type of probabilistic loop invariant, which is linked to a loop's so-called occupation measure. The occupation measure associates program states with their expected number of visits, given the initial distribution. Based on this, we derive the notion of an occupation invariant. Such invariants are essentially dual to probabilistic martingales, the predominant technique for formal probabilistic loop analysis in the literature. A key feature of occupation invariants is that they can take the initial distribution into account and often yield a proof of positive almost sure termination as a by-product. Finally, we present an automatic, template-based invariant synthesis approach for occupation invariants by encoding them as generating functions. The approach is implemented and evaluated on a set of benchmarks.

cs.PL↗

arXiv2026

Quantifier Elimination and Craig Interpolation, Quantitatively

Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order theories such as linear rational arithmetic. What about their applicability in the quantitative setting where formulae evaluate to numbers and quantitative supremum/infimum quantifiers are the natural counterparts of Boolean quantifiers? Applications include establishing quantitative properties of programs, such as bounds on expected outcomes of probabilistic programs featuring nondeterminism, and analyzing the flow of information through programs. In this paper, we present, to the best of our knowledge, the first QE algorithm for possibly unbounded, $\infty$- or $-\infty$-valued, or discontinuous piecewise linear quantities. They are the quantitative counterpart to linear rational arithmetic, and they are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper space complexity bounds. Moreover, we present two applications of our QE algorithm. First, our algorithm yields a quantitative CI theorem: given arbitrary piecewise linear quantities $f$ and $g$ with $f \models g$, both the strongest and the weakest Craig interpolant of $f$ and $g$ are quantifier-free and effectively constructible. Second, we apply our QE algorithm to compute minimal and maximal expected outcomes of loop-free probabilistic programs featuring unbounded nondeterminism.

cs.LO↗

arXiv2025

Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)

This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing slices for (1) error reporting, (2) proof simplification, and (3) preserving successful verification results. By formally defining these different notions on HeyVL, an existing quantitative intermediate verification language (IVL), our concepts (and implementation) can be used to obtain diagnostics for a range of probabilistic programming languages. Slicing for error reporting is a novel notion of error localization for quantitative assertions. We demonstrate slicing-based diagnostics on a variety of proof rules such as quantitative versions of the specification statement and invariant-based loop rules, and formally prove the correctness of specialized error messages and verification hints. We implemented our user diagnostics into the deductive verifier Caesar. Our novel implementation -- called \emph{Brutus} -- can search for slices which do or do not verify, corresponding to each of the three diagnostic notions. For error reporting (1), it exploits a binary search-based algorithm that minimizes error-witnessing slices. To solve for slices that verify (2 and 3), we empirically compare different algorithms based on unsatisfiable cores, minimal unsatisfiable subset enumeration, and a direct SMT encoding of the slicing problem. Our empirical evaluation of Brutus on existing and new benchmarks shows that we can find slices that are both small and informative.

cs.PL↗

arXiv2025

Natural Strategic Ability in Stochastic Multi-Agent Systems

Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, natural strategies are a recently proposed framework striking a balance between the ability of agents to strategize with memory and the model-checking complexity, but until now has been restricted to fully deterministic settings. For the first time, we consider the probabilistic temporal logics PATL and PATL* under natural strategies (NatPATL and NatPATL*, resp.). As main result we show that, in stochastic MAS, NatPATL model-checking is NP-complete when the active coalition is restricted to deterministic strategies. We also give a 2NEXPTIME complexity result for NatPATL* with the same restriction. In the unrestricted case, we give an EXPSPACE complexity for NatPATL and 3EXPSPACE complexity for NatPATL*.

cs.LO↗

arXiv2025

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains

Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with constants. The parameters allow encoding dependencies between transitions, which sets pMCs apart from interval MCs. The verification problem for pMCs asks whether each MC in the corresponding family satisfies a given temporal specification. The state-of-the-art approach for this problem is parameter lifting (PL) -- an abstraction-refinement loop that abstracts the pMC to a non-parametric model analyzed with standard probabilistic model checking techniques. This paper presents two key improvements to tackle the main limitations of PL. First, we introduce generalized parameter lifting (GPL) to lift various restrictive assumptions made by PL. Second, we present a big-step transformation algorithm that reduces parameter dependencies in pMCs and, therefore, results in tighter approximations. Experiments show that GPL is widely applicable and that the big-step transformation accelerates pMC verification by up to orders of magnitude.

cs.LO↗

arXiv2025

Compositional Reasoning for Parametric Probabilistic Automata

We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.

cs.LO↗