arXiv subjects

Erik Voogd

Publications and source records attributed to Erik Voogd.

5 recordsLinked to original sources

arXiv2026

Correct and Complete Symbolic Execution for Free

Symbolic execution is a powerful technique for program analysis. However, the formal semantics underlying symbolic execution is often developed on an ad-hoc basis and decoupled from the concrete semantics of the programming language. To overcome this issue, we introduce symbolic SOS: a rule format that allows us to simultaneously specify concrete and symbolic operational semantics. We prove that symbolic semantics, when generated from symbolic SOS, is both correct and complete with respect to the corresponding concrete semantics. The approach relies only on an algebraic signature of the source language, and is thus language-independent.

cs.PL↗

arXiv2024

Joint Distributions in Probabilistic Semantics

Various categories have been proposed as targets for the denotational semantics of higher-order probabilistic programming languages. One such proposal involves joint probability distributions (couplings) used in Bayesian statistical models with conditioning. In previous treatments, composition of joint measures was performed by disintegrating to obtain Markov kernels, composing the kernels, then reintegrating to obtain a joint measure. Disintegrations exist only under certain restrictions on the underlying spaces. In this paper we propose a category whose morphisms are joint finite measures in which composition is defined without reference to disintegration, allowing its application to a broader class of spaces. The category is symmetric monoidal with a pleasing symmetry in which the dagger structure is a simple transpose.

cs.PL↗

arXiv2024

Towards a Proof System for Probabilistic Dynamic Logic

Whereas the semantics of probabilistic languages has been extensively studied, specification languages for their properties have received less attention -- with the notable exception of recent and on-going efforts by Joost-Pieter Katoen and collaborators. In this paper, we revisit probabilistic dynamic logic (pDL), a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. Building on dynamic logic, pDL can express both first-order state properties and probabilistic reachability properties. In this paper, we report on work in progress towards a deductive proof system for pDL. This proof system, in line with verification systems for dynamic logic such as KeY, is based on forward reasoning by means of symbolic execution.

cs.LO↗

arXiv2023

Symbolic Semantics for Probabilistic Programs (extended version)

We present a new symbolic execution semantics of probabilistic programs that include observe statements and sampling from continuous distributions. Building on Kozen's seminal work, this symbolic semantics consists of a countable collection of measurable functions, along with a partition of the state space. We use the new semantics to provide a full correctness proof of symbolic execution for probabilistic programs. We also implement this semantics in the tool symProb, and illustrate its use on examples.

cs.PL↗

arXiv2019

Minimal Session Types (Extended Version)

Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols. Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction passing), we prove that every process typable with usual (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types. Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow's results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types.

cs.LO↗