License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.1
URN: urn:nbn:de:0030-drops-134141
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13414/
Go to the corresponding OASIcs Volume Portal

Rosu, Grigore

Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)

pdf-format:
OASIcs-FMBC-2020-1.pdf (0.2 MB)

Abstract

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 will 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 language specification.

BibTeX - Entry

@InProceedings{rosu:OASIcs:2020:13414,
  author =	{Grigore Rosu},
  title =	{{Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{1:1--1:1},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bruno Bernardo and Diego Marmsoler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13414},
  URN =		{urn:nbn:de:0030-drops-134141},
  doi =		{10.4230/OASIcs.FMBC.2020.1},
  annote =	{Keywords: Blockchain, K Framework}
}

Keywords: Blockchain, K Framework
Collection: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue Date: 2020
Date of publication: 11.12.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI