Loop invariants – where should we put them?

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…...

I was singing Freddy, My Love as a lullaby for my toddler last night, and enjoying the nifty rhyming triplets (catches–patches–matches, and so on), when I suddenly realised that the song has almost twice as many rhymes as I had previously thought! The last three lines of each verse not only rhyme at their ends,… Continue reading In praise of...