Home

Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vulnerabilities to denial-of-service (DoS) attacks. However, it is non-trivial to generate worst-case inputs for concurrent programs, particularly for resources like memory where the peak cost depends on how processes are scheduled. This article presents the first sound worst-case input generation algorithm for concurrent programs under non-monotone resource metrics like memory. The key insight is to leverage resource-annotated session types and symbolic execution. Session types describe communication protocols on channels in process calculi. Equipped with resource annotations, resource-annotated session types not only encode cost bounds but also indicate how many resources can be reused and transferred between processes. This information is critical for identifying a worst-case execution path during symbolic execution. The algorithm is sound: if it returns any input, it is guaranteed to be a valid worst-case input. The algorithm is also relatively complete: as long as resource-annotated session types are sufficiently expressive and the background theory for SMT solving is decidable, a worst-case input is guaranteed to be returned. A simple case study of a web server's memory usage demonstrates the utility of the worst-case input generation algorithm.

---

Multi-structural (MS) games are combinatorial games that capture the number of quantifiers of first-order sentences. On the face of their definition, MS games differ from Ehrenfeucht-Fraisse (EF) games in two ways: first, MS games are played on two sets of structures, while EF games are played on a pair of structures; second, in MS games, Duplicator can make any number of copies of structures. In the first part of this paper, we perform a finer analysis of MS games and develop a closer comparison of MS games with EF games. In particular, we point out that the use of sets of structures is of the essence and that when MS games are played on pairs of structures, they capture Boolean combinations of first-order sentences with a fixed number of quantifiers. After this, we focus on another important difference between MS games and EF games, namely, the necessity for Spoiler to play on top of a previous move in order to win some MS games. Via an analysis of the types realized during MS games, we delineate the expressive power of the variant of MS games in which Spoiler never plays on top of a previous move. In the second part we focus on simultaneously capturing number of quantifiers and number of variables in first-order logic. We show that natural variants of the MS game do *not* achieve this. We then introduce a new game, the quantifier-variable tree game, and show that it simultaneously captures the number of quantifiers and number of variables. We conclude by generalizing this […]

---

In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical type theory (CTT). The result -- cubical modal type theory (Cubical MTT) -- has the desirable features of both systems. In fact, the whole is more than the sum of its parts: Cubical MTT validates desirable extensionality principles for modalities that MTT only supported through ad hoc means. We investigate the semantics of Cubical MTT and provide an axiomatic approach to producing models of Cubical MTT based on the internal language of topoi and use it to construct presheaf models. Finally, we demonstrate the practicality and utility of this axiomatic approach to models by constructing a model of (cubical) guarded recursion in a cubical version of the topos of trees. We then use this model to justify an axiomatization of L\"ob induction and thereby use Cubical MTT to smoothly reason about guarded recursion.

---

We study the equivalence between eval-readback and eval-apply big-step evaluators in the general setting of the pure lambda calculus. We study `one-step' equivalence (same strategy) and also discuss `big-step' equivalence (same final result). One-step equivalence extends for free to evaluators in other settings (calculi, programming languages, proof assistants, etc.) by restricting the terms (closed, convergent) while maintaining the strategy. We present a proof that one-step equivalence holds when (1) the `readback' stage satisfies straightforward well-formedness provisos, (2) the `eval' stage implements a `uniform' strategy, and (3) the eval-apply evaluator implements a `balanced hybrid' strategy that has `eval' as a subsidiary strategy. The proof proceeds the `lightweight fusion by fixed-point promotion' program transformation on evaluator implementations to fuse readback and eval into the balanced hybrid. The proof can be followed with no previous knowledge of the transformation. We use Haskell 2010 as the implementation language, with all evaluators written in monadic style to guarantee semantics (strategy) preservation, but the choice of implementation language is immaterial. To illustrate the large scope of the equivalence, we provide an extensive survey of the strategy space using canonical eval-apply evaluators in code and big-step `natural' operational semantics. We discuss the strategies' properties, some of their uses, and their abstract machines. We improve the […]

---

A set of configurations $H$ is a home-space for a set of configurations $X$ of aPetri net if every configuration reachable from (any configuration in) $X$ can reach (some configuration in) $H$. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations $X$, $H$, if $H$ is a home-space for $X$. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when $X$ is a singleton and $H$ is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any semilinear set of configurations $H$ we can effectively compute a semilinear set $C$ of configurations, called a non-reachability core for $H$, such that for every set $X$ the set $H$ is not a home-space for $X$ if, and only if, $C$ is reachable from $X$. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.

---