Details: Speakers, titles and abstracts
Morning session: Blockchain
ALGORAND: The Blockchain for the Borderless Economy
By: Silvio Micali of MIT
Blockchains stand to revolutionize the way democratic societies and traditional economies operate. As currently implemented, however, blockchains are aspirational and cannot achieve their enormous potential.
Algorand is an alternative, democratic, and efficient blockchain. Its consensus protocol dispenses with ‘proof of work’ and ‘miners’; requires only a negligible amount of computation; guarantees that its transaction history does not ‘fork’ (i.e., guarantees the finality of all transactions); and allows for consensual evolution, so as to enable the community to meet its future needs without any ‘hard forks.’
Algorand is the first blockchain that is simultaneously secure, scalable and truly decentralized, and its deep roadmap will greatly augment the value of its platform.
Based in Boston and founded by cryptography pioneer and Turing award winner Silvio Micali,
Session: Blockchain Infrastructure
Tezos: self-amendment, formal verification and research time scales
by Michel Mauny, Board member, Tezos
Tezos' upgradability, through its self-amendment capabilities, and its strong links with formal verification allow it to interact with research on different time scales. In this presentation, I will recall the main features of the Tezos blockchain, and discuss its links with the world of research.
Affiliation: Nomadic Lacs <nomadic-labs.com>
Michel is Chief Scientific Officer at Nomadic Labs, on leave from Inria (the French National Institute for Computer Science and Applied Mathematics), where he was a senior researcher and more recently Chief Executive Officer of the Inria Foundation. Michel is also a member of the Board of the Tezos Foundation. Michel’s scientific interests are mainly in the fields of programming languages: design, implementation, semantics, static analysis, and type systems. After his Ph.D. at Paris-Diderot University, Michel joined Inria in 1985 and worked on programming languages with the research group that designed and developed OCaml, the functional programming language used to implement Tezos, and the Coq proof assistant. From 1989 to 2005, Michel led the research team that further developed OCaml, and he has been a Professor of Computer Science at Ensta-ParisTech from 2005 to 2016.
Plutus — Functional Smart Contracts on Cardano
by Manuel Chakravarty, Blockchain Language Architect, IOHK
Functional programming and blockchains are a match made in heaven! The immutable and reproducible nature of distributed ledgers is mirrored in the semantic foundation of functional programming. Nevertheless, most existing blockchains
In this talk, I will outline how IOHK’s Plutus team combines programming language theory, functional programming, and domain-specific languages to develop a radically new approach to blockchain contract development. This not only helps us to reason about safety and security
Manuel M T Chakravarty has published extensively on programming languages, compilers, and high-performance computing. He contributed to both the design and implementation of the Haskell programming language as well as several Haskell tools and open source libraries. With the increasing adoption of functional programming in industry, he shifted his focus to unlocking new application areas for functional programming and helping development teams reap the benefits of modern programming language technology. He is currently co-leading the research-driven Plutus smart contract language team at IOHK.
Founded in 2015 by Charles Hoskinson and Jeremy Wood, IOHK is a technology company committed to using peer-to-peer innovations to provide financial services to the three billion people who don’t have them. We are an engineering company that builds cryptocurrencies and blockchains for academic institutions, government entities
Session: Blockchain Ecosystem
Turning A Vehicle Into An Economic Platform
by Michael Huth, CTO, XAIN
Consumer expectations and fierce market competition have led to margins becoming increasingly thinner for manufacturers of consumer and commercial vehicles. These actors realize now more than ever, that the value of their goods no longer rests on the basic functions they provide, but rather on the types and qualities of user experiences they can offer: extra horse-power on demand, ability to share usage, selling data streams to third parties - to name a few.
Increasingly, manufacturers are exploring ways to capture this value by turning a vehicle into a mini-economic platform that facilitates value exchange. Usage of that platform must be controlled so that value creation and consumption are neither
Our R&D in policy-based access control, distributed ledger technology, and embedded systems has led to the development of FROST Technology for fully programmable sharing ecosystems and flexible usage control on a vehicle’s
Michael Huth is CTO of XAIN AG and a Professor of Computer Science in the Department of Computing at Imperial College London. He is a Diplom-Mathematiker (TU Darmstadt, Germany), obtained his
XAIN AG was incorporated in February 2017 in Germany. It is a Berlin-based startup that does research in cybersecurity and machine learning. XAIN prevailed over 120+ competitors to win the 1st Porsche Innovation Contest in 2017. XAIN successfully completed a pilot with Porsche in March 2018 that brought blockchain technology into a Porsche Panamera.
Session: Verified Smart Contracts
Formal Design, Implementation
and Verification of Blockchain Languages
Many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses of the underlying blockchain programming languages or virtual machines. The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal specification. We demonstrate the feasibility of the proposed approach by applying it to two blockchains, Ethereum and Cardano.
Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the president and CEO of Runtime Verification, Inc (RV). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering
Modularity for Accurate Static Analysis of Smart Contracts
by Mooly Sagiv:
Static code analysis is a useful technique for finding bugs in
I will describe a new way to perform accurate static analysis (ASA) of smart contracts in order to identify bugs and prove their absence before the code is deployed. ASA guarantees that all bugs are reported and that all errors are real. ASA operates on bytecode programs which enables to check the code even when the source is not available.
Scalability of the method is guaranteed by verifying each of the contracts with respect to the requirements of other contracts.
Mooly Sagiv is a CEO of
Verified Oak smart contracts
by Bas Spitters
Concordium's Oak/Acorn smart contract language is a member of the ML-family of programming languages. This language is functional and has no run-time exceptions, thus avoiding a large class of bugs. We have embedded this language in the Coq proof assistant. This allows us to give mathematical proofs about Oak smart contracts. For instance, we have shown that an Oak implementation of the infamous TheDAO contract is not vulnerable to a large class of attacks.
Bas Spitters is associate professor computer science at Aarhus University, WP leader in the Concordium Blockchain Research Center and
Concordium's Chief Scientific Advisor formal verification and smart contracts. He holds a
mathematics feasible at
The Concordium blockchain network (https://www.concordium.com/) is the first business-friendly ID/KYC-enabled blockchain ledger. Features