arXiv subjects

Jules Jacobs

Publications and source records attributed to Jules Jacobs.

8 recordsLinked to original sources

arXiv2026

Type-Directed Discretization of Probabilistic Programs (Extended Version)

We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where continuous values are compared against finitely many constants, so exact inference reduces to a discrete problem. Our central technical contribution is a non-local, type-directed analysis that infers where continuous values can be partitioned into finitely many observationally relevant regions, then rewrites sampling and comparison behavior over those regions. We call this transformation Slice. Because this construction is global and type-directed, correctness requires reasoning beyond the local syntax: we formalize the transformation and prove soundness for boolean queries using a coupling-style logical relations argument over operational semantics. As an application, transformed programs can be executed by discrete engines such as Dice, Roulette, and Storm. Our empirical evaluation shows two complementary strengths of Slice when paired with discrete backends: it enables exact inference for challenging continuous programs that lie beyond the reach of previous exact systems, and, on benchmarks where direct comparison is possible, it is competitive with state-of-the-art exact inference systems for continuous programs.

cs.PL↗

arXiv2026

NEST: Network Enforced Session Types (Technical Report)

This paper introduces NEST (Network-Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior work that instruments or wraps application code, we synthesize packet-level monitors that enforce protocols directly in the data plane. We develop algorithms to generate network-level monitors from session types and extend them to handle packet loss and reordering. We implement NEST in P4 and evaluate it on applications including microservice and network-function models, showing that network-level monitors can enforce realistic non-trivial protocols.

cs.PL↗

arXiv2026

Deciding Serializability in Network Systems

We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to some serial execution. SER programs are suitably restricted to make this problem decidable, while still allowing for an unbounded number of concurrent threads of execution, each potentially running for an unbounded number of steps. Building on prior theoretical results, we give the first automated end-to-end decision procedure that either proves serializability by producing a checkable certificate, or refutes it by producing a counterexample trace. We also present a network-system abstraction to which SER programs compile. Our decision procedure then reduces serializability in this setting to a Petri net reachability query. Furthermore, in order to scale, we curtail the search space via multiple optimizations, including Petri net slicing, semilinear-set compression, and Presburger-formula manipulation. We extensively evaluate our framework and show that, despite the theoretical hardness of the problem, it can successfully handle various models of real-world programs, including stateful firewalls, BGP routers, and more.

cs.FL↗

arXiv2025

StacKAT: Infinite State Network Verification

We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and - most importantly - access to a stack with accompanying push and pop operations. By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like NetKAT. We develop a decision procedure for StacKAT program equivalence, based on finite automata. This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs. Finally, we provide an axiomatization of StacKAT equivalence and establish its completeness.

cs.PL↗

arXiv2024

KATch: A Fast Symbolic Verifier for NetKAT

We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification.

cs.PL↗

arXiv2022

Fast Coalgebraic Bisimilarity Minimization

Coalgebraic bisimilarity minimization generalizes classical automaton minimization to a large class of automata whose transition structure is specified by a functor, subsuming strong, weighted, and probabilistic bisimilarity. This offers the enticing possibility of turning bisimilarity minimization into an off-the-shelf technology, without having to develop a new algorithm for each new type of automaton. Unfortunately, there is no existing algorithm that is fully general, efficient, and able to handle large systems. We present a generic algorithm that minimizes coalgebras over an arbitrary functor in the category of sets as long as the action on morphisms is sufficiently computable. The functor makes at most $\mathcal{O}(m \log n)$ calls to the functor-specific action, where $n$ is the number of states and $m$ is the number of transitions in the coalgebra. While more specialized algorithms can be asymptotically faster than our algorithm (usually by a factor of $\mathcal{O}(\frac{m}{n})$), our algorithm is especially well suited to efficient implementation, and our tool Boa often uses much less time and memory on existing benchmarks, and can handle larger automata, despite being more generic.

cs.FL↗

arXiv2021

Paradoxes of Probabilistic Programming

Probabilistic programming languages allow programmers to write down conditional probability distributions that represent statistical and machine learning models as programs that use observe statements. These programs are run by accumulating likelihood at each observe statement, and using the likelihood to steer random choices and weigh results with inference algorithms such as importance sampling or MCMC. We argue that naive likelihood accumulation does not give desirable semantics and leads to paradoxes when an observe statement is used to condition on a measure-zero event, particularly when the observe statement is executed conditionally on random data. We show that the paradoxes disappear if we explicitly model measure-zero events as a limit of positive measure events, and that we can execute these type of probabilistic programs by accumulating infinitesimal probabilities rather than probability densities. Our extension improves probabilistic programming languages as an executable notation for probability distributions by making it more well-behaved and more expressive, by allowing the programmer to be explicit about which limit is intended when conditioning on an event of measure zero.

cs.PL↗

arXiv2020

A magic determinant formula for symmetric polynomials of eigenvalues

Symmetric polynomials of the roots of a polynomial can be written as polynomials of the coefficients, and by applying this to the characteristic polynomial we can write a symmetric polynomial of the eigenvalues $a_{i}$ of an $n\times n$ matrix $A$ as a polynomial of the entries of the matrix. We give a magic formula for this: symbolically substitute $a\mapsto A$ in the symmetric polynomial and replace multiplication by $\det$. For instance, for a $2\times2$ matrix $A$ with eigenvalues $a_{1},a_{2}$, \begin{align*} a_1 a_2^2 +a_1^2 a_2 & =\det(A_1, A_2^2)+ \det(A_1^2, A_2) \end{align*} where $A_i^k$ is the $i$-th column of $A^k$. One may also take negative powers, allowing us to calculate: \begin{align*} a_1a_2^{-1}+a_1^{-1}a_{2} & =\det(A_{1},A_{2}^{-1})+\det(A_1^{-1},A_{2}) \end{align*} The magic method also works for multivariate symmetric polynomials of the eigenvalues of a set of commuting matrices, e.g. for $2\times2$ matrices $A$ and $B$ with eigenvalues $a_1,a_2$ and $b_{1},b_{2}$, \begin{align*} a_1 b_1 a_2^2 + a_1^2a_2b_2 & = \det(AB_{1},A_2^2) + \det(A_1^2,AB_2) \end{align*}

math.CO↗