Massimo Bartoletti

Lug 182016

Upcoming Seminar

July 22, 15.00 (Aula C)
Palazzo delle Scienze - Cagliari

Andrea Bracciali

SICSA Lecturer - University of Stirling (UK)

Abstract. Decentralised smart contracts represent the next step in the development of protocols that support the interaction of independent players without the presence of a coercing authority. Based on protocols à la BitCoin for digital currencies, smart contracts are believed to be a potentially enabling technology for a wealth of future applications. The validation of such an early developing technology is as necessary as it is complex. In this paper we combine game theory and formal models to tackle the new challenges posed by the validation of such systems.
 Scritto da in 18 luglio 2016  seminari  Commenti disabilitati su Seminar: Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods
Lug 022016
Upcoming Seminar
July 7, 15.00 (Aula C) Palazzo delle Scienze - Cagliari
Alceste Scalas
Imperial College London
Abstract. Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style (CPS) protocols, studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.
 Scritto da in 2 luglio 2016  seminari  Commenti disabilitati su Seminar: Lightweight session programming in Scala
Giu 132016

1 - Introduction to cryptocurrencies and smart contracts

15.4.2016 h12.00 - Lab M (Massimo Bartoletti)

2 - Introduction to smart contracts in Ethereum

22.4.2016 h12.00 - Lab M (Tiziana Cimoli)  --  Slides

3 - Incentives for smart contracts

29.4.2016 h11.00 - Lab M (Nicola Atzei) -- Slides

4 - Vulnerabilities of Bitcoin

6.5.2016 h11.00 - Lab M (Stefano Lande) -- Slides

5 - Analysis of the Bitcoin protocol

13.5.2016 - h11.00 - Lab M (Alessandro Sebastian Podda) -- Slides

6 - Ethereum in depth

20.5.2016 h11.00 - Lab M (Nicola Atzei and Tiziana Cimoli) -- Slides

7 - A survey of frameworks for smart contracts

27.5.2016 h11.00 - Lab M (Livio Pompianu) -- Slides

 Scritto da in 13 giugno 2016  seminari  Commenti disabilitati su Seminars series: cryptocurrencies and smart contracts
Set 022015
Compliance and subtyping in timed session types September 7, 15.45 (Aula F) Palazzo delle Scienze - Cagliari Maurizio Murgia
Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari
Abstract. We propose an extension of binary session types, to formalise timed communication protocols between two participants at the endpoints of a session. We introduce a decidable compliance relation, which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. We then show a sound and complete technique to decide when a timed session type admits a compliant one, and if so, to construct the least session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results. We exploit our theory to design and implement a message-oriented middleware, where distributed modules with compliant protocols can be dynamically composed, and their communications monitored, so to guarantee safe interactions.
 Scritto da in 2 settembre 2015  seminari  Commenti disabilitati su Seminar: Compliance and subtyping in timed session types
Set 022015

Upcoming Seminar

On the decidability of honesty and of its variants

September 3, 11.30 (Aula F)
Palazzo delle Scienze - Cagliari

Massimo Bartoletti
Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari

We address the problem of designing distributed applications which require the interaction of loosely-coupled and mutually distrusting services. In this setting, services can use contracts to protect themselves from unsafe interactions with the environment: when their partner in an interaction does not respect its contract, it can be blamed (and punished) by the service infrastructure. We extend a core calculus for services, by using a semantic model of contracts which subsumes various kinds of behavioural types. In this formal framework, we study some notions of honesty for services, which measure their ability to respect contracts, under different assumptions about the environment. In particular, we find conditions under which these notions are (un)decidable.
 Scritto da in 2 settembre 2015  Senza categoria  Commenti disabilitati su Seminar: On the decidability of honesty and of its variants
Ago 192015
Multiparty testing preorders August 25, 15.00 (Aula F) Palazzo delle Scienze - Cagliari
Hernan Melgratti
Department of Computing, Faculty of Science, University of Buenos Aires
Abstract. Variants of the must testing approach have been successfully applied in Service Oriented Computing for analysing the compliance between (contracts exposed by) clients and servers or, more generally, between two peers. It has however been argued that multiparty scenarios call for more permissive notions of compliance, because partners usually do not have full coordination capabilities. We propose two new testing preorders, which are obtained by restricting the set of potential observers. For the first preorder, called uncoordinated, we allow only sets of parallel observers that use different parts of the interface of a given service and have no possibility of intercommunication. For the second preorder, that we call independent, we instead rely on parallel observers that perceive as silent all the actions that are not in the interface of interest. We have that the uncoordinated preorder is coarser than the classical must testing preorder and finer than the independent one. We also provide a characterisation in terms of decorated traces for both preorders: the uncoordinated preorder is defined in terms of must-sets and Mazurkiewicz traces, while the distributed one is described in terms of classes of filtered traces that only contain designated visible actions and must-sets.
credits | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929
note legali | privacy

Nascondi la toolbar