976 papers · page 2 of 49
Max-policy iteration is an approach to computing precise numeric program invariants by successive attempts at resolving maximum operators and reduction to mathematical optimization. Mathematical optimization, though, may be expensive. Here, we show, for max-policy iteration on sy…
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system bas…
Abstract Existing Curry-Howard interpretations of call-by-value evaluation for the $$\lambda $$ λ -calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact th…
Abstract We introduce a novel approach to studying properties of processes in the $$\pi $$ π -calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics …
Abstract Remote Direct Memory Access (RDMA) is a modern technology enabling high-performance inter-node communication. Despite its widespread adoption, theoretical understanding of permissible behaviours remains limited, as RDMA follows a very weak memory model. This paper addres…
Abstract De Nicola and Hennessy’s $$\textsc {must}$$ M U S T -preorder is a liveness preserving refinement which states that a server $$q$$ q refines a server $$p$$ p if all clients satisfied by $$p$$ p are also satisfied by $$q$$ q . Owing to the universal quantification over cl…
Abstract We introduce a new abstract domain for analyzing memory block manipulations, focusing on programs with dynamically allocated arrays. This domain computes properties universally quantified over the value of the loop counters, both for assignments and tests. These properti…
Abstract Charts, figures, and text derived from data play an important role in decision making. But making sense of or fact-checking outputs means understanding how they relate to the underlying data. Even for experts with access to the source code and data sets, this poses a sig…
Abstract Operational game semantics (OGS) is a method for interpreting programs as strategies in suitable games, or more precisely as labelled transition systems over suitable games, in the sense of Levy and Staton. Such an interpretation is called sound when, for any two given p…
Abstract This artifact report is a companion to the ESOP’25 paper An abstract, certified account of operational game semantics [3]. The paper describes the construction of a sound model for an abstract notion of language. The model is built using a semantic technique named Operat…