William Denman

Name:	William Denman
Affiliation:	University of Cambridge
E-mail:	(only provided to users who are logged into talks.cam)
Last login:	Thu Oct 09 08:42:06 +0000 2014

Public lists managed by William Denman

• Computer Laboratory Automated Reasoning Group Lunches

Talks given by William Denman

Obviously this only lists talks that are listed through talks.cam. Furthermore, this facility only works if the speaker's e-mail was specified in a talk. Most talks have not done this.

• Introductory meeting
• Formal Verification of Analog Designs using MetiTarski

Talks organised by William Denman

This list is based on what was entered into the 'organiser' field in a talk. It may not mean that William Denman actually organised the talk, they may have been responsible only for entering the talk into the talks.cam system.

• Interfacing and improving proof tools
• CakeML: A Verified Implementation of ML
• A Verified Bignum Implementation in x86-64 Machine Code
• Diabelli: a framework for heterogeneous reasoning
• Extending deforestation
• On the Strength of Owicki-Gries for Resources
• Discovery of Invariants through Automated Theory Formation
• Zeno: An automated theorem prover for functional programs
• Work in progress: a prototype refactoring tool based on a mechanically-verified core
• How do I know my GPU or multicore floating point computations are correct?
• Title to be confirmed
• Using the Cambridge ARM model to verify the concrete machine code of seL4
• Validating QBF Validity in HOL4
• Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers
• Rough-and-ready proof reconstruction
• The Strategy Challenge in Computer Algebra