HILT 2013             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Formal Methods: An Industrial Perspective

Thursday, November 14, 9:00-10:30am

Jeannette Wing

Abstract

Formal methods research has made tremendous progress since the 1980s when a proof using a theorem prover was worthy of a Ph.D. thesis and a bug in a VLSI textbook was found using a model checker. Now, with advances in theorem proving, model checking, satisfiability modulo theories (SMT) solvers, and program analysis, the engines of formal methods are more sophisticated and are applicable and scalable: to a wide range of domains, from biology to mathematics; to a wide range of systems, from asynchronous systems to spreadsheets; and for a wide range of properties, from security to program termination. In this talk, will present a few Microsoft Research stories of advances in formal methods and their application to Microsoft products and services. Formal methods use, however, is not routine—yet—in industrial practice. So, I will close with outstanding challenges and new directions for research in formal methods.


Created on 29 May 2014;  website comments and corrections to ClydeRoby at ACM.Org