This is one of the few research groups that are doing interesting practical work in this area.
from Derek Jones blog note - a link to the paper
That team’s awesome. One of few groups in formal methods using rewriting logic (Maude) with excellent results. They build their own modified logic called matching logic on top that they claim is better than separation logic. More interesting, their use of these tools allowed them to make their C semantics executable in a style similar to GCC:
I want this group to do one for Rust and SPARK as a reference spec for certifying compilers for those. It might be easier to use than a lot of the work in Coq or Isabelle/HOL. Might. I’m just guessing by how much faster they do their semantics.
EDIT to add: They also have a company that they use to partly fund this work.