John Wickerson

People

Current team members

Quentin Corradi, PhD student^† since 2022
Michalis Pardalos, PhD student since 2023

† = jointly with George Constantinides; ‡ = jointly with Alastair Donaldson

Former team members

Ilan Ilumbwe, UROP student, Summer 2024
Benny Liu, UROP student, Summer 2024
Chengsong Tan, postdoc^‡ since 2022
Yann Herklotz, PhD student 2019–2024 ➔ postdoc at EPFL
Jianyi Cheng, PhD student^† 2018–2023 ➔ postdoc at University of Cambridge ➔ assistant professor at University of Edinburgh
Jack Clark, research assistant^‡ 2021–2023
Vasileios Klimis, postdoc^‡ 2021–2023 ➔ lecturer at Queen Mary University of London
Dan Iorga, PhD student^‡ and postdoc 2018–2023 ➔ CPU verification engineer at Qualcomm
Nadesh Ramanathan, PhD student^† and postdoc 2015–2021 ➔ system analyst at Arm Ltd.
Matt Windsor, postdoc^‡ 2018–2021 ➔ postdoc at University of York ➔ software engineer at Anaplan

Collaborators

Selected blog articles

10-Sep-2024: Who checks the equivalence checkers?
09-Sep-2024: Automated feature testing of Verilog parsers using fuzzing
28-Jun-2024: Mix-testing: revealing a new class of compiler bugs
11-May-2024: Cycling from King's Cross to Imperial College London
01-Mar-2024: Verified high-level synthesis – now with hyperblocks!
15-Feb-2024: What is the other Incorrectness logic?
24-Aug-2023: CXL: What's all the fuss about?
27-Jan-2023: Hyphenation: when and why?
05-Dec-2022: Proving the existence of God using a computer
14-Jul-2022: A Squash and a Squeeze – Academic Edition
13-Jun-2022: People of PL: Special Mentoring Edition
18-May-2022: Some reflections on FCCM 2022
30-Mar-2022: The "Cluedo" effect in randomised testing
27-Aug-2021: High-level synthesis, but correct
03-Jul-2021: Understanding the memory semantics of multi-threaded CPU/FPGA programs
09-Jun-2021: Introducing C4: the C Compiler Concurrency Checker
07-May-2021: Fuzzing High-Level Synthesis Tools
18-Sep-2020: A translation puzzle
19-Aug-2020: People of PL: Derek Dreyer
18-Jun-2020: People of PL: Ron Garcia
03-Jun-2020: People of PL: Mike Hicks
26-May-2020: People of PL: Alexandra Silva
21-May-2020: Diagrams for composing compilers
27-Feb-2020: Highlights from FPGA 2020
19-Feb-2020: New names for odd and even functions
22-Nov-2019: Fuzzing FPGA synthesis tools
14-Nov-2019: A plot twist, part II: In praise of scatter plots
12-Nov-2019: A plot twist: Drawing better graphs in PL papers
04-Oct-2019: Loop invariants – where should we put them?
05-Sep-2019: Modulo scheduling with rational initiation intervals
08-Aug-2019: How to draw block diagrams
16-Feb-2019: A wordless proof
29-Jun-2018: Greatest Hits of PLDI 2018
6-May-2018: What is the difference between latency and throughput?
4-May-2018: Greatest Hits of FCCM 2018
5-Mar-2018: Concurrency-aware scheduling for high-level synthesis

Peer-reviewed papers, articles, and book chapters

DVCon 2024: Michalis Pardalos, Alastair F. Donaldson, Emiliano Morini, Laura Pozzi, and John Wickerson. Who checks the checkers? Automatically finding bugs in C-to-RTL formal equivalence checkers. In Design and Verification Conference, 2024.
[ pdf ]
FUZZING 2024: Quentin Corradi, John Wickerson, and George A. Constantinides. Automated feature testing of Verilog parsers using fuzzing (registered report). In International Fuzzing Workshop @ ISSTA, 2024.
[ pdf ]
OOPSLA 2024: Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, and John Wickerson. Mix testing: Specifying and testing ABI compatibility of C/C++ atomics implementations. Proc. ACM on Programming Languages, (OOPSLA), 2024.
[ pdf ]
PLDI 2024: Yann Herklotz and John Wickerson. Hyperblock scheduling for verified high-level synthesis. Proc. ACM on Programming Languages, (PLDI), 2024.
[ DOI | magazine feature | press | blog | pdf ]
ICSE-NIER 2024: Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, and Azalea Raad. Challenges in empirically testing memory persistency models. In IEEE/ACM Int. Conf. on Software Engineering: New Ideas and Emerging Results, 2024.
[ DOI | pdf ]
EuroSys 2024: Jack Clark, Alastair F. Donaldson, John Wickerson, and Manuel Rigger. Validating database system isolation level implementations with version certificate recovery. In European Conference on Computer Systems, 2024. Best Paper award.
[ DOI | pdf ]
ESOP 2024: Azalea Raad, Ori Lahav, John Wickerson, Piotr Balcer, and Brijesh Dongol. Intel PMDK transactions: Specification, validation and concurrency. In European Symposium on Programming, 2024.
[ pdf ]
TSE 2023: Dan Iorga, John Wickerson, and Alastair F. Donaldson. Simulating operational memory models using off-the-shelf program analysis tools. IEEE Trans. on Software Engineering, 2023.
[ DOI ]
TC 2023: Jianyi Cheng, Estibaliz Fraca, John Wickerson, and George A. Constantinides. Balancing static islands in dynamically scheduled circuits using continuous Petri nets. IEEE Trans. on Computers, 2023.
[ DOI | pdf ]
TRETS 2023: Jianyi Cheng, Lana Josipović, John Wickerson, and George A. Constantinides. Parallelising control flow in dynamic-scheduling high-level synthesis. ACM Trans. on Reconfigurable Technology and Systems, 2023.
[ DOI | pdf ]
POPL 2023: Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson. Taking back control in an intermediate representation for GPU computing. Proc. ACM on Programming Languages, 7(POPL), 2023.
[ DOI | pdf ]
FPL 2022: Jianyi Cheng, Lana Josipović, George A. Constantinides, and John Wickerson. Dynamic inter-block scheduling for HLS. In IEEE Int. Symp. on Field-Programmable Logic and Applications, 2022. Finalist for the Michal Servit Best Paper Award.
[ DOI | pdf ]
FCCM 2022: Michalis Pardalos, Yann Herklotz, and John Wickerson. Resource sharing for verified high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2022. Short paper category.
[ DOI | pdf ]
FCCM 2022: Jianyi Cheng, John Wickerson, and George A. Constantinides. Dynamic C-slow pipelining for HLS. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2022.
[ DOI | pdf ]
STVR 2022: Matt Windsor, Alastair F. Donaldson, and John Wickerson. High-coverage metamorphic testing of concurrency support in C compilers. Software Testing, Verification and Reliability, 2022.
[ DOI | blog | pdf ]
ESOP 2022: Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, and John Wickerson. View-based Owicki–Gries reasoning for persistent x86-TSO. In European Symposium on Programming, 2022. Distinguished Artifact award.
[ DOI | pdf ]
TCAD 2022: Patrick Sittel, Nicolai Fiege, John Wickerson, and Peter Zipf. Optimal and heuristic approaches to modulo scheduling with rational initiation intervals in hardware synthesis. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 41:614--627, 2022.
[ DOI | pdf ]
TCAD 2022: Jianyi Cheng, Lana Josipović, George A. Constantinides, Paolo Ienne, and John Wickerson. DASS: Combining dynamic & static scheduling in high-level synthesis. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 41:628--641, 2022.
[ DOI | pdf ]
FPGA 2022: Jianyi Cheng, John Wickerson, and George A. Constantinides. Finding and finessing static islands in dynamically scheduled circuits. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2022.
[ DOI | pdf ]
OOPSLA 2021: Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, and John Wickerson. The semantics of shared memory in Intel CPU/FPGA systems. Proc. ACM on Programming Languages, 5(OOPSLA), 2021.
[ DOI | blog | pdf ]
OOPSLA 2021: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal verification of high-level synthesis. Proc. ACM on Programming Languages, 5(OOPSLA), 2021.
[ DOI | pdf ]
OOPSLA 2021: Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, and Alastair F. Donaldson. Specifying and testing GPU workgroup progress models. Proc. ACM on Programming Languages, 5(OOPSLA), 2021.
[ DOI | pdf ]
FPL 2021: Jianyi Cheng, John Wickerson, and George A. Constantinides. Exploiting the correlation between dependence distance and latency in loop pipelining. In IEEE Int. Symp. on Field-Programmable Logic and Applications, 2021.
[ DOI | pdf ]
ISSTA 2021: Matt Windsor, Alastair F. Donaldson, and John Wickerson. C4: the C compiler concurrency checker. In ACM SIGSOFT Int. Symp. on Software Testing and Analysis, 2021. Tool demonstrations track.
[ DOI | blog | pdf ]
LATTE 2021: Yann Herklotz and John Wickerson. High-level synthesis tools should be proven correct. In Workshop on Languages, Tools, and Techniques for Accelerator Design, 2021.
[ video | pdf ]
FCCM 2021: Yann Herklotz, Zewei Du, Nadesh Ramanathan, and John Wickerson. An empirical study of the reliability of high-level synthesis tools. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2021. Short paper category.
[ DOI | blog | pdf ]
FCCM 2021: Jianyi Cheng, John Wickerson, and George A. Constantinies. Probabilistic optimization for high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2021.
[ DOI | blog | pdf ]
TC 2021: Jianyi Cheng, Shane Fleming, Yu Ting Chen, Jason Anderson, John Wickerson, and George A. Constantinides. Efficient memory arbitration in high-level synthesis from multi-threaded code. IEEE Transactions on Computers, 2021.
[ DOI | pdf ]
MET 2021: Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, and John Wickerson. Dreaming up metamorphic relations: Experiences from three fuzzer tools. In Int. Workshop on Metamorphic Testing, 2021.
[ DOI | pdf ]
TVLSI 2021: Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Global analysis of C concurrency in high-level synthesis. IEEE Trans. on Very Large Scale Integration (VLSI) Systems, 29(1):24--37, 2021.
[ DOI | pdf ]
FPL 2020: Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Precise pointer analysis in high-level synthesis. In Int. Conf. on Field Programmable Logic and Applications, 2020.
[ DOI | pdf ]
CAV 2020: James Brotherston, Diana Costa, Aquinas Hobor, and John Wickerson. Reasoning over permissions regions in concurrent separation logic. In Int. Conf. on Computer Aided Verification, 2020.
[ DOI | pdf ]
RTAS 2020: Dan Iorga, Tyler Sorensen, John Wickerson, and Alastair F. Donaldson. Slow and steady: Measuring and tuning multicore interference. In IEEE Real-Time and Embedded Technology and Applications Symposium, 2020.
[ DOI | pdf ]
FPGA 2020: Yann Herklotz and John Wickerson. Finding and understanding bugs in FPGA synthesis tools. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2020.
[ DOI | slides | blog | pdf ]
FPGA 2020: Jianyi Cheng, Lana Josipović, George A. Constantinides, Paolo Ienne, and John Wickerson. Combining dynamic and static scheduling in high-level synthesis. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2020.
[ DOI | pdf ]
POPL 2020: Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. Persistency semantics of the Intel-x86 architecture. Proc. ACM on Programming Languages, 4(POPL), 2020.
[ DOI | pdf ]
TVLSI 2020: He Li, James J. Davis, John Wickerson, and George A. Constantinides. Architect: Arbitrary-precision hardware with digit elision for efficient iterative compute. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 28(2):516--529, 2020.
[ DOI | pdf ]
ASP-DAC 2020: Patrick Sittel, John Wickerson, Martin Kumm, and Peter Zipf. Modulo scheduling with rational initiation intervals in custom hardware design. In Asia and South Pacific Design Automation Conference, 2020. Nominated for Best Paper award.
[ DOI | blog | pdf ]
OOPSLA 2019: Azalea Raad, John Wickerson, and Viktor Vafeiadis. Weak persistency semantics from the ground up. Proc. ACM on Programming Languages, 3(OOPSLA), 2019.
[ DOI | pdf ]
TCAD 2018: Junyi Liu, John Wickerson, Samuel Bayliss, and George A. Constantinides. Polyhedral-based dynamic loop pipelining for high-level synthesis. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 37(9), September 2018.
[ DOI | pdf ]
ARITH 2018: He Li, James J. Davis, John Wickerson, and George A. Constantinides. Digit elision for arbitrary-accuracy iterative computation. In IEEE Symp. on Computer Arithmetic, 2018.
[ DOI | pdf ]
PLDI 2018: Nathan Chong, Tyler Sorensen, and John Wickerson. The semantics of transactions and weak memory in x86, Power, ARM, and C++. In ACM Conf. on Programming Language Design and Implementation, 2018. Distinguished Paper award. Also presented at USENIX ATC 2019 in the Best of the Rest track.
[ DOI | press | video | short slides | long slides | blog | pdf ]
FCCM 2018: Nadesh Ramanathan, George A. Constantinides, and John Wickerson. Concurrency-aware thread scheduling for high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2018. Runner-up, Best Paper award.
[ DOI | blog | pdf ]
2018: John Wickerson and George A. Constantinides. From irregular heterogeneous software to reconfigurable hardware. In Bashir Al-Hashimi and Geoff Merrett, editors, Many Core Computing: Hardware and Software. IET Press, 2018.
[ DOI ]
TC 2018: Nadesh Ramanathan, John Wickerson, and George A. Constantinides. Scheduling weakly consistent C concurrency for reconfigurable hardware. IEEE Transactions on Computers, 67(7), July 2018.
[ DOI | pdf ]
FPT 2017: He Li, James J. Davis, John Wickerson, and George A. Constantinides. ARCHITECT: Arbitrary-precision constant-hardware iterative compute. In Int. Conf. on Field-Programmable Technology, 2017. Best Paper Presentation award.
[ DOI | pdf ]
FPL 2017: Junyi Liu, John Wickerson, and George A. Constantinides. Tile size selection for optimized memory reuse in high-level synthesis. In Int. Conf. on Field Programmable Logic and Applications, 2017.
[ DOI | pdf ]
FPGA 2017: Nadesh Ramanathan, Shane T. Fleming, John Wickerson, and George A. Constantinides. Hardware synthesis of weakly consistent C concurrency. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2017.
[ DOI | slides | blog | pdf ]
POPL 2017: John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. Automatically comparing memory consistency models. In ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 2017.
[ DOI | tex | poster | additional material | video | slides | blog | pdf ]
HiPC 2016: Andrea Picciau, Gordon E. Inggs, John Wickerson, Eric C. Kerrigan, and George A. Constantinides. Balancing locality and concurrency: solving sparse triangular systems on GPUs. In IEEE Int. Conf. on High Performance Computing, Data, and Analytics, 2016.
[ DOI | pdf ]
FPT 2016: Yiren Zhao, John Wickerson, and George A. Constantinides. An efficient implementation of online arithmetic. In Int. Conf. on Field-Programmable Technology, 2016.
[ DOI | pdf ]
FCCM 2016: Junyi Liu, John Wickerson, and George A. Constantinides. Loop splitting for efficient pipelining in high-level synthesis. In IEEE Int. Symp. on Field-Programmable Custom Computing Machines, 2016.
[ DOI | pdf ]
FPGA 2016: Nadesh Ramanathan, John Wickerson, Felix Winterstein, and George A. Constantinides. A case for work-stealing on FPGAs with OpenCL atomics. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2016. Short paper category.
[ DOI | pdf ]
FPGA 2016: Xitong Gao, John Wickerson, and George A. Constantinides. Automatically optimizing the latency, area, and accuracy of C programs for high-level synthesis. In ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays, 2016.
[ DOI | pdf ]
POPL 2016: Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling SC atomics in C11 and OpenCL. In ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 2016.
[ DOI | tex | additional material | video | slides | pdf ]
TOPLAS 2015: Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, and John Wickerson. The design and implementation of a verification technique for GPU kernels. ACM Trans. Programming Languages and Systems, 37(3), 2015.
[ DOI | pdf ]
FPT 2015: Felix Winterstein, Kermin Fleming, Hsin-Jung Yang, John Wickerson, and George A. Constantinides. Custom-sized caches in application-specific memory hierarchies. In Int. Conf. on Field-Programmable Technology, 2015.
[ DOI | pdf ]
OOPSLA 2015: John Wickerson, Mark Batty, Bradford M. Beckmann, and Alastair F. Donaldson. Remote-scope promotion: Clarified, rectified, and verified. In ACM SIGPLAN Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, 2015.
[ DOI | tex | additional material | video | slides | pdf ]
ASPLOS 2015: Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. GPU concurrency: Weak behaviours and programming assumptions. In ACM Int. Conf. on Architectural Support for Programming Languages and Operating Systems, 2015.
[ DOI | additional material | pdf ]
IWOCL 2014: Ethel Bardsley, Alastair F. Donaldson, and John Wickerson. KernelInterceptor: Automating GPU kernel verification by intercepting kernels and their parameters. In Int. Workshop on OpenCL, 2014.
[ DOI | pdf ]
ESOP 2013: John Wickerson, Mike Dodds, and Matthew J. Parkinson. Ribbon proofs for separation logic. In Europ. Symp. on Programming, 2013.
[ DOI | tex | slides | pdf ]
LICS 2012: John Wickerson, Mike Dodds, and Matthew J. Parkinson. Ribbon proofs for separation logic. In ACM/IEEE Symp. on Logic in Computer Science, 2012. Short paper category.
[ slides | pdf ]
2011: Tony Hoare and John Wickerson. Unifying models of data flow. In Manfred Broy, Christian Leuxner, and Tony Hoare, editors, Software and Systems Safety. IOS Press, 2011.
[ DOI | slides | pdf ]
ESOP 2010: John Wickerson, Mike Dodds, and Matthew J. Parkinson. Explicit stabilisation for modular rely-guarantee reasoning. In Europ. Symp. on Programming, 2010.
[ DOI | tex | slides | pdf ]

Invited papers, unpublished notes, and theses

DHPCC++ 2018: John Wickerson. Journey to the centre of the OpenCL memory model. In Workshop on Distributed and Heterogeneous Programming in C and C++, 2018. Keynote Address.
[ slides ]
FMATS 2018: John Wickerson. Towards verified hardware compilation. In Sixth Workshop on Formal Methods and Tools for Security, 2018.
[ slides ]
ACSSC 2017: Junyi Liu, John Wickerson, Samuel Bayliss, and George A. Constantinides. Run fast when you can: Loop pipelining with uncertain and non-uniform memory dependencies. In Asilomar Conf. on Signals, Systems and Computers, 2017. Invited paper.
[ DOI | pdf ]
CONCUR 2017: Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, and John Wickerson. Forward progress on GPU concurrency. In Int. Conf. on Concurrency Theory, 2017. Invited paper.
[ DOI | pdf ]
2013: John Wickerson. Ribbon proofs and dynamically-scoped quantifiers. Unpublished note, 2013.
[ pdf ]
2013: John Wickerson. Concurrent Verification for Sequential Programs. other, University of Cambridge, July 2013.
[ DOI | pdf ]
2009: John Wickerson. Partial and total correctness as greatest and least fixed points. Unpublished note, 2009.
[ pdf ]
2008: John Wickerson. Nominal prolog. Final-year (Part II) dissertation, University of Cambridge, July 2008.
[ pdf ]

Professional service

Conference and workshop organisation:

2025: Design, Automation, and Test in Europe (DATE), topic co-chair for System-Level Design Methodologies and High-Level Synthesis
2024: POPL 2024 Workshop on The Future of Weak Memory, co-organiser
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM), vice chair of Software and Tools track
Design, Automation, and Test in Europe (DATE), topic co-chair for System-Level Design Methodologies and High-Level Synthesis
2023: IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM), vice chair of Software and Tools track
2022: Isaac Newton Institute Concurrency Meeting, co-organiser
Field-Programmable Logic and Applications (FPL), workshops/tutorials chair
FLASHLIGHT, co-organiser
2021: ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI), publicity chair
2020: ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI), publicity chair
2015: Imperial Concurrency Workshop, co-organiser

Program/review committee member:

2025: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)
ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
2024: Field-Programmable Logic and Applications (FPL)
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
2023: Asian Symposium on Programming Languages and Systems (APLAS)
Designer Track, Design Automation Conference (DAC)
2022: ACM Symp. on Principles of Programming Languages (POPL)
ACM SIGSOFT Int. Symp. on Software Testing and Analysis (ISSTA)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
2021: ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
Europ. Conf. on Object-Oriented Programming (ECOOP)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
2020: ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
2019: Europ. Conf. on Object-Oriented Programming (ECOOP), external review committee
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
Asia and South Pacific Design Automation Conference (ASP-DAC)
Designer Track, Design Automation Conference (DAC)
Field-Programmable Logic and Applications (FPL)
2018: Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)
Designer Track, Design Automation Conference (DAC)
Field-Programmable Logic and Applications (FPL)
2017: Field-Programmable 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)

Reviewer for the following conferences and journals:

2024: IEEE Transactions on Computer-Aided Design of Integrated Circuits (TCAD)
ACM Transactions on Software Engineering and Methodology (TOSEM)
Springer Science of Computer Programming (SCICO)
2022: ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
Springer Formal Methods in System Design (FMSD)
2021: ACM Trans. on Reconfigurable Technology and Systems (TRETS)
ACM Trans. on Programming Languages and Systems (TOPLAS)
2020: ACM Trans. on Reconfigurable Technology and Systems (TRETS)
2019: Science of Computer Programming
2018: IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (TCAD)
IEEE Int. Symp. on Field-Programmable 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 Field-Programmable 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 Object-Oriented 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 (RTA-TLCA)
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 and other roles

Lecturer for a module on Instruction Architectures and Compilers for second-year EIE students (since 2018)
Lecturer for a module on Hardware and Software Verification for fourth-year EIE students and MSc students (since 2019)
Lecturer for a lab on Mastering Digital Design for MSc students (2019–2022)
Course Director for the Electrical and Information Engineering degree
Deputy Tutor for PhD students
Personal Tutor for first-year EE students
Affiliate of the Imperial Institute for Security Science and Technology
Senior Member of the IEEE
Member of the ACM