4 ms·

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

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_Undefinedness_of_C 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 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.

fiddlerwoaroof 10y ago
Any write up about the errors they found? Are they a problem with SCOOP as such or an implementation issue?
- nickpsecurity 10y ago
  My memory is hazy but the abstract suggests this is the one I read before: http://se.ethz.ch/~meyer/publications/concurrency/scoop_maude.pdf http://se.ethz.ch/~meyer/publications/concurrency/scoop_maud... The good thing about SCOOP particularly is there was a lot of CompSci work improving on it in many ways. Most of the safer, concurrency models didn't get such attention. Example: http://cme.ethz.ch/publications/ http://cme.ethz.ch/publications/