ion and Completeness for Real-Time Maude Peter Csaba ¨Olveczky a,b and Jos´e Meseguer b a Department of Informatics, University of Oslo b Department of Computer Science, Universi...
We introduce the idea of optimisation validation, which is to formally establish that an instance of an optimising transformation indeed improves with respect to some resource mea...
David Aspinall, Lennart Beringer, Alberto Momiglia...
We propose a compositional technique for efficient verification of networks of parallel processes. It is based on an automatic analysis of LTSs of individual processes (using a f...
Reasoning about graph and model transformation systems is an important means to underpin model-driven software engineering, such as Model-Driven Architecture (MDA) and Model Integ...
Abstract Machine Describing Event Structure Composition Claudia Faggian and Mauro Piccolo 1 ,2 ,3 Dipartimento di Matematica Pura e Applicata – PPS Universit´a di Padova – Par...
We study, from the expressiveness point of view, the impact of synchrony in the communication primitives that arise when combining together some common and useful programming feat...
We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching of binding bigraphs. Our results pave the way f...
Lars Birkedal, Troels Christoffer Damgaard, Arne J...
The paper reports on the foundations and experimental results with a model checker for component connectors modelled by networks of channels in the calculus Reo. The specificatio...
We discuss the tensions between intensionality and extensionality of spatial observations in distributed systems, showing that there are natural models where extensional observati...