BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:DAYLIGHT DTSTART:20080309T020000 RDATE:20080309T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080915T100544Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080916T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080916T103000 DTSTAMP;VALUE=DATE-TIME:20080915T100544Z LAST-MODIFIED;VALUE=DATE-TIME:20080915T100544Z UID:http://calagator.org/events/1250455735 DESCRIPTION:Title: Theorem Proving for Verification \;\n \;\nS peaker: John Harrison \;\n Principal Engineer \;\n Intel \;\n \;\nDate: Tuesday\, September 16th. \;\n 10.30am \;\n \;\nLocation: Galois\, Inc. \;\n 421 SW 6th Ave. Suite 300 \;\n (3rd floor of t he Commonwealth Building) \;\n Portland\, Oregon \;\n&# 13\;\nAbstract: \;\n \;\n The theorem proving approach to verif ication involves modelling a system in a rich formalism such as higher-o rder logic or set theory\, then performing a human-driven interactive co rrectness proof using a proof assistant. In a striking contrast\, techni ques like model checking\, by limiting the user to a less expressive for malism (propositional logic\, CTL etc.)\, can offer completely automated decision methods\, making them substantially easier to use and often mo re productive. \;\n \;\n With this in mind\, why should one be interested in the theorem proving approach? In this tutorial I will expl ain some of the advantages of theorem proving\, showing situations where the generality of theorem proving is beneficial\, allowing us to tackle domains that are beyond the scope of automated methods or providing oth er important advantages. I will talk about the state of the art in theor em proving systems and and give a little demonstration to give an impres sion of what it's like to work with such a system. \;\n \;\nBiogra phical details: \;\n \;\n John Harrison has worked in formal ve rification and automated theorem proving since 1990\, when he joined Mik e Gordon's "\;Hardware Verification Group"\; (HVG) at the Univer sity of Cambridge Computer Laboratory. As well as working on the develop ment of the HOL theorem prover\, he developed a particular interest in t he formalization of real analysis and its application to formal verifica tion of floating-point hardware. His PhD in this area\, "\;Theorem P roving with the Real Numbers"\;\, written under Mike Gordon's superv ision\, won a UK Distinguished Dissertation award and was published as a book. He also redesigned HOL from scratch\, resulting in an alternative version called HOL Light. After completing his PhD research in 1995\, J ohn Harrison spent a very enjoyable year at Abo Akademi University and T urku Centre for Computer Science (TUCS) in Turku\, Finland\, where he wa s a member of Ralph Back's Programming Methods Research Group. Among oth er activities\, he championed the "\;declarative"\; proofs of th e Mizar system and showed how these could be integrated into other theor em-provers\, work subsequently taken up in DECLARE\, Isar and other syst ems. \;\n \;\n John Harrison then returned to Cambridge and wor ked on a formal model of floating-point arithmetic and its application t o the verification of some realistic algorithms for transcendental funct ions. This work attracted the attention of Intel\, and in 1998 John Harr ison joined the company as a Senior Software Engineer (now Principal Eng ineer) specializing in the design and formal verification of mathematica l algorithms. He has formally verified and in many cases designed or red esigned numerous algorithms for mathematical functions including divisio n\, square root and transcendental functions. \;\n \;\n In his limited spare time over the past 10 years\, John Harrison has been worki ng on a book giving a comprehensive introduction to automated theorem pr oving. (http://www.cambridge.org/9780521899574) \;\n \;\nAbout th e Galois Tech Talks. \;\n \;\n Galois (http://galois.com) has b een holding weekly technical seminars for several years on topics from f unctional programming\, formal methods\, compiler and language design\, to cryptography\, and operating system construction\, with talks by many figures from the programming language and formal methods communities.&# 13\;\n \;\n The talks are open and free. If you're planning to att end\, dropping a note to is appreciated\, but not required. If you're i nterested in giving a talk\, we're always looking for new speakers. \ ;\n\n\nTags: galois\, technology\, functional programming\, pdxfunc\n\nI mported from: http://calagator.org/events/1250455735 SUMMARY:Galois Tech Talk: Theorem Proving for Verification LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT END:VCALENDAR