976 papers · page 2 of 49
David Monniaux, Helmut Seidl
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…
Duc-Than Nguyen, William Mansky
Malo Revel, Thomas Genet, Thomas P. Jensen
Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh, Mahesh Vishwanathan
Philipp Schröer, Darion Haase, Joost-Pieter Katoen
Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi
Hasti Toossi, Ningning Xie
Toby Ueno, Ankush Das
Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen, David N. Jansen
Han Xu, Di Wang
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi
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…
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford
Beniamino Accattoli
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…
Matteo Acclavio, Giulia Manara, Fabrizio Montesi
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 …
Guillaume Ambal, Ori Lahav, Azalea Raad
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…
Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, Léo Stefanesco
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…
Jérôme Boillot, Jérôme Feret
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…
Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard, Roly Perera
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…
Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski
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…
Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski
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…