5 ms·

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 s

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 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 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/ https://runtimeverification.com/

pjmlp 9y ago
Maybe making Frama-C part of the C standard would also be an improvement.
jcranmer 9y ago
One of the courses I took involved working with K, and I certainly left the course thinking "I would love to use this tool in the future if I had a project to do with it." It is actually a fairly amazing tool, even if the instructions for using it involve "start by downloading it again, because we keep fixing bugs". One problem with building semantics for Rust is that the language doesn't have a sufficiently formal specification yet. LLVM IR also has a similar problem in that the community has generally somewhat resisted pinning down precise semantics of undefined behavior (this is changing, though, in large part because the imprecision is causing problems).
- nickpsecurity 9y ago
  "It is actually a fairly amazing tool" Since I watch formal methods from a distance, I can't really tell how good their approach is versus Microsoft's VCC w/ separation logic, Coq specifications, and so on. I just note they seem to have it easier than most like Coq with their method more flexible than separation logic. How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material? "One problem with building semantics for Rust is that the language doesn't have a sufficiently formal specification yet." My solution there was to make the semantics represent the current state of Rust and/or LLVM at any moment. They got the advantage of being the standard implementation. So, the spec needs to do what they do so users don't get inconsistent behavior. Then, the spec work might find errors or validate proposals that can feed back into reference implementations. Finally, as with KCC, the implementation might be useful for looking into compiler errors or subversions.
  - jcranmer 9y ago
    > How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material? I am not a formal methods person, and I have very little grounding in it. I still felt quite happy using it and came out of the course thinking "gee, I think I might actually like to use this if I ever had a need," which is the opposite anecdote I hear from people using a lot of formal methods tooling. You probably do need a basic grounding in semantics, though, things like big-step versus small-step operational semantics. Beyond that, the K framework itself has a tutorial on actually building the semantics in K. (See http://www.kframework.org/index.php/K_Tutorial http://www.kframework.org/index.php/K_Tutorial and the corresponding directories within its tooling).
tom_mellior 9y ago
> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonsensical. What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle? This is great work, and they are definitely using the right tool for the job. But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges.
- nickpsecurity 9y ago
  "What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle?" In the others, they tend to do formal semantics of interpreters or compilers then extract them to ML or something. This group uses an executable, rewriting engine to do an executable semantics of a lot of languages which seems to require less people. Perhaps they're doing less on the verification side but what I've seen make me think more should try such methods. Most work I see posted in formal methods isn't done with rewriting tools like Maude. The ones I see use it get some interesting results for effort put in such as the SCOOP verification. So, I took the time to highlight that they use a different approach with quite a bit of tooling to use that people might want to look into trying. My 2nd reply, jcranmer, had exactly the kind of positive experience I was thinking readers might get out of a follow-up. "But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges." You wouldn't notice it's enormous with the number of people that use a relatively-small set of tools. Convergence is usually good since ecosystems get built that can make new work easier. Coq and Isabelle/HOL are good examples where people keep plugging in prior work to new work. There's also quite a few more that don't get as much attention. Hence, me highlighting two (Maude and K) that had a series of practical results out of research using it.
- solidangle 9y ago
  Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.

pjmlp 9y ago

Maybe making Frama-C part of the C standard would also be an improvement.

jcranmer 9y ago

One of the courses I took involved working with K, and I certainly left the course thinking "I would love to use this tool in the future if I had a project to do with it." It is actually a fairly amazing tool, even if the instructions for using it involve "start by downloading it again, because we keep fixing bugs". One problem with building semantics for Rust is that the language doesn't have a sufficiently formal specification yet. LLVM IR also has a similar problem in that the community has generally somewhat resisted pinning down precise semantics of undefined behavior (this is changing, though, in large part because the imprecision is causing problems).

nickpsecurity 9y ago
"It is actually a fairly amazing tool" Since I watch formal methods from a distance, I can't really tell how good their approach is versus Microsoft's VCC w/ separation logic, Coq specifications, and so on. I just note they seem to have it easier than most like Coq with their method more flexible than separation logic. How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material? "One problem with building semantics for Rust is that the language doesn't have a sufficiently formal specification yet." My solution there was to make the semantics represent the current state of Rust and/or LLVM at any moment. They got the advantage of being the standard implementation. So, the spec needs to do what they do so users don't get inconsistent behavior. Then, the spec work might find errors or validate proposals that can feed back into reference implementations. Finally, as with KCC, the implementation might be useful for looking into compiler errors or subversions.
- jcranmer 9y ago
  > How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material? I am not a formal methods person, and I have very little grounding in it. I still felt quite happy using it and came out of the course thinking "gee, I think I might actually like to use this if I ever had a need," which is the opposite anecdote I hear from people using a lot of formal methods tooling. You probably do need a basic grounding in semantics, though, things like big-step versus small-step operational semantics. Beyond that, the K framework itself has a tutorial on actually building the semantics in K. (See http://www.kframework.org/index.php/K_Tutorial http://www.kframework.org/index.php/K_Tutorial and the corresponding directories within its tooling).

tom_mellior 9y ago

> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonsensical. What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle? This is great work, and they are definitely using the right tool for the job. But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges.

nickpsecurity 9y ago
"What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle?" In the others, they tend to do formal semantics of interpreters or compilers then extract them to ML or something. This group uses an executable, rewriting engine to do an executable semantics of a lot of languages which seems to require less people. Perhaps they're doing less on the verification side but what I've seen make me think more should try such methods. Most work I see posted in formal methods isn't done with rewriting tools like Maude. The ones I see use it get some interesting results for effort put in such as the SCOOP verification. So, I took the time to highlight that they use a different approach with quite a bit of tooling to use that people might want to look into trying. My 2nd reply, jcranmer, had exactly the kind of positive experience I was thinking readers might get out of a follow-up. "But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges." You wouldn't notice it's enormous with the number of people that use a relatively-small set of tools. Convergence is usually good since ecosystems get built that can make new work easier. Coq and Isabelle/HOL are good examples where people keep plugging in prior work to new work. There's also quite a few more that don't get as much attention. Hence, me highlighting two (Maude and K) that had a series of practical results out of research using it.
solidangle 9y ago
Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.