The work presented here investigates the combination of Kleene algebra with the synchrony model of concurrency from Milner's SCCS calculus. The resulting algebraic structure ...
A formalism for expressing the operational semantics of proof languages used in procedural theorem provers is proposed. It is argued that this formalism provides an elegant way to...
Model programs are high-level behavioral specifications used for software testing and design analysis. Composition of model programs is a versatile technique that, at one end of t...
Abstract. Noting that the usual `propositionally' based way of composing retrenchments can yield many `junk' cases, alternative approaches to composition are introduced (...
K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of configurations, comput...
We present a calculus for tracking equality relationships between values through pairs of bytecode programs. The calculus may serve as a certification mechanism for noninterferenc...
We present a general framework for the analysis of quantitative and qualitative properties of reactive systems, based on a notion of weighted transition systems. We introduce and ...
The aim of the paper is to give a formal compositional semantics for Spiking Neural P systems (SNP systems) by following the Structural Operational Semantics (SOS) approach. A pro...
Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo ...