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