arXiv subjects

Bart Jacobs

Publications and source records attributed to Bart Jacobs.

At least 19 recordsLinked to original sources

arXiv2026

Verifying the Rust Standard Library

Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign's effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.

cs.LO↗

arXiv2026

Counting Votes with Multisets

A multiset is a 'set' in which elements may occur multiple times. These structures are ideal for expressing the outcome of an election, for instance of the form 60 'yes' and 40 'no'. Moreover, multisets are a useful datatype in vote counting algorithms. This will be illustrated in three different forms of vote counting, known as: 'instant-runoff', 'De Borda', and 'single transferrable vote'. The relevant abstract properties of multisets are: (1) they form a (free) commutative monoid, and (2) they form a functor, and (3) also a monad. This paper illustrates how such categorical properties can be put to good use in deriving and expressing election outcomes. The emphasis is not on the (elementary) category theory involved, but on its application in voting systems.

math.GM↗

arXiv2026

Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions

The Rust programming language is famous for its strong ownership regime: at each point, each value is either exclusively owned, exclusively borrowed through a mutable reference, or borrowed as read-only through one or more shared references. These rules, known as Rust's pointer-aliasing rules, are exploited by the Rust compiler to generate more efficient machine code, and enforced by Rust's static type system, except inside unsafe blocks. In this paper, we present our work in progress towards the first program logic for modularly verifying that Rust programs that use unsafe blocks comply with the pointer-aliasing rules.

cs.PL↗

arXiv2026

Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring

VeriFast is a leading tool for the modular formal verification of correctness properties of single-threaded and multi-threaded C and Rust programs. It verifies a program by symbolically executing each function in isolation, exploiting user-annotated preconditions, postconditions, and loop invariants written in a form of separation logic, and using a separation logic-based symbolic representation of memory. However, the tool itself, written in roughly 30K lines of OCaml code, has not been formally verified. Therefore, bugs in the tool could cause it to falsely report the correctness of the input program. We here report on an early result extending VeriFast to emit, upon successful verification of a Rust program, a Rocq proof script that proves correctness of the program with respect to a Rocq-encoded axiomatic semantics of Rust. This significantly enhances VeriFast's applicability in safety-critical domains. We apply hinted mirroring: we record key information from VeriFast's symbolic execution run, and use it to direct a replay of the run in Rocq.

cs.PL↗

arXiv2025

A Fresh Look at Bivariate Binomial Distributions

Binomial distributions capture the probabilities of `heads' outcomes when a (biased) coin is tossed multiple times. The coin may be identified with a distribution on the two-element set {0,1}, where the 1 outcome corresponds to `head'. One can also toss two separate coins, with different biases, in parallel and record the outcomes. This paper investigates a slightly different `bivariate' binomial distribution, where the two coins are dependent (also called: entangled, or entwined): the two-coin is a distribution on the product {0,1} x {0,1}. This bivariate binomial exists in the literature, with complicated formulations. Here we use the language of category theory to give a new succint formulation. This paper investigates, also in categorically inspired form, basic properties of these bivariate distributions, including their mean, variance and covariance, and their behaviour under convolution and under updating, in Laplace's rule of succession. Furthermore, it is shown how Expectation Maximisation works for these bivariate binomials, so that mixtures of bivariate binomials can be recognised in data. This paper concentrates on the bivariate case, but the binomial distributions may be generalised to the multivariate case, with multiple dimensions, in a straightforward manner.

math.PR↗

arXiv2025

Compositional Inference for Bayesian Networks and Causality

Inference is a fundamental reasoning technique in probability theory. When applied to a large joint distribution, it involves updating with evidence (conditioning) in one or more components (variables) and computing the outcome in other components. When the joint distribution is represented by a Bayesian network, the network structure may be exploited to proceed in a compositional manner -- with great benefits. However, the main challenge is that updating involves (re)normalisation, making it an operation that interacts badly with other operations. String diagrams are becoming popular as a graphical technique for probabilistic (and quantum) reasoning. Conditioning has appeared in string diagrams, in terms of a disintegration, using bent wires and shaded (or dashed) normalisation boxes. It has become clear that such normalisation boxes do satisfy certain compositional rules. This paper takes a decisive step in this development by adding a removal rule to the formalism, for the deletion of shaded boxes. Via this removal rule one can get rid of shaded boxes and terminate an inference argument. This paper illustrates via many (graphical) examples how the resulting compositional inference technique can be used for Bayesian networks, causal reasoning and counterfactuals.

cs.LO↗

arXiv2025

Discrete Boltzmann distributions via multisets and their coefficients

This paper investigates the combinatorics that gives rise to the Boltzmann probability distribution. Despite being one of the most important distributions in physics and other fields of science, the mathematics of the underlying model of particles at different energy levels is underexplored. This paper gives a reconstruction, using multisets with fixed sums as mathematical representations. Counting (the coefficients of) such multisets gives a general description of binomial, trinomial, quadrinomial etc.\ coefficients, here called N-nomials. These coefficients give rise to multiple discrete Boltzmann distributions that are linked to explanations in the physics literature.

math.PR↗

arXiv2025

VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs

VeriFast is one of the leading tools for semi-automated modular formal program verification. A central feature of VeriFast is its support for higher-order ghost code, which enables its support for expressively specifying fine-grained concurrent modules, without the need for the later modality. We present the first formalization and soundness proof for this aspect of VeriFast's logic, and we compare it both to Iris, a state-of-the-art logic for fine-grained concurrency which features the later modality, as well as to some recent proposals for Iris-like reasoning without the later modality.

cs.PL↗

arXiv2025

An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model

We propose an approach for modular verification of programs that use relaxed-consistency atomic memory access primitives and fences. The approach is sufficient for verifying the core of Rust's Atomic Reference Counting (ARC) algorithm. We first argue its soundness, when combined with a simple static analysis and admitting an open sub-problem, with respect to the C20 memory consistency model. We then argue its soundness, even in the absence of any static analysis and without any assumptions, with respect to YC20, a minor strengthening of XC20, itself a recently proposed minor strengthening of C20 that rules out out-of-thin-air behaviors but allows load buffering. In contrast to existing work on verifying ARC, we do not assume acyclicity of the union of the program-order and reads-from relations. We define an interleaving operational semantics, prove its soundness with respect to (Y)C20's axiomatic semantics, and then apply any existing program logic for fine-grained interleaving concurrency, such as Iris.

cs.PL↗

arXiv2024

A Simple Formal Language for Probabilistic Decision Problems

Probabilistic puzzles can be confusing, partly because they are formulated in natural languages - full of unclarities and ambiguities - and partly because there is no widely accepted and intuitive formal language to express them. We propose a simple formal language with arrow notation ($\gets$) for sampling from a distribution and with observe statements for conditioning (updating, belief revision). We demonstrate the usefulness of this simple language by solving several famous puzzles from probabilistic decision theory. The operational semantics of our language is expressed via the (finite, discrete) subdistribution monad. Our broader message is that proper formalisation dispels confusion.

cs.LO↗

arXiv2024

Drawing with Distance

Drawing (a multiset of) coloured balls from an urn is one of the most basic models in discrete probability theory. Three modes of drawing are commonly distinguished: multinomial (draw-replace), hypergeometric (draw-delete), and Polya (draw-add). These drawing operations are represented as maps from urns to distributions over multisets of draws. The set of urns is a metric space via the Kantorovich distance. The set of distributions over draws is also a metric space, using Kantorovich-over-Kantorovich. It is shown that these three draw operations are all isometries, that is, they exactly preserve the Kantorovich distances. Further, drawing is studied in the limit, both for large urns and for large draws. First it is shown that, as the urn size increases, the Kantorovich distances go to zero between hypergeometric and multinomial draws, and also between P\'olya and multinomial draws. Second, it is shown that, as the drawsize increases, the Kantorovich distance goes to zero (in probability) between an urn and (normalised) multinomial draws from the urn. These results are known, but here, they are formulated in a novel metric manner as limits of Kantorovich distances. We call these two limit results the law of large urns and the law of large draws.

cs.LO↗

arXiv2024

Getting Wiser from Multiple Data: Probabilistic Updating according to Jeffrey and Pearl

In probabilistic updating one transforms a prior distribution in the light of given evidence into a posterior distribution, via what is called conditioning, updating, belief revision or inference. This is the essence of learning, as Bayesian updating. It will be illustrated via a physical model involving (adapted) water flows through pipes with different diameters. Bayesian updating makes us wiser, in the sense that the posterior distribution makes the evidence more likely than the prior, since it incorporates the evidence. Things are less clear when one wishes to learn from multiple pieces of evidence / data. It turns out that there are (at least) two forms of updating for this, associated with Jeffrey and Pearl. The difference is not always clearly recognised. This paper provides an introduction and an overview in the setting of discrete probability theory. It starts from an elementary question, involving multiple pieces of evidence, that has been sent to a small group academic specialists. Their answers show considerable differences. This is used as motivation and starting point to introduce the two forms of updating, of Jeffrey and Pearl, for multiple inputs and to elaborate their properties. In the end the account is related to so-called variational free energy (VFE) update in the cognitive theory of predictive processing. It is shown that both Jeffrey and Pearl outperform VFE updating and that VFE updating need not decrease divergence - that is correct errors - as it is supposed to do.

cs.LO↗

arXiv2023

A flexible specification approach for verifying total correctness of fine-grained concurrent modules

A well-established approach to proving progress properties such as deadlock-freedom and termination is to associate obligations with threads. For example, in most existing work the proof rule for lock acquisition prescribes a standard usage protocol by burdening the acquiring thread with an obligation to release the lock. The fact that the obligation creation is hardcoded into the acquire operation, however, rules out non-standard clients e.g. where the release happens in a different thread. We overcome this limitation by instead having the blocking operations take the obligation creation operations required for the specific client scenario as arguments. We dub this simple instance of higher-order programming with auxiliary code Sassy. To illustrate Sassy, we extend HeapLang, a simple, higher-order, concurrent programming language with erasable code and state. The resulting language gets stuck if no progress is made. Consequently, we can apply standard safety separation logic to compositionally reason about termination in a fine-grained concurrent setting. We validated Sassy by developing (non-foundational) machine-checked proofs of representative locks -- an unfair Spinlock (competitive succession), a fair Ticketlock (direct handoff succession) and the hierarchically constructed Cohortlock that is starvation-free if the underlying locks are starvation-free -- against our specifications using an encoding of the approach in the VeriFast program verifier for C and Java.

cs.PL↗

arXiv2023

Overdrawing Urns using Categories of Signed Probabilities

A basic experiment in probability theory is drawing without replacement from an urn filled with multiple balls of different colours. Clearly, it is physically impossible to overdraw, that is, to draw more balls from the urn than it contains. This paper demonstrates that overdrawing does make sense mathematically, once we allow signed distributions with negative probabilities. A new (conservative) extension of the familiar hypergeometric ('draw-and-delete') distribution is introduced that allows draws of arbitrary sizes, including overdraws. The underlying theory makes use of the dual basis functions of the Bernstein polynomials, which play a prominent role in computer graphics. Negative probabilities are treated systematically in the framework of categorical probability and the central role of datastructures such as multisets and monads is emphasised.

math.PR↗

arXiv2023

Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)

Bounded proofs are convenient to use due to the high degree of automation that exhaustive checking affords. However, they fall short of providing the robust assurances offered by unbounded proofs. We sketch how completeness thresholds serve as a bridge, allowing us to derive unbounded guarantees from bounded proofs. Using a bubble sort implementation as example, we demonstrate that a bounded proof only needs to consider a few specific inputs to yield unbounded guarantees.

cs.LO↗

arXiv2023

Pearl's and Jeffrey's Update as Modes of Learning in Probabilistic Programming

The concept of updating a probability distribution in the light of new evidence lies at the heart of statistics and machine learning. Pearl's and Jeffrey's rule are two natural update mechanisms which lead to different outcomes, yet the similarities and differences remain mysterious. This paper clarifies their relationship in several ways: via separate descriptions of the two update mechanisms in terms of probabilistic programs and sampling semantics, and via different notions of likelihood (for Pearl and for Jeffrey). Moreover, it is shown that Jeffrey's update rule arises via variational inference. In terms of categorical probability theory, this amounts to an analysis of the situation in terms of the behaviour of the multiset functor, extended to the Kleisli category of the distribution monad.

cs.LO↗

arXiv2023

Certifying C program correctness with respect to CH2O with VeriFast

VeriFast is a powerful tool for verification of various correctness properties of C programs using symbolic execution. However, VeriFast itself has not been verified. We present a proof-of-concept extension which generates a correctness certificate for each successful verification run individually. This certificate takes the form of a Coq script which, when successfully checked by Coq, removes the need for trusting in the correctness of VeriFast itself. The Coq script achieves this by applying a chain of soundness results, allowing us to prove correctness of the program with regards to the third-party CH2O small step semantics for C11 by proving correctness in terms of symbolic execution in Coq. This proof chain includes two intermediate auxiliary big step semantics, the most important of which describes VeriFast's interpretation of C. Finally, symbolic execution in Coq is implemented by transforming the exported AST of the program into a Coq proposition representing the symbolic execution performed by VeriFast itself.

cs.LO↗

arXiv2023

Verifying C++ Dynamic Binding

We propose an approach for modular verification of programs written in an object-oriented language where, like in C++, the same virtual method call is bound to different methods at different points during the construction or destruction of an object. Our separation logic combines Parkinson and Bierman's abstract predicate families with essentially explicitly tracking each subobject's vtable pointer. Our logic supports polymorphic destruction. Virtual inheritance is not yet supported. We formalised our approach and implemented it in our VeriFast tool for semi-automated modular formal verification of C++ programs.

cs.PL↗