Computer Systems

This blogpost is the second part of a trilogy of formal verification on computer systems. Here we will take a quick tour of what formal verification means, with a particular focus on verifying systems software and examples of verifying some file system. If you have not read the previous post on system verification, feel free to jump there first for an introduction! Case studies CompCert CompCert1 is probably one of the first and most famous verified compilers (and perhaps also computer systems)....

This blogpost is the first part of a trilogy of formal verification on computer systems. Here we will take a quick tour of what formal verification means, with a particular focus on verifying systems software and examples of verifying some file system. What do you mean by formally verified systems? Sometimes we hear people say we have built this formally verified system that is provably correct, and does all sorts of amazing things without bugs....