c-semantics

I believe it is "simpler" in terms of formal semantics. Formalizing standard C is way harder (see https://github.com/kframework/c-semantics). In fact, C0 is explicitly targeted at computer scientists rather than engineers.

That team’s awesome. One of few groups in formal methods using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. They also build their own modified logic called matching logic on top that they claim is better than separation logic. http://www.kframework.org/index.php/Main_Page More interesting, their use of these tools allowed them to make their C semantics executable in a style similar to GCC: https://github.com/kframework/c-semantics I want this group to do one for Rust and SPARK as a reference spec for certifying compilers for those. Also useful for the diverse compilation concept to counter Karger's compiler/compiler subversion. On a side note, they also have a company that they use to fund and apply their work: https://runtimeverification.com/

I'm a fan of both sides of the Coq and Isabelle/HOL activities. I'm keeping an eye on CertiCoq. Right now, though, Isabelle/HOL seems to be ahead with work like Myreen and Davis's in terms of verified stacks: https://www.cl.cam.ac.uk/~mom22/ This data structure refinement with one version getting automated to a large degree: https://www21.in.tum.de/~lammich/pub/cpp2016_impds.pdf Thanks to DeepSpec, Coq might exceed that in some ways: https://deepspec.org/main Note that a lot of work around Coq goes through CompCert which is proprietary software with restrictions on how it's used if one doesn't pay. The Isabelle/HOL alternatives like Simpl/C and CakeML are free software. Then, outside those two, we got a bunch of work being done in Maude (esp K Framework) with one an executable, formal semantics for C done like a compiler: https://github.c

I wonder why he mentions this TIS interpreter but not the development of complete semantics for C and specifically the k framework (https://github.com/kframework/c-semantics). Afaik, kcc is also really good at finding undefined behavior. Regehr even wrote about it in the past (https://blog.regehr.org/archives/523).

I presume that KCC in question is https://github.com/kframework/c-semantics, i.e., a formalization of C programming language in a form suitable for evaluation. It indeed can detect undefined behaviour, though last time I played with it (a few years ago) it was hardly something that you can use on anything but trivial examples. Not to mention that it crashed on various implementation defined behaviours (for example comparing unrelated pointers with <) limiting its usefulness even further. BTW, both gcc and clang contain runtime checker for easily detectable undefined behaviours like singed overflow you have mentioned. You can enable it with -fsanitize=undefined.

"Deterministically locating all undefined behavior is undecidable. Static analyzers can only locate a subset of it." It might be true but barely matters when we have tools like KCC. It's built on an executable semantics of C that runs in a framework on top of Maude rewrite engine. http://www.kframework.org/index.php/Main_Page https://github.com/kframework/c-semantics http://fsl.cs.illinois.edu/FSL/papers/2015/hathhorn-ellison-...

The kcc compiler is really good at being predicatable. A formal semantics of the language gives warnings whenever undefined behavior occurs. https://github.com/kframework/c-semantics

I suggest you email the team that did the C formal semantics about doing one for Rust. They did it in K Framework (Maude-based) with a front end, KCC, designed to be usable like GCC. Their other work includes functional and logic languages. A team that did an executable semantics for all of those seems ideal for a formalized compiler for Rust given it's like several styles combined. Their rewriting based tools could probably handle at least a subset. Then you get DDC for free plus a way to equivalence check reference compiler for certain features. https://github.com/kframework/c-semantics http://www.kframework.org/index.php/Main_Page

Also see the work done in the under-utilized K Framework which captures & rejects undefined behavior as well: http://fsl.cs.illinois.edu/index.php/Defining_the_Undefinedn... Since it's K, they were able to turn it into a GCC-like compiler for you verifying things about your application. If it even compiles, you have no undefined behavior. https://github.com/kframework/c-semantics On concurrency side, it's built on top of Maude tool that an inexperienced student was able to use to find errors in Eiffel's SCOOP model for concurrency. So, it can probably handle that aspect as well.