Three Research Vignettes in Memory of Mike Gordon

An Informal Session at FLoC 2018

In Collaboration with the CAV 2018 and ITP 2018 Conferences

LT3, Oxford University Mathematical Institute, 13 July 2018, 16:30-18:00

Mike Gordon (1948 - 2017) was a pioneer of deductive theorem proving and formal hardware verification. An inspirational mentor to generations of research students, his tools and techniques have exerted a huge influence across the field of formal verification. In recognition of his scientific achievements, he was elected to the Royal Society in 1994.

This special, informal session at FLoC 2018 gave colleagues, students, collaborators, and friends of Mike an opportunity to come together for three brief research talks on work he influenced.

Registration was free and open to all participants of FLoC, or others who wish to celebrate the scientific legacy of Mike Gordon. We were delighted that over 70 registered participants came, representing all periods of Mike's scientific career.

Programme

Chair, John Harrison.

16:30-17:00 Tom Melham, Proof Programming from LCF_LSM to Goaled via HOL (slides).

17:00-17:30 Michael Norrish, HOL Developed and HOL Used: Interconnected Stories of Real-World Applications (slides)

17:30-18:00 Magnus Myreen, From Processor Verification Upwards (slides)

FLoC 2018 Logo