Introducing C4: the C Compiler Concurrency Checker

Ilan Iwumbwe and Benny Liu did undergraduate research placements with me this summer, and I’m very pleased that they will be presenting their work at the Programming Languages for Quantum Computing (PLanQC) workshop at POPL next month. Ilan and Benny built a tool called QuteFuzz that randomly generates descriptions of quantum circuits. The idea...

I wrote earlier this year about my attempt to understand the repercussions of toggling and when giving a semantics to Hoare triples. In response to that post, Yann Herklotz helpfully pointed me to Patrick Cousot’s POPL 2024 paper [10], which does all this and a lot more besides. In particular, Cousot’s paper includes the following… Continue...

The UK government imposes a tax on people’s income, and, as is quite conventional, the rate at which a person pays this tax increases as their income increases. However, I was surprised to notice recently that this rate does not increase monotonically with income. Here is how the UK government explains the calculation of income… Continue reading...

This post provides a short introduction to a paper that will be presented at DVCon in Munich next month by my PhD student Michalis Pardalos about work we have done with collaborators Alastair Donaldson, Emi Morini and Laura Pozzi. Hardware engineers take great care to ensure that their designs are correct. Unlike bugs in software,… Continue...

I’m delighted that Quentin Corradi, a PhD student I jointly supervise with George Constantinides, will be presenting his work to improve the reliability of hardware design tools next week at the FUZZING’24 workshop, a satellite event of the ISSTA conference. The Verilog language is widely used in hardware design, and is accepted by a multitude…...