On Mon, May 2, 2016 at 4:30 PM, Gabriel Scherer <gabriel.scherer@gmail.com>
wrote:

> I have been trying to motivate the Frama-C people to find an excellent
> intern to write a specification of the OCaml memory model in ACSL
> (their specification language for C, http://frama-c.com/acsl.html );
> the dream is that one may then be able to use Frama-C to check for
> safety of the C stubs, and even possibly verify some parts of the C
> codebase in the compiler distribution (probably not the runtime
> implementation itself, which precisely breaks the abstraction of the
> memory model, but at least large parts of C implementation of
> primitives, otherlibs/, etc.). I think they are interested as well,
> but I'm not sure they have found the time and people to work on this.
>
>
We're still very much interested in this, although I think the challenges
are more important than what you expect. The duality pointer/integer in
OCaml's runtime is a major pitfall. Triaging between both by looking at the
least significant bit won't be easy to handle.

In any case, if somebody looking for an internship is interested by this
topic, you're more than welcome to contact me!