EECS Department, UC Berkeley
Title: What Good Are Formal Models? (Slides)
Formal models are central to building confidence in complex software systems. Type systems, interface theories, formal semantics, and concurrent models of computation all augment classical software engineering techniques such as object-oriented design to catch errors and to make software more modular and composable. Every formal model lives within a modeling framework that gives semantics to the model, and many modeling frameworks have been developed that enable rigorous analysis and proof of properties. But every such modeling framework is an imperfect mirror of reality. A computer system operating in the physical world may or may not accurately reflect behaviors predicted by a model, and the model may not reflect behaviors that are critical to correct operation of the software. Software in a cyber-physical system, for example, has timing properties that are rarely represented in formal models. In this talk, I will examine the limitations in the use of models. I will show that two very different classes of models are used in practice, classes that I call “scientific models” and “engineering models.” These two classes have complementary properties, and many misuses of models stem from confusion about which class is being used.
Edward A. Lee is the Robert S. Pepper Distinguished Professor Emeritus in EECS at UC Berkeley. He is the author of several books and more than 300 papers and has delivered more than 170 keynote and other invited talks at venues worldwide. Lee’s research focuses on cyber-physical systems, which integrate physical dynamics with software and networks. His focus is on the use of deterministic models as a central part of the engineering toolkit for such systems. He is the director of iCyPhy, the Berkeley Industrial Cyber-Physical Systems Research Center, and the director of the Berkeley Ptolemy project. From 2005-2008, he served as chair of the EE Division and then chair of the EECS Department at UC Berkeley. He led the development of several influential open-source software packages, notably Ptolemy and its spinoffs. From 1979 to 1982 he was a member of technical staff at Bell Labs in Holmdel, New Jersey. He is a co-founder of BDTI, Inc. and has consulted for a number of other companies. He is a Fellow of the IEEE, was an NSF Presidential Young Investigator, won the 1997 Frederick Emmons Terman Award for Engineering Education, received the 2016 Outstanding Technical Achievement and Leadership Award from the IEEE Technical Committee on Real-Time Systems (TCRTS) and The Berkeley Citation in 2018.
University of Illinois at Urbana-Champaign
Title: Formal Design, Implementation and Verification of Blockchain Languages (Slides)
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 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 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 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.
School of Computing, KAIST, South Korea
Title: Lessons Learned from Automated Analysis of Industrial SW for 15 Years (Slides)
Automated SW analysis techniques such as SW model checking and symbolic execution have been popular in research communities for the last few decades. However, still such techniques are not successfully applied to industrial SW due to lack of trained field engineers, hidden costs to apply these techniques to industrial SW and so on. Thus, to enable technology transfer to industry, collaborated case studies between industry and academia are essential. First, these studies can serve as references for field engineers who want to improve quality of SW by adopting automated analysis techniques. Second, concrete applications of such techniques to industrial SW can guide new research directions to resolve practical limitations of the techniques observed in the studies. In this talk, I will share lessons learned from my 15 years’ experience of applying various automated SW analysis techniques to industrial SW such as Samsung NAND flash memory and smartphones, LG home appliances, and Hyundai automotive SW.
Moonzoo Kim is an associate professor in the School of Computing at KAIST where he leads SW Testing and Verification (SWTV) group. He focuses on automated SW testing and debugging techniques using formal methods such as model checking and concolic testing, and published research results at top SE conferences. Also, he has applied advanced SW analysis techniques to detect many bugs in real-world industrial projects such as Samsung NAND flash memory and smartphones, LG home appliances, and Hyundai automotive SW. He is now leading a NRF-funded research project (Next-Gen. Info. Computing Dev. Program) involving 6 universities for intelligent testing and debugging of multi-lingual full-stack SW. Prof. Kim received his Ph.D. at Univ. of Penn. in 2001. After working as a researcher at Samsung SECUi.COM and POSTECH, he joined the faculty of KAIST in 2006. He has served research communities as a conf. program co-chair (ATVA 2008, VALID 2009), a conf. track co-organizer (ICSE 2020 SE In Practice, ISSTA 2019 workshop co-chair, ICSE 2016 New Faculty Symp., ASE 2015 publication co-chair) and an associated journal editor for STVR and JCSE. He received a best paper award at ICST 2018 and several best paper awards at domestic conf. KCSE and KCC.