Automata models are well-established in many areas of computer science and are supported by a wealth of theoretical results including a wide range of algorithms and techniques to specify and
Smart contracts are pieces of software stored on the blockchain that control the transfer of assets between parties under certain conditions. In this paper we analyze the bahaviour of smart
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types
We identify two important features to enhance the design of communication protocols specified in the pi-calculus, that are linear and static channels, and present a compiler, named GoPi, that maps high level specifications into executable Go programs. Channels declared as linear are deadlock-free, while the scope of static channels, which are bound by a hide declaration, does not enlarge at runtime; this is enforced statically by means of type inference, while specifications do not include annotations. Well-behaved processes are transformed into Go code that supports non-deterministic synchronizations and race-freedom. We sketch two main examples involving protection against message forwarding, and forward secrecy, and discuss the features of the tool, and the generated code. We argue that GoPi can support academic activities involving process algebras and formal models, which range from the analysis and testing of concurrent processes for research purposes to teaching formal languages and concurrent systems.
Petri Nets are a well-known model of concurrency and pro- vide an ideal setting for the study of fundamental aspects in concurrent systems. Despite their simplicity, they still lack a
Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is stan- dard for multiparty session type systems
Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and notifyAll) is notoriously challenging. Not only these primitives affect the scheduling of processes, but also notifications unmatched by
Pomsets are a model of concurrent computations introduced by Pratt. We adopt pomsets as a syntax-oblivious specification model of distributed systems where coordination happens via asynchronous message-passing. In this paper,