The Automated-Reasoning Revolution: From Theory to Practice and Back

Moshe Y. Vardi

Abstract:

For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic automated-reasoning problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design. In this talk I will review this amazing development and show how automated reasoning is now an industrial reality.

I will then describe how we can leverage SAT solving to accomplish other automated-reasoning tasks.  Sampling uniformly at random satisfying truth assignments of a given Boolean formula or counting the number of such assignments are both fundamental computational problems in computer science with applications in software testing, software synthesis, machine learning, personalized learning, and more.  While the theory of these problems has been thoroughly investigated since the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances.  Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees.

Short Bio:

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.

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

Adithya Nagarajan

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.

Short Bio:

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.