Upcoming paper (to appear in LMCS)
Massimo Bartoletti, Alceste Scalas, Emilio Tuosto and Roberto Zunino
Abstract. We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises made, or not. Type safety guarantees that a typeable process is honest - that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidable, and it allows to safely approximate the honesty of processes using either synchronous or asynchronous communication.
Bitcoin and Blockchain Technologies
August 31st 2016
Cottrell building 4B96 - University of Stirling
An open, international, one-day of study, brainstorming and networking opportunities for interested researchers and stakeholders.
Courant Institute of Mathematical Sciences and School of Medicine
New York University
Mt Sinai School of Medicine
Beyond the keynote talk, the day will comprise short introductions by the participants on ongoing research, initiatives, and groups focussing on BTC/BC. Networking opportunities and discussion on possible grants and projects will also be part of the day. We will be targeting H2020 and other EU initiatives, as well as UK funders and US-EU possible partnerships.
09.30 Coffee & registration
Welcome and round of short introductions
10.20 Daniela Bolle, Research Office, University of Stirling
Funding opportunities + questions/comments/insights.
(including COST, ITN, Global Challenge, …)
11.00 Invited talk: Bud Mishra, New York University.
12.00 Lunch (Room 2B87)
13.15 Short talks
Andrea Bracciali, University of Stirling
Validation of decentralised Smart Contracts through game theory and formal methods
Massimo Bartoletti, TCS group University of Cagliari
Martin Chapman, King's College
Andrea Pinna, Agile group University of Cagliari
Federico Pintore, University of Trento
Simon Dobson, University of St Andrews
Can blockchains help make science must trustworthy?
15.30 Coffee break
16.00 Discussion on grant applications
A networking session aimed at exploring the possibility of collaborations and funding
applications, with a specific focus on selected EU and National programmes.
Participation is free, but registration required for organisational purposes. Please register at:
preferably not later than 28th August!
Accommodation can be booked on campus or in nearby structures. Please see
for useful information about traveling to and staying in Stirling, as well as on-campus accommodation (please note that the event precedes the CIBB2016 conference, which is an independent event, but you can enquire for accommodation through the conference channels).
Abstract: this talk will focus on Bit-Coins and BlockChain Technologies and their implications for Privacy, Anonymity, Data Science, Finance and Market Micro-structure.
Topics: Information Asymmetry, Signaling Games, Risks and Deception – Signaling Games On the Internet (& Biology) – Costly Signaling, Block Chains, Verifiers and Recommenders – Circulating Money via Signaling Games – Value-Storing Money via Signaling Games – Case Studies: Bit-Coins, Dark Web, Silk Road and MtGox – Data Science and Finance
Slides: available here.
Bud Mishra is a professor of computer science and mathematics at NYU's Courant Institute of Mathematical Sciences, professor of computer science and engineering at NYU’s Tandon School of Engineering, professor of human genetics at Mt. Sinai School of Medicine, and a professor of cell biology at NYU School of Medicine. Prof. Mishra has a degree in Physics from Utkal University, in Electronics and Communication Engineering from IIT, Kharagpur, and MS and PhD degrees in Computer Science from Carnegie-Mellon University. He has industrial experience in Computer and Data Science (brainiad, Genesis Media, Pypestream, Tartan Laboratories, and ATTAP), Finance (Instadat, Tudor Investment and PRF, LLC), Robotics and Bio- and Nanotechnologies (Bioarrays, InSilico, Seqster, Abraxis, MRTech, and OpGen). He is the author of a textbook on algorithmic algebra and more than two hundred archived publications. He has advised and mentored more than 35 graduate students and post-docs in the areas of computer science, robotics and control engineering, applied mathematics, finance, biology and medicine. He is a fellow of IEEE, ACM and AAAS, a Distinguished Alumnus of IIT- Kharagpur, and a NYSTAR Distinguished Professor. From 2003-2006, he held adjunct professorship at Tata Institute of Fundamental Research in Mumbai, India. From 2001-04, he was a professor at the Watson School of Biological Sciences, Cold Spring Harbor Lab; currently he is a QB visiting scholar at Simons Center for Quantitative Biology, Cold Spring Harbor Lab.
Upcoming paper (to be presented at WISE 2016)
Massimo Bartoletti, Stefano Lande, and Alessandro Massa
Abstract. User reputation is a crucial indicator in social networks, where it is exploited to promote authoritative content and to marginalize spammers. To be accurate, reputation must be updated periodically, taking into account the whole historical data of user activity. In big social networks like Twitter and Facebook, these updates would require to process a huge amount of historical data, and therefore pose serious performance issues. We address these issues in the context of Twitter, by studying a technique which can update user reputation in constant time. This is obtained by using an arbitrary ranking algorithm to compute user reputation in the most recent time window, and by combining it with a summary of historical data. Experimental evaluation on large datasets show that our technique improves the performance of existing ranking algorithms, at the cost of a negligible degradation of their precision.
July 22, 15.00 (Aula C)
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.
SICSA Lecturer - University of Stirling (UK)
July 7, 15.00 (Aula C)
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.
A short course on behavioural contracts was given at the BETTY Summer School 2016, held in Limassol (Cyprus) from June 27 to July 1, 2016. The teaching material is included below.
1. Contracts as games
2. Timed session types
3. Contract-oriented computing
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
6.5.2016 h11.00 - Lab M (Stefano Lande) -- Slides
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
27.5.2016 h11.00 - Lab M (Livio Pompianu) -- Slides
Blockchain technologies have a strong transformational potential. Bitcoin and other cryptocurrencies, currently the most well-known blockchain based applications, enable the possibility of a distributed management of secure transactions amongst “anonymous” parties, i.e. payments in this case, without the need of a centralised validation authority.
However, a much wider range of possible applications are emerging for blockchains. Examples include smart contracts, i.e. enforceable, fully-decentralised agreements between independent peers; the possibility of enforcing fairness in distributed protocols, so-far unachieved; and the availability of a public Big Data set of transactions to be explored by Data Scientists to unveil useful knowledge.
Although highly volatile, Bitcoin has a capitalisation of 7 billion USD (doubled over the last year) and is receiving a lot of interest from private companies and institutional partners, noticeably the EU parliament (April 2016). The success of Bitcoin has fostered the development of alternative cryptocurrencies and frameworks for smart contracts, notably Ethereum with a market capitalization of 700 million USD.
Despite their diffusion and resilience in practice (the only successful attacks to Bitcoin have been, so far, standard frauds), foundations of blockchain technologies have still to be fully understood, and no fully satisfactory scientific validation of their correctness and security exist yet. Difficulties arise from many sources at different levels: the complexity of the decentralised, probabilistic and multi-layer structure of a blockchain, the scattered documentation, the relevance of human and economical aspects on the management and stability of the system, and the globalised dimension of the applications, which also brings into play political aspects, to cite but a few.
Even considering all the issues, challenges and currently open problems, blockchain technologies are clearly deemed to have a strong impact on society, empowering people, companies and institutions to directly manage some of their interactions, akin to the empowering made by Internet in terms of direct access to knowledge and communication. Analogously to what happened with Internet, which for instance is nowadays accepted as a trusted commerce medium, blockchain technologies need to be deeply understood and validated before the breakthrough changes that they will enable can become a trusted component of our society.
Read the full discussion at: https://ec.europa.eu/futurium/en/content/how-much-bitcoin-worth-and-why
Upcoming paper (to be presented at FORTE 2016)
Nicola Atzei and Massimo Bartoletti
Abstract. Modern distributed applications are typically obtained by integrating new code with legacy (and possibly untrusted) third-party services. Some recent works have proposed to discipline the interaction among these services through behavioural contracts. The idea is a dynamic discovery and composition of services, where only those with compliant contracts can interact, and their execution is monitored to detect and sanction contract breaches.
In this setting, a service is said honest if it always respects the contracts it advertises. Being honest is crucial, because it guarantees a service not to be sanctioned; further, compositions of honest services are deadlock-free. However, developing honest programs is not an easy task, because contracts must be respected even in the presence of failures (whether accidental or malicious) of the context.
In this paper we present Diogenes, a suite of tools which supports programmers in writing honest Java programs. Through an Eclipse plugin, programmers can write a specification of the service, verify its honesty, and translate it into a skeletal Java program. Then, they can refine this skeleton into proper Java code, and use the tool to verify that its honesty has not been compromised by the refinement.
Upcoming paper (to appear in JLAMP)
Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira
Abstract. Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.