Program Verification: A 50-Year Retrospective

Moshe Y. Vardi

Rice University

Tony Hoare's seminal paper, "An axiomatic basis for computer programming", was published 50 years ago. The paper has had a profound impact on computing research, inspiring generations of researchers, as well as arousing deep opposition. In this talk, I assess the impact of this paper, describing how recent developments show the paper was at the same time both prophetic and misguided.

The talk is aimed at a general computer-science audience.

Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, the Southeastern Universities Research Association's Distinguished Scientist Award, and the ACM SIGLOG Church Award. He is the author and co-author of over 600 papers, as well as two books: Reasoning about Knowledge and Finite Model Theory and Its Applications. He is a Fellow of the American Association for the Advancement of Science, the American Mathematical Society the Association for Computing Machinery, the American Association for Artificial Intelligence, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds six honorary doctorates. He is currently a Senior Editor of of the Communications of the ACM, after having served for a decade as Editor-in-Chief.

Title:

Evolution of Software Engineering in Industry — challenges and opportunities for Testing.

Abstract:

In the last few decades, the software industry has seen a sea of changes in the mode software is delivered to the consumers. We have transitioned successfully from shrinkwrap software to online services. Rich functionalities are being delivered to the users real-time using online services reducing the time to market. This transition has a profound impact on the type of challenges industry is faced with from the software engineering and testing standpoint. Over the last decade, I have experienced the transition working at companies of varying size and complexity. In this talk, I will highlight the software testing challenges that the industry is facing and the opportunities for innovating new test methodologies.

Adithya Nagarajan is a Senior Engineering Manager at Apple. He has many years of experience developing, testing, and maintaining Enterprise Resource Planning (ERP) solutions, Online services, and E-Commerce. Over the past few years, he has been working on the Apple Maps product, delivering high-quality maps experience to Maps users. He currently leads a large organization responsible for developing testing platforms using large-scale distributed systems, with expertise in computer vision, 3D graphics, performance profiling, and device automation.

Data Intelligence Enables  Intelligent R&D

Abstract： 

Coming to the new era of software application – Agile、Micro-Service、DevOps … the development cycle is shortened but the quality of software should not be compromised. Therefore in the Software industry , the R&D model which include the software architecture itself, the software development process, the software development environment and the company organization are going through Engineering Transforming to facilitate the software development projects stake holders accomplish their tasks effectively and intelligently. This presentation will address the mission from the perspective of a corporate wide R&D competence promoter， which is to provide an intelligent research and development environment that will provide right assistances to the right R&D person at the right time in one shot. During the presentation will also highlight the key enablers of this intelligent R&D mission – build Data Intelligence through data correlation, software traceability and software analytics technologies to conduct the Intelligent Testing.

Bio of Tony Chang:

Tony has served at Nortel from 1987-2007 and Huawei Technology from 2008-Present, during these periods he has been acting as the engineer、manager、 Sr. manager、Direct  or、 Sr. Director、VP and Corporate Test Authority -- led/ guided the teams to be the industry Test Technology leader in the CT domain: build up the company-wide Test Automation Platform,、Lab Standardization/Dynamic Resource Allocation、industry leading Test Methodologies 、Standardized Test Case Framework、 Customer Solution Integration Automations/Ecosystem and Intelligent R&D.  As of now, Tony is driving company’s goal on open collaboration and joint innovation in the industry Standard committee (TMForum , ETSI) to  promote and share the advanced trends and concept of Test technology and Delivery method. He is currently acting as the Huawei US RDCC lab leader、Corporate Chief Test Expert and got the honor of “Asia America Executive of the Year” in 2017.

Automated Fault Finding and Fixing with Sapienz at Facebook

Abstract:

Sapienz designs system tests that simulate user interactions with mobile apps. It automatically finds app issues, localizes, tracks and triages them to developers. SapFix automatically generates patches for specific bugs. This talk will cover how Sapienz is deployed at a large scale at Facebook, including its continuous integration with Facebook's development process, fault signal boosting with Infer static analysis and SapFix patch generation. This talk contains joint work of the whole Sapienz team and its partners and collaborators at Facebook.

Bio of Ke Mao:

Ke Mao is a software engineer at Facebook where he works on Sapienz for automated fault finding and fixing. Sapienz has been deployed at Facebook since October 2017. It aut  omatically designs, executes, and reports results of tests on the Facebook's Android and iOS apps that are used by over a billion users worldwide every day. Sapienz grew out of his PhD research work. He co-founded the start-up Majicke with Prof. Mark Harman and Dr. Yue Jia and later the co-founders moved to Facebook in February 2017. He holds a PhD degree in computer science from University College London (UCL) and an MS in computer science from the Institute of Software, Chinese Academic of Sciences (ISCAS).