Matt Windsor

Hi

I'm Matt Windsor. I'm a computer science postdoc researcher, currently working in the RoboStar group of the Department of Computer Science at the University of York on the TAS Verifiability Node.

I've previously worked at the Multicore Programming Group at Imperial College London on the Interface Reasoning for Interacting Systems, notably on the C4 project (on which I'm still working as and when I can!)

My main focus is tools and languages for software testing and verification. I have worked, at different times, on:

• automated verification of low-level concurrency (PhD)
• testing of concurrency support for C compilers (first postdoc)
• specifying properties of autonomous systems (current postdoc)

Projects

• C4, a toolkit for testing concurrency behaviour of C compilers (2018-)
• Starling, a tool and associated program logic for proving properties of low-level concurrent algorithms (2016-2019)

Publications

• C4: the C Compiler Concurrency Checker with Alastair F. Donaldson and John Wickerson (ISSTA Tool Demonstrations 2021, to appear)
• Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools with Andrei Lascu, Alastair F. Donaldson, Tobias Grosser, and John Wickerson (MET Workshop'2021, proceedings forthcoming)
• A framework for automated concurrency verification (PhD dissertation, 2019)
• Starling: Lightweight Concurrency Verification with Views with Mike Dodds, Ben Simner, and Matt Parkinson (CAV'2017)