Formal Methods at Intel - An OverviewSince 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
Document ID
20100018535
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Harrison, John (INTEL Corp. Hillsboro, OR, United States)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium