Professional service
Organiser:
 2015
 Imperial Concurrency
Workshop
Program committee member:
 2018
 Designer Track, Design Automation Conference (DAC)
FieldProgrammable Logic and
Applications (FPL)
 2017
 FieldProgrammable Logic and
Applications (FPL)
 2016
 Reengineering for Parallelism in Heterogeneous Parallel
Platforms (RePara)
Tiny Transactions on Computer Science (TinyTOCS)
 2015
 Automated Verification of Critical Systems (AVoCS)
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)
Artifact evaluation committee member:
 2015
 ACM Symp. on Principles of Programming Languages (POPL)
External reviewer for the following conferences and journals:
 2018

IEEE Int. Symp. on FieldProgrammable Custom Computing Machines (FCCM)
IEEE Int. Conf. on Software Testing, Verification and Validation (ICST)
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
 2017

ACM/SIGDA Int. Symp. on FieldProgrammable Gate Arrays (FPGA)
Journal of Supercomputing
Symp. on Parallelism in Algorithms and Architectures (SPAA)
 2016

ACM Trans. on Computational Logic (TOCL)
ACM Trans. on Reconfigurable Technology and Systems (TRETS)
ACM Int. Conf. on ObjectOriented Programming, Systems, Languages, and Applications (OOPSLA)
ACM Symp. on Principles of Programming Languages (POPL)
ACM Symp. on Principles and Practice of Parallel Programming (PPoPP)
 2015

Int. Conf. on Computer Aided Verification (CAV)
Europ. Symp. on Programming (ESOP)
ACM Symp. on Principles of Programming Languages (POPL)
ACM Symp. on Principles and Practice of Parallel Programming (PPoPP)
 2014

Joint Int. Conf. on Rewriting and Typed Lambda Calculi (RTATLCA)
Int. Conf. on Runtime Verification (RV)
Static Analysis Symp. (SAS)
 2012

ACM Int. Conf. on Certified Programs and Proofs (CPP)
Int. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS)
Symp. on Parallelism in Algorithms and Architectures (SPAA)
Int. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)
 2011

Int. Conf. on Computer Aided Verification (CAV)
 2010

Europ. Symp. on Programming (ESOP)
ACM/IEEE Symp. on Logic in Computer Science (LICS)
ACM Symp. on Principles of Programming Languages (POPL)
Int. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)
 2009

ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
Teaching
In the 2015/16 and 2016/17 academic years, I was a guest lecturer for the Computer Science
course Models of
Computation at Imperial. My slides on
the Lambda Calculus, and YouTube videos of my
lectures, are available here:
 2015, 2016
 The Lambda Calculus. (pdf, video
1, video
2, video
3)
In the 2014/15 academic year, I was a guest lecturer for the Computer Science
course Separation Logic at Imperial. The slides presented in my lectures are available here:
 18Nov2014
 Ribbon Proofs for Separation Logic. (pdf, 7.3MB)
In the 2013/14 academic year, I was a guest lecturer for the Computer Science course Software Reliability at Imperial. The slides presented in my lectures are available here:
 04Mar2014
 Lecture 16. Verifying heapmanipulating
programs using Separation Logic. (pdf, 2.1MB)
 06Mar2014
 Lecture 17. Verifying
concurrent programs using Rely/Guarantee and Separation Logic. (pdf, 1.6MB)
In the 2013/14 academic year, I was a guest lecturer for the Part II Computer Science course Hoare Logic at Cambridge. The slides presented in my lecture are available here:
 11Feb2014
 Lecture 8. Automatic Verification of GPU kernels. (pdf, 594kB)
I gave a tutorial at the HiPEAC '14 conference about the GPUVerify tool developed here in the Multicore Group at Imperial.
 21Jan2014
 Formal Analysis Techniques for GPU kernels. (pdf, 627kB)
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:
 15Jan2013
 A graphical introduction to Separation Logic (Part I). (pdf  both lectures, 364kB)
 22Jan2013
 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:
 8Feb2011
 Lecture 6. More Separation Logic. (pdf, 1.6MB)
 8Mar2011
 Lecture 14. RelyGuarantee (pdf, 504kB)
 10Mar2011
 Lecture 15. RGSep (pdf, 1MB)
At Cambridge, I supervised several courses:
 Denotational Semantics
 Discrete Mathematics II
 Hoare Logic
 Foundations of Functional Programming
 Prolog
 Semantics of Programming Languages
 Specification and Verification I
 Topics in Concurrency
 Types
I also organised the
Churchill Compsci Talks series.