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 Computer Laboratory - John Wickerson
John Wickerson
Technische Universität Berlin , supported by a University of Cambridge Kurt Hahn Trust scholarship from the DAAD . My work focuses on software verification. I'm currently interested in diagrammatic proof systems for Rely-Guarantee reasoning and separation logic.
From 2008 to 2012, I was a PhD student in the Programming, Logic and Semantics Group , supervised by Matthew Parkinson and Glynn Winskel .
From July to October 2011, I was an intern at European Microsoft Innovation Center in Aachen, where I worked on the VCC project. From April to July 2010, I was an intern at Microsoft Research Cambridge , where I was supervised by Sir Tony Hoare .
email Firstname.Surname@cl.cam.ac.uk
Concurrent Verification for Sequential Programs . tech report ) Ribbon proofs . entry , proof document , html version ) Ribbon proofs for separation logic . Mike Dodds and Matthew Parkinson . ESOP 2013 .preprint , publisher's version ) Ribbon proofs for separation logic .Mike Dodds and Matthew Parkinson . LICS 2012 .preprint , slides )Unifying Models of Data Flow .Tony Hoare and John Wickerson. preprint , publisher's version )Explicit Stabilisation for Modular Rely-Guarantee Reasoning .Mike Dodds and Matthew Parkinson . ESOP 2010 .preprint , publisher's version , tech report , Isabelle proofs )
The ribbonproofs package .package , pdf manual )
Ribbon proofs and dynamically-scoped quantifiers .pdf )
20-Mar-2013 Ribbon Proofs for Separation Logic .ESOP 2013 .pdf , 11.2MB)27-Jun-2012 Ribbon Proofs for Separation Logic .LICS 2012 .pdf , 1.3MB)15-Apr-2011 Ribbon Proofs for Separation Logic .Dublin Concurrency Workshop .pdf , 2.7MB)25-Oct-2010 Separation Logic and Graphical Models .Semantics Lunch .1-up pdf , 1.2MB; 6-up pdf , 1.5MB)06-Jul-2010 A dataflow model of concurrency, communication and weak memory .Cambridge Concurrency Workshop .1-up pdf , 213kB; 6-up pdf , 225kB)09-Mar-2010 Explicit Stabilisation for modular Rely-Guarantee Reasoning .pdf , 1.2MB) 25-Nov-2009 Verifying malloc .Northern Concurrency Workshop .1-up pdf , 938kB; 6-up pdf , 893kB)26-Oct-2009 Verifying malloc using RGSep and 'Explicit
Stabilisation' . Semantics Lunch . pdf , 5.3MB) 13-May-2009 Local Rely-Guarantee Reasoning . Program Verification reading group .pdf , 616kB) 04-Feb-2009 Automatic verification of C programs using the BLAST software model checker . Program Verification reading group .pdf , 892kB)
In the 2012/13 academic year, I was a guest lecturer for the graduate course Quality Assurance of Embedded Systems at TU Berlin. The slides presented in my lectures are available here:
15-Jan-2013 A graphical introduction to Separation Logic (Part I). (pdf - both lectures , 364kB) 22-Jan-2013 A graphical introduction to Separation Logic (Part II).
In the 2010/11 academic year, I was a lecturer for the MPhil course Programming Logics and Software Verification . The slides presented in my lectures are available here:
8-Feb-2011 Lecture 6. More Separation Logic. (pdf , 1.6MB)
8-Mar-2011 Lecture 14. Rely-Guarantee (pdf , 504kB)
10-Mar-2011 Lecture 15. RGSep (pdf , 1MB)
Supervising
In the 2011/12 academic year, I supervised the following
Computer Science Tripos courses:
Denotational Semantics
Discrete Mathematics II
Hoare Logic
In previous years I have supervised:
Foundations of Functional Programming
Prolog
Semantics of Programming Languages
Specification and Verification I
Topics in Concurrency
Types
I supervise for Churchill College , where I also organise the Churchill Compsci Talks series.
And finally...
I have a personal blog at johnwickerson.wordpress.com .