Colloquium Details
Formal Methods at Intel - An Overview
| Author: | John Harrison Intel Corporation |
|---|---|
| Date: | June 28, 2011 |
| Time: | 19:00 |
| Location: | 110 Knight Law Center |
| Host: | Zena Ariola |
Abstract
Since the 1990s, Intel has invested heavily in formal methods, which are now deployed in several domains: hardware, software, firmware, protocols etc. Many different formal methods tools and techniques are in active use, including symbolic trajectory evaluation, temporal logic model checking, SMT-style combined decision procedures, and interactive higher-order logic theorem proving. I will try to give a broad overview of some of the formal methods activities taking place at Intel, and describe the challenges of extending formal verification to new areas and of effectively using multiple formal techniques in combination.
This talk is given as part of the Oregon Programming Languages Summer School. The complete schedule is available at www.cs.uoregon.edu/Activities/summerschool/summer11/schedule.html.