Seong Ju Kang, Korea Post
Grigore Rosu, University of Illinois at Urbana-Champaign
Title : Blockchain-based Postal Services at Korea Post
Seong Ju Kang
President, Korea Post
Bio : Seong Ju Kang has been serving as the President of Korea Post since November 2017. Prior to the present position, he served in various public positions such as Director General of ICT Policy and R&D Bureau, Ministry of Science and ICT (April 2008 to Nov. 2017), Minister-Counselor at the Permanent Delegation of Korea to the OECD (Feb. 2011 to Mar. 2013), Assistant Secretary to the President at the Office of the President (Feb. 2007 to Feb. 2008) and Director of ICT Planning and Coordination, Ministry of Information and Communications (Dec. 1997 to Feb. 2007), mainly covering ICT policy including e-government, cyber security, economic development, government innovation and regional development.
Seong Ju Kang received his MS degree from Syracuse University and PhD degree from Penn State University in public administration and MIS. He also taught at the School of Public Administration at the Catholic University of Korea and Penn State University.
Title : Formal Design, Implementation and Verification of Blockchain Languages
Professor of Computer Science, University of Illinois at Urbana-Champaign
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.
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 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 and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 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), the Runtime Verification test of time award (for an RV 2001 paper), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002.