This is cool work. Peter Sewell has been giving talks about this, and he is a great speaker. Here is one from this year's EuroLLVM developers' meeting, includin

This is cool work. Peter Sewell has been giving talks about this, and he is a great speaker. Here is one from this year's EuroLLVM developers' meeting, including some demos of the Cerberus tool: "The Cerberus Memory Object Semantics for ISO and De Facto C" https://www.youtube.com/watch?v=SI3uycKDH8Y https://www.youtube.com/watch?v=SI3uycKDH8Y