Name
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, I 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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2527269.2527291 | HILT |
Keywords | Field | DocType |
industrial perspective,microsoft product,wide range,model checking,microsoft research story,theorem prover,formal methods research,model checker,program analysis,program termination,formal method,satisfiability modulo theories,constraint satisfaction,formal methods,verification,specification,theorem proving | Formal system,Programming language,Program synthesis,Computer science,Automated theorem proving,Formal specification,Program analysis,Formal methods,Formal verification,Satisfiability modulo theories | Conference |
Volume | Issue | ISSN |
33 | 3 | 1094-3641 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeannette M. Wing | 1 | 6429 | 874.60 |