Formally proving tiny bits of qemu using Frama-C

Richard W.M. Jones (rjones @ redhat.com)
Monday November 16th, 2020

Formal verification of software proves that the software is mathematically correct with respect to its specification. Frama-C is an open source modular framework for formal verification of programs written in C.