VLDB 2026 Research / reviewers in the wild / expert
Matt Windsor
dblp:202/8969
· DBLP profile ↗
4ranked-venue papers
4as first author
3since 2021 · last 2022
0000-0003-1285-0080ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 4 · 4 first-author · 3 since 2021Theory of computation · 1 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2022 | RoboCert: Property Specification in Robotics
Matt Windsor, Ana Cavalcanti 0001 |
ICFEM | 1 |
| 2022 | High-coverage metamorphic testing of concurrency support in C compilersabstractSummary We present a technique and automated toolbox for randomized testing of C compilers. Unlike prior compiler‐testing approaches, we generate concurrent test cases in which threads communicate using fine‐grained atomic operations, and we study actual compiler implementations rather than abstract mappings. Our approach is (1) to generate test cases with precise oracles directly from an axiomatization of the C concurrency model; (2) to apply metamorphic fuzzing to each test case, aiming to amplify the coverage they are likely to achieve on compiler codebases; and (3) to execute each fuzzed test case extensively on a range of real machines. Our tool, C4, benefits compiler developers in two ways. First, test cases generated by C4 can achieve line coverage of parts of the LLVM C compiler that are reached by neither the LLVM test suite nor an existing (sequential) C fuzzer. This information can be used to guide further development of the LLVM test suite and can also shed light on where and how concurrency‐related compiler optimizations are implemented. Second, C4 can be used to gain confidence that a compiler implements concurrency correctly. As evidence of this, we show that C4 achieves high strong mutation coverage with respect to a set of concurrency‐related mutants derived from a recent version of LLVM and that it can find historic concurrency‐related bugs in GCC. As a by‐product of concurrency‐focused testing, C4 also revealed two previously unknown sequential compiler bugs in recent versions of GCC and the IBM XL compiler. Matt Windsor, Alastair F. Donaldson, John Wickerson |
Softw. Test. Verification Reliab. | 1 |
| 2021 | C4: the C compiler concurrency checkerabstractThe correct compilation of atomic-action concurrency is vital now that multicore processors are ubiquitous. Despite much recent work on automated compiler testing, little existing tooling can test how real-world compilers handle compilation of atomic-action code. We demonstrate C4, a tool for exploring the concurrency behaviour of real-world C compilers such as GCC and LLVM. C4 automates a workflow based on generating, fuzzing, and executing litmus tests. So far, C4 has found two new control-flow bugs in GCC and IBM XL, and reproduced two historic concurrency bugs in GCC 4. Matt Windsor, Alastair F. Donaldson, John Wickerson |
ISSTA | 1 |
| 2017 | Starling: Lightweight Concurrency Verification with Views
Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson |
CAV (1) | 1 |