Formalization of token implementation in Ethereum smart contracts using the tool behind the C semantics.
Yeah, they’re interesting since they use rewriting logic in K and Maude instead of traditional proof assistants. One use of Maude was finding errors in SCOOP model for concurrency that Eiffel uses. The language work ranges from Scheme to Prolog to C with the semantics of latter into a compiler. If I picked one, I’d have this group do the semantics for Rust with C as the output leveraging their existing work. That could solve a lot problems in terms of reusing tooling.
Their recent work is the company hosting the submission with the static analyzer for C programs with no or few false positives being most notable. It’s a cool group. I was glad to see on this submission that they’re porting K to LLVM for performance enhancement.