Moshe Y. Vardi(Rice University)
Title:Program Verification: a 70+-Year History
Abstract:
The year 2019 sees the 70th anniversary to Alan Turing's 1949 paper, "Checking a Large Routine" and the 50th anniversary of Tony Hoare's paper, "An Axiomatic Basis for Compuer Programming". In the latter paper, Hoare stated: "When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics."
In this talk, I will review the history of this vision, describing the obstacles, the controversies, and progress milestones. I will conclude with the description of both impressive progress and dramatic failures exhibited over the past few years.
Biography:
Moshe Y. Vardi is University Professor and the George Distinguished Service Professor in Computational Engineering at Rice University. He is the recipient of several awards, including the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Knuth Prize, the IEEE Computer Society Goode Award, and the EATCS Distinguished Achievements Award. He is the author and co-author of over 650 papers, as well as two books. He is a Guggenheim Fellows as well as fellow of several societies, and a member of several academies, including the US National Academy of Engineering and National Academy of Science. He holds seven honorary doctorates. He is a Senior Editor of the Communications of the ACM, the premier publication in computing.
Kokichi Futatsugi (JAIST, JP)
Title:Advances of Proof Scores in CafeOBJ
Abstract:
Critical flaws continue to exist at the level of domain, requirement, and/or design specification, and specification verification, i.e., to prove a specification has desirable properties, is still one of the most important challenges in software engineering.
CafeOBJ is an executable algebraic specification language system that can be used for specification verification by writing proof scores. Domain/requirement/design engineers using CafeOBJ are expected to construct proof scores for getting reliable specifications. CafeOBJ is a sister language of OBJ and proof scores have been brought up by the OBJ/CafeOBJ community.
Specification verification is theorem proving where the specification is a set of axioms and the desirable properties are theorems. Fully automatic theorem proving often fails to convey an understanding of proof, and one should seek to make optimal use of the respective abilities of humans and computers, so that computers do the tedious formal calculations, and humans do the high level planning. Proof scores intend to meet these goals by hiding the detailed calculations done by machines while revealing the proof plan created by humans.
This talk explains advances of proof scores for specification verification in CafeOBJ.
Biography:
Kokichi Futatsugi is a Professor Emeritus at Japan Advanced Institute of Science and Technology (JAIST), Nomi, Ishikawa, Japan. He worked for JAIST from 1993 to 2017 as a Professor, a Dean of School, an Adviser of President, and a Specially Assigned Professor. Before getting a professorship at JAIST, he worked for Electrotechnical Laboratory (ETL, the national research institute for electronics and informatics) from 1975 to 1993 as a Researcher, a Section Chief, and a Chief Researcher of Institute. He worked for SRI International (Stanford Research Institute) in California as an International Fellow from 1983 to 1984 and designed and implemented OBJ algebraic specification language system. From around mid nineties he headed several research projects funded by Japanese Government for developing CafeOBJ algebraic specification language system. Professor Futatsugi served for many international scholarly activities including a Program Committee Chair of 20th International Conference of Software Engineering (ICSE 1998) and an Associate Editor of ACM Transactions of Software Engineering and Methodology (TOSEM) from 1995 to 2002. He is an Honorary Member of Japan Society of Software Science and Technology since 2019.
Hai Jin (Huazhong University of Science and Technology, CN)
Title:The Research and Practice of Containers System
Abstract:
Container technology has been widely used in various real-world situations, like cloud platforms, CI/CD, and DevOps. By enabling a layered image system and OS-level virtualization, container technology can provide agile deployment and isolate execution environment for applications. However, existing container systems fail to support containers efficiently, flexibly, and securely. On the one hand, coarse-grained image management makes the deployment and update of applications time-consuming when the corresponding images need to be delivered in network. On the other hand, shared OS kernel may arise resource contention and flexibility and security issues. This talk shows our research and practice of container systems. Specifically, I will introduce approaches of image management for fast container deployment and OS Kernel isolation for secure and high-performance container execution environment.
Biography:
Hai Jin is a Cheung Kung Scholars Chair Professor of computer science and engineering at Huazhong University of Science and Technology (HUST) in China. Jin received his PhD in computer engineering from HUST in 1994. In 1996, he was awarded a German Academic Exchange Service fellowship to visit the Technical University of Chemnitz in Germany. Jin worked at The University of Hong Kong between 1998 and 2000, and as a visiting scholar at the University of Southern California between 1999 and 2000. He was awarded Excellent Youth Award from the National Science Foundation of China in 2001. Jin is the chief scientist of National 973 Basic Research Program Project of Virtualization Technology of Computing System, and Cloud Security.
Jin is a Fellow of IEEE, Fellow of CCF, and a life member of the ACM. He has co-authored more than 20 books and published over 900 research papers. His research interests include computer architecture, virtualization technology, cluster computing and cloud computing, peer-to-peer computing, network storage, and network security.