We consider a more general formulation of Bit-vector Finite Automata (BFAs) that we introduced in our iFM'22 paper. The extended formalism accounts for both ‘may call’ and ‘must call’ properties (the latter is new to this paper). In particular, we show how the main ideas of our approach can be accommodated to support ‘must call’ logic. We provide full proofs of correctness for the extended BFAs and the extension of the experimental evaluation.

Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.

Session types enable the static verification of message-passing programs. A session type specifies a channel’s protocol as sequences of messages. Prior work established a minimality result: every process typable with standard session types can be compiled down to a process typable using minimal session types: session types without sequencing construct. This result justifies session types in terms of themselves; it holds for a higher-order session 𝜋-calculus, where values are abstractions (functions from names to processes). This paper establishes a minimality result but now for the session 𝜋-calculus, the language in which values are names and for which session types have been more widely studied. This new minimality result for the session 𝜋 -calculus can be obtained by composing existing results. We develop associated optimizations and enhancements of this result, and establish its static and dynamic correctness.

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.

We study a minimal formulation of session types without sequencing. We show how to forgoing sequencing in types, and only with sequencing on the level of processes, we can recover the usual theory of session types. More specifically, we show an encoding of regular session types into minimal session types, grounded in Parrow’s decomposition of a pi-calculus process into a collection of trios. We show that the correctness of the decomposition using a form of a session-typed bisimulation.