Explicit Stabilisation for Modular Rely-Guarantee Reasoning. - John Wickerson; Mike Dodds; Matthew J. Parkinson (ESOP, 2010)

Unifying Models of Data Flow. - Tony Hoare; John Wickerson (Software and Systems Safety - Specification and Verification, 2011)

Ribbon Proofs for Separation Logic. - John Wickerson; Mike Dodds; Matthew J. Parkinson (ESOP, 2013)

Ribbon Proofs. - John Wickerson (Arch. Formal Proofs, 2013)

Concurrent verification for sequential programs. - John Wickerson (2013)

KernelInterceptor: automating GPU kernel verification by intercepting kernels and their parameters. - Ethel Bardsley; Alastair F. Donaldson; John Wickerson (IWOCL, 2014)

Syntax and semantics of a GPU kernel programming language. - John Wickerson (Arch. Formal Proofs, 2014)

GPU Concurrency: Weak Behaviours and Programming Assumptions. - Jade Alglave; Mark Batty; Alastair F. Donaldson; Ganesh Gopalakrishnan; Jeroen Ketema; Daniel Poetzl; Tyler Sorensen 001; John Wickerson (ASPLOS, 2015)

Custom-sized caches in application-specific memory hierarchies. - Felix Winterstein; Kermin Fleming; Hsin-Jung Yang; John Wickerson; George A. Constantinides (FPT, 2015)

Remote-scope promotion: clarified, rectified, and verified. - John Wickerson; Mark Batty; Bradford M. Beckmann; Alastair F. Donaldson (OOPSLA, 2015)

Taming the complexities of the C11 and OpenCL memory models. - John Wickerson; Mark Batty (CoRR, 2015)

The Design and Implementation of a Verification Technique for GPU Kernels. - Adam Betts; Nathan Chong; Alastair F. Donaldson; Jeroen Ketema; Shaz Qadeer; Paul Thomson; John Wickerson (ACM Trans. Program. Lang. Syst., 2015)

Loop Splitting for Efficient Pipelining in High-Level Synthesis. - Junyi Liu; John Wickerson; George A. Constantinides (FCCM, 2016)

Automatically Optimizing the Latency, Area, and Accuracy of C Programs for High-Level Synthesis. - Xitong Gao; John Wickerson; George A. Constantinides (FPGA, 2016)

A Case for Work-stealing on FPGAs with OpenCL Atomics. - Nadesh Ramanathan; John Wickerson; Felix Winterstein; George A. Constantinides (FPGA, 2016)

An efficient implementation of online arithmetic. - Yiren Zhao; John Wickerson; George A. Constantinides (FPT, 2016)

Balancing Locality and Concurrency: Solving Sparse Triangular Systems on GPUs. - Andrea Picciau; Gordon E. Inggs; John Wickerson; Eric C. Kerrigan; George A. Constantinides (HiPC, 2016)

Overhauling SC atomics in C11 and OpenCL. - Mark Batty; Alastair F. Donaldson; John Wickerson (POPL, 2016)

Run fast when you can: Loop pipelining with uncertain and non-uniform memory dependencies. - Junyi Liu; John Wickerson; Samuel Bayliss; George A. Constantinides (ACSSC, 2017)

Forward Progress on GPU Concurrency (Invited Talk). - Alastair F. Donaldson; Jeroen Ketema; Tyler Sorensen 001; John Wickerson (CONCUR, 2017)

Hardware Synthesis of Weakly Consistent C Concurrency. - Nadesh Ramanathan; Shane T. Fleming; John Wickerson; George A. Constantinides (FPGA, 2017)

Tile size selection for optimized memory reuse in high-level synthesis. - Junyi Liu; John Wickerson; George A. Constantinides (FPL, 2017)

architect: Arbitrary-precision constant-hardware iterative compute. - He Li 008; James J. Davis 001; John Wickerson; George A. Constantinides (FPT, 2017)

Automatically comparing memory consistency models. - John Wickerson; Mark Batty; Tyler Sorensen 001; George A. Constantinides (POPL, 2017)

The Semantics of Transactions and Weak Memory in x86, Power, ARMv8, and C++. - Nathan Chong; Tyler Sorensen 001; John Wickerson (CoRR, 2017)

Digit Elision for Arbitrary-accuracy Iterative Computation. - He Li 008; James J. Davis 001; John Wickerson; George A. Constantinides (ARITH, 2018)

Concurrency-Aware Thread Scheduling for High-Level Synthesis. - Nadesh Ramanathan; George A. Constantinides; John Wickerson (FCCM, 2018)

The semantics of transactions and weak memory in x86, Power, ARM, and C++. - Nathan Chong; Tyler Sorensen 001; John Wickerson (PLDI, 2018)

Scheduling Weakly Consistent C Concurrency for Reconfigurable Hardware. - Nadesh Ramanathan; John Wickerson; George A. Constantinides (IEEE Trans. Computers, 2018)

Polyhedral-Based Dynamic Loop Pipelining for High-Level Synthesis. - Junyi Liu; John Wickerson; Samuel Bayliss; George A. Constantinides (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. - Azalea Raad; John Wickerson; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

Modulo Scheduling with Rational Initiation Intervals in Custom Hardware Design. - Patrick Sittel; John Wickerson; Martin Kumm; Peter Zipf (ASP-DAC, 2020)

Reasoning over Permissions Regions in Concurrent Separation Logic. - James Brotherston; Diana Costa 001; Aquinas Hobor; John Wickerson (CAV (2), 2020)

Combining Dynamic & Static Scheduling in High-level Synthesis. - Jianyi Cheng; Lana Josipovic; George A. Constantinides; Paolo Ienne; John Wickerson (FPGA, 2020)

Finding and Understanding Bugs in FPGA Synthesis Tools. - Yann Herklotz; John Wickerson (FPGA, 2020)

Precise Pointer Analysis in High-Level Synthesis. - Nadesh Ramanathan; George A. Constantinides; John Wickerson (FPL, 2020)

Slow and Steady: Measuring and Tuning Multicore Interference. - Dan Iorga; Tyler Sorensen 001; John Wickerson; Alastair F. Donaldson (RTAS, 2020)

Persistency semantics of the Intel-x86 architecture. - Azalea Raad; John Wickerson; Gil Neiger; Viktor Vafeiadis (Proc. ACM Program. Lang., 2020)

architect: Arbitrary-Precision Hardware With Digit Elision for Efficient Iterative Compute. - He Li 008; James J. Davis 001; John Wickerson; George A. Constantinides (IEEE Trans. Very Large Scale Integr. Syst., 2020)

Probabilistic Scheduling in High-Level Synthesis. - Jianyi Cheng; John Wickerson; George A. Constantinides (FCCM, 2021)

An Empirical Study of the Reliability of High-Level Synthesis Tools. - Yann Herklotz; Zewei Du; Nadesh Ramanathan; John Wickerson (FCCM, 2021)

Probabilistic Optimization for High-Level Synthesis. - Jianyi Cheng; John Wickerson; George A. Constantinides (FPGA, 2021)

Fuzzing High-Level Synthesis Tools. - Zewei Du; Yann Herklotz; Nadesh Ramanathan; John Wickerson (FPGA, 2021)

Exploiting the Correlation between Dependence Distance and Latency in Loop Pipelining for HLS. - Jianyi Cheng; John Wickerson; George A. Constantinides (FPL, 2021)

Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools. - Andrei Lascu; Matt Windsor; Alastair F. Donaldson; Tobias Grosser; John Wickerson (MET@ICSE, 2021)

C4: the C compiler concurrency checker. - Matt Windsor; Alastair F. Donaldson; John Wickerson (ISSTA, 2021)

Formal verification of high-level synthesis. - Yann Herklotz; James D. Pollard; Nadesh Ramanathan; John Wickerson (Proc. ACM Program. Lang., 2021)

The semantics of shared memory in Intel CPU/FPGA systems. - Dan Iorga; Alastair F. Donaldson; Tyler Sorensen 001; John Wickerson (Proc. ACM Program. Lang., 2021)

Specifying and testing GPU workgroup progress models. - Tyler Sorensen 001; Lucas F. Salvador; Harmit Raval; Hugues Evrard; John Wickerson; Margaret Martonosi; Alastair F. Donaldson (Proc. ACM Program. Lang., 2021)

Global Analysis of C Concurrency in High-Level Synthesis. - Nadesh Ramanathan; George A. Constantinides; John Wickerson (IEEE Trans. Very Large Scale Integr. Syst., 2021)

View-Based Owicki-Gries Reasoning for Persistent x86-TSO. - Eleni Vafeiadi Bila; Brijesh Dongol; Ori Lahav 001; Azalea Raad; John Wickerson (ESOP, 2022)

Dynamic C-Slow Pipelining for HLS. - Jianyi Cheng; John Wickerson; George A. Constantinides (FCCM, 2022)

Resource Sharing for Verified High-Level Synthesis. - Michalis Pardalos; Yann Herklotz; John Wickerson (FCCM, 2022)

Finding and Finessing Static Islands in Dynamically Scheduled Circuits. - Jianyi Cheng; John Wickerson; George A. Constantinides (FPGA, 2022)

Dynamic Inter-Block Scheduling for HLS. - Jianyi Cheng; Lana Josipovic; George A. Constantinides; John Wickerson (FPL, 2022)

View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version). - Eleni Vafeiadi Bila; Brijesh Dongol; Ori Lahav 001; Azalea Raad; John Wickerson (CoRR, 2022)

High-coverage metamorphic testing of concurrency support in C compilers. - Matt Windsor; Alastair F. Donaldson; John Wickerson (Softw. Test. Verification Reliab., 2022)

Efficient Memory Arbitration in High-Level Synthesis From Multi-Threaded Code. - Jianyi Cheng; Shane T. Fleming; Yu Ting Chen; Jason Helge Anderson; John Wickerson; George A. Constantinides (IEEE Trans. Computers, 2022)

DASS: Combining Dynamic & Static Scheduling in High-Level Synthesis. - Jianyi Cheng; Lana Josipovic; George A. Constantinides; Paolo Ienne; John Wickerson (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022)

Optimal and Heuristic Approaches to Modulo Scheduling With Rational Initiation Intervals in Hardware Synthesis. - Patrick Sittel; Nicolai Fiege; John Wickerson; Peter Zipf (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022)

A Case for Precise, Fine-Grained Pointer Synthesis in High-Level Synthesis. - Nadesh Ramanathan; George A. Constantinides; John Wickerson (ACM Trans. Design Autom. Electr. Syst., 2022)

Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version). - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (CoRR, 2023)

Taking Back Control in an Intermediate Representation for GPU Computing. - Vasileios Klimis; Jack Clark; Alan Baker; David Neto; John Wickerson; Alastair F. Donaldson (Proc. ACM Program. Lang., 2023)

Balancing Static Islands in Dynamically Scheduled Circuits Using Continuous Petri Nets. - Jianyi Cheng; Estíbaliz Fraca; John Wickerson; George A. Constantinides (IEEE Trans. Computers, 2023)

Parallelising Control Flow in Dynamic-scheduling High-level Synthesis. - Jianyi Cheng; Lana Josipovic; John Wickerson; George A. Constantinides (ACM Trans. Reconfigurable Technol. Syst., 2023)

Simulating Operational Memory Models Using Off-the-Shelf Program Analysis Tools. - Dan Iorga; John Wickerson; Alastair F. Donaldson (IEEE Trans. Software Eng., 2023)

Intel PMDK Transactions: Specification, Validation and Concurrency. - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (ESOP (2), 2024)

Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency. - Azalea Raad; Ori Lahav 001; John Wickerson; Piotr Balcer; Brijesh Dongol (ESOP (2), 2024)

Validating Database System Isolation Level Implementations with Version Certificate Recovery. - Jack Clark; Alastair F. Donaldson; John Wickerson; Manuel Rigger (EuroSys, 2024)

Automated Feature Testing of Verilog Parsers using Fuzzing (Registered Report). - Quentin Corradi; John Wickerson; George A. Constantinides (FUZZING, 2024)

Challenges in Empirically Testing Memory Persistency Models. - Vasileios Klimis; Alastair F. Donaldson; Viktor Vafeiadis; John Wickerson; Azalea Raad (NIER@ICSE, 2024)

Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour. - Vasileios Klimis; Alastair F. Donaldson; Viktor Vafeiadis; John Wickerson; Azalea Raad (CoRR, 2024)

Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations. - Luke Geeson; James Brotherston; Wilco Dijkstra; Alastair F. Donaldson; Lee Smith; Tyler Sorensen 001; John Wickerson (Proc. ACM Program. Lang., 2024)

Hyperblock Scheduling for Verified High-Level Synthesis. - Yann Herklotz; John Wickerson (Proc. ACM Program. Lang., 2024)

Formalising CXL Cache Coherence. - Chengsong Tan; Alastair F. Donaldson; John Wickerson (ASPLOS (2), 2025)

The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs. - Chengsong Tan; Alastair F. Donaldson; Jonathan Julián Huerta y Munive; John Wickerson (FormaliSE, 2025)

Hardware.jl - An MLIR-based Julia HLS Flow (Work in Progress). - Benedict Short; Ian McInerney; John Wickerson (CoRR, 2025)