Proof System Case Study
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). It is itself a significant piece of work which took around 15 years. It is a rather important corner stone, however, that is achieved by the verification community, with tools/frameworks available in 2009, it is already possible to formally verify a complex system such as a compiler. ...