[oss] Prezentare "Smart contracts" - Grigore Rosu (UIUC) - vineri, 22 iunie 2018 - 2PM - PR105

[Razvan Deaconescu]

Salutare.

Vineri 22 iunie 2018, intervalul 14:00-15:00, are loc, în sala PR105,
prezentare din zona blockchain a lui Grigore Rosu, profesor la Universitatea
Urbana-Champaign (UIUC) din Statele Unite. Prezentarea se numește
"Formal Design, Implementation and Verification of Blockchain Languages
and Virtual Machines".

Mai jos este Un scurt abstract și o biografie a lui Grigore.

Vă încurajez sa participați, mai ales dacă vă interesează partea de
securitate, verificare formală sau blockchain.

Răzvan

-----
Title:
Formal Design, Implementation and Verification of Blockchain Languages and Virtual Machines

Abstract:
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. We
also discuss the mathematical foundations underlying our formal
analysis and verification tools, specifically matching logic and the K
framework.

Bio:
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 founder and president of
Runtime Verification, Inc (RV). His research interests encompass both
theoretical foundations and system development in the areas of formal
methods, software engineering and programming languages. Before
joining UIUC in 2002, he was a research scientist at NASA. He obtained
his Ph.D. at the University of California at San Diegoin 2000. He was
offered the CAREER award by the NSF, the Dean's award for excellence
in research by the College of Engineering at UIUC in 2014, and the
outstanding junior award by the Computer Science Department at UIUC in
2005. He won the ASE IEEE/ACM most influential paper award in 2016
(for an ASE 2001 paper that helped shape the runtime verification
field), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE
2016, and OOPSLA 2016, and the best software science paper award at
ETAPS 2002.
-----