Events

Date: 10 February 2025   Time: 15:00 - 17:00

Location: Peter Landin 4.24

Speaker: Vasilis Klimis

Title: Fuzzing

The work is about how we applied lightweight formal methods to improve SPIRV, the industry-standard language for GPU computing. One major focus was on structured control flow: we built a formal model that helped us identify ambiguities and unnecessary complexities in the specification. This led to improvements in the spec itself (now part of the latest release) after collaborating with spec's authors.
We also used the model to validate developer tools and conformance test suites, cross-checking them to catch inconsistencies. A particularly interesting outcome was using the model to design a new fuzzing method for SPIRV compilers, which ended up uncovering a surprising number of miscompilation bugs in compilers from Google, Intel, Mozilla, and others.
I think this work is a good example of how formal modelling can be practical and impactful in real-world programming languages.

The seminar will be followed by a social event at which all are welcome.