Invited Speakers
1st Workshop on Formal Methods for Blockchains
hosted by the 3rd Formal Methods World Congress on October 11, 2019 in Porto, Portugal
Ilya Sergey
Ilya Sergey is a tenure-track Associate Professor at Yale-NUS College (Singapore), holding a joint appointment with NUS School of Computing. From November 2015 till October 2018, he was a faculty at the Department of Computer Science of University College London. Prior to joining UCL, from December 2012 to October 2015, he was a postdoc at IMDEA Software Institute. From November 2008 to November 2012, he was a research assistant in the CS Department of KU Leuven, where he obtained his PhD. During his doctoral studies he was a visiting PhD fellow in the Department of Computer Science of Aarhus University and a research intern in the PPT group at MSR Cambridge. He got a MSc degree in Mathematics and CS in 2008 from Dept. of Mathematics and Mechanics of Saint Petersburg State University. Before joining academia he worked as a software developer at JetBrains.
The Scilla Journey: From Proof General to Thousands of Nodes
The Scilla project has started in late 2017 as a 100-lines-of-code prototype implemented in Coq proof assistant. Learning from the mistakes of Ethereum, which had pioneered the area of blockchain-based applications (aka smart contracts), the aim of Scilla was to provide a smart contract language, which is expressive enough to accommodate most of the reasonable use-cases, while allowing for scalable and tractable formal verification and analysis. As such, Scilla has been positioned as an intermediate-level language, suitable to serve as a compilation target and also as an independent programming framework. Two years later, Scilla is now powering the application layer of Zilliqa, the world's first publicly deployed sharded blockchain system. Since its public launch less than a year ago, dozens of unique smart contracts implemented in Scilla have been deployed, including custom tokens, collectibles, auctions, multiplayer games, name registries, atomic token swaps, and many others. In my talk, I will describe the motivation, design principles, and semantics of Scilla, and outline the main use cases and the tools provided by the developer community. I will also present a framework for lightweight verification of Scilla programs, and showcase it with two automated domain-specific analyses. Finally, I will discuss the pragmatic pitfalls of designing a new smart contract language from scratch, and present the future exciting research directions that are enabled by Scilla's take on smart contract design.
The slides of the talk are available here.