We argue in this paper that benchmarking should be complemented by direct measurement of parallelisation overheads when evaluating parallel state-space exploration algorithms. Thi...
Graph transformation units are an approach-independent concept for programming by applying rules and imported transformation units to graphs, starting in an initial and ending in ...
Automatic generation of formal specifications from requirement reduces cost and complexity of formal models creation. Thus, the generated formal model brings the possibility to ca...
Team automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patter...
Maurice H. ter Beek, Fabio Gadducci, Dirk Janssens
We present a graphical semantics for the pi-calculus, that is easier to visualize and better suited to expressing causality and temporal properties than conventional relational se...
Logical frameworks have enjoyed wide adoption as meta-languages for describing deductive systems. While the techniques for representing object languages in logical frameworks are ...
In [24] the authors studied the expressiveness of persistence in the asynchronous -calculus (A) wrt weak barbed congruence. The study is incomplete because it ignores the issue of...
Defining operational semantics for a process algebra is often based either on labeled transition systems that account for interaction with a context or on the so-called reduction ...
Matching systems were introduced by Carbone and Maffeis, and used to investigate the expressiveness of the pi-calculus with polyadic synchronisation. We adapt their definition and...
We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in so...
Sylvain Conchon, Evelyne Contejean, Johannes Kanig...