Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers

David Monniaux

Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the…