BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Industrial Use of a Mechanical Theorem Prover - J Strother Moore (
 University of Texas at Austin\; University of Edinburgh)
DTSTART:20170706T100000Z
DTEND:20170706T110000Z
UID:TALK73236@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Several mechanical theorem provers and many&nbsp\; mechanized 
 decision procedures are in routine<br>use in&nbsp\; the computing industry
 .&nbsp\; The complexity of computer&nbsp\; chip designs allow design flaws
  to slip past<br>unaided&nbsp\; human reasoning of even the most<br>talent
 ed designers.<br><br>&nbsp\;Bugs in fabricated<br>chips can cost hundreds 
 of millions&nbsp\; of<br>dollars to fix. So microprocessor companies use&n
 bsp\;<br>mechanized theorem proving to prove that critical parts&nbsp\; of
  designs implement the specified<br>functionality.&nbsp\; In&nbsp\; this t
 alk I will explain how one theorem<br>prover is used&nbsp\; in several com
 panies\,<br>including Intel\, AMD\, Centaur\,&nbsp\; ARM\,<br>Oracle\, and
  Rockwell Collins.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR