Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

Address: [go: Go Back, main page]

---

Remove Scripts Accept Cookies Show Images Show Referer Rotate13 Base64 Strip Meta Strip Title Session Cookies

Michael J. C. Gordon Professor of Computer Assisted Reasoning The University of Cambridge Computer Laboratory Room FE19, William Gates Building 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK office: 01223 334627, mobile: 07774 017428, fax: 01223 334678 @ email: mjcg cl.cam.ac.uk   Show Hide everything

Hide Past research

• Why higher order logic is a good formalism for specifying and verifying hardware
• Mechanizing programming logics in higher order logic
• From LCF to HOL: a short history
• State Transition Assertions (STAs)
• Combining set theory and type theory
• Verilog HDL
• Comparing HOL and PVS
• PROSPER: Proof and Specification Assisted Design Environments
• Christopher Strachey: recollections of his influence
• Formal Specification and Verification of ARM6
• Directions in Formal and Semi-Formal Verification
• Fully Expansive Proof and Algorithmic Verification
• HolBddLib, HolSatLib, puzzleTool
• Deep embedding of Accellera PSL (IBM Sugar 2.0) in HOL
• Programming combinations of deduction and BDD-based symbolic calculation
• STRL Annual Distinguished Seminar
• Invited talk at CAV 2003
• Strachey Lecture
• PSL Semantics in Higher Order Logic (contribution to DCC 2004)
• Translating HOL to hardware (FAQ)
• Linking the HOL4 and ACL2 proof systems
• Mechanically Proving Hoare Formulae (talk at event celebrating Tony Hoare's 75th birthday)
• The MITB project
• Linking ACL2 and HOL (talk given at 2014 ACL2 workshop in Vienna)
• Tactics for mechanized reasoning (invited contribution to a special issue of Phil. Trans. R. Soc. Lond. A)
• The unforeseen evolution of theorem proving in ARM processor verification (talk at Swansea University, 28th April 2015)

Hide Past teaching

• Temporal Logic and Model Checking
• Hoare Logic
• Notes for a talk to PhD students starting in October 2014
• Notes for a talk given to potential PhD students on November 12, 2013
• Programming Logics and Software Verification (discontinued)
• Specification and Verification I (replaced by Hoare Logic after 2010)
• Specification and Verification II (replaced by Temporal Logic and Model Checking 2010)
• Short talk given to new PhD students on the 2008 Induction Day
• Introduction to Functional Programming (only of historical interest - last taught in 1996!)

Hide Miscellaneous

• Google stuff: ads, alerts, dashboard, data, devices, drive, history, location, permissions
• Google Maps UK, AA Route Planner, Mapquest UK, streetmap.co.uk, Multimap, Mapblast, Mapquest
• Airport taxi services
  1. AirportLynx (good, but parking and waiting may put up costs)
  2. ECS (excellent: used by Computer Lab and MSR)
  3. BATS taxis (never tried, but may be cheap)
• Cambridge University Reporter
• Visitors
• Computer Science Lecture-List timetables
• Term dates
• The Royal Society, and its Fellows
• TTVSI (my talk)
• Seating posture and adjustment of my office chair
• In praise of thumb-operated trackballs and the ergonomic problems of mice
• What has a snow watching lantern got to do with the HOL88 system?
• Avra Cohn's paper The Notion of Proof in Hardware Verification and her unfinished paper Proof Accounts in HOL
• Good advice from Dijkstra and Hoare
• Automated Reasoning Group Old FTP Area for HOL
• HTML tablemaker, table of HTML characters, HTML validator and WikiFAQ FAQ hosting site
• My first (and last) use of Java applets (from 1996 -- may crash your browser)
• University of Cambridge Library catalogues
• Melatonin for jetlag (NYT, April 30, 1997) and Jetlag Calculator
• TechEncyclopedia
• HTML 4.0 symbols
• Automated reasoning group home page
• HOL at SourceForge (contains obsolete material)
• A Himalayan Sunset (memoir written by my late mother)
• What I did as Deputy Head of Department