3 papers
cs.PL2026
The complexity of verifying the release-acquire semantics over register machines
Parosh Abdulla, Elli Anastasiadi, Mohamed Faouzi Atig +2
The Release-Acquire (RA) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed system…
cs.PL2025
Denotational Semantics for Probabilistic and Concurrent Programs
Noam Zilberstein, Daniele Gorla, Alexandra Silva
We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as pr…
cs.LO2025
Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory
Luca Aceto, Antonis Achilleos, Duncan Paul Attard +4
Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its executio…