Blog Post

ICSE 2011: Grigore Rosu - The Art and Science of Program Verification

Sign in to queue

The Discussion

  • User profile image
    AceHack

    How does this compare to something like TAL?
    https://channel9.msdn.com/Shows/Going+Deep/Chris-Hawblitzel-and-Juan-Chen-Introduction-to-Typed-Assembly-Language-TAL
    Are they completely different, do they overlap, exactly the same?  I'm just curious.

    Will vefified language approaches like this be able to have abstractions like C++ AMP.
    https://channel9.msdn.com/posts/Daniel-Moth-Blazing-fast-code-using-GPUs-and-more-with-C-AMP

    Are there efforts to auto optimize for different memory setups, like computer clusters, harddrives, local memeory, etc... kinda a distanct to information optimization based on a verified spec?  A language call Sequoia++ is similar to this.
    http://sequoia.stanford.edu/

     This was a great talk, thanks.

  • User profile image
    Chucky Ellison

    I should add the K project page can be found at https://code.google.com/p/k-framework/ and the semantics of C in K (mentioned in the talk) can be found at http://code.google.com/p/c-semantics/ .

    I am not sure TAL is very closely related to K, term rewriting, or matching logic.

    K could handle language abstractions as long as they too were given semantics.

    The closest thing I think to your last point is that implementation-defined behavior in C is configurable. This would be things like different sized ints or pointers. There is a small amount of work on speeding up formal interpreters (http://hdl.handle.net/2142/17444) but the focus hasn't been on performance yet.

  • User profile image
    EvgeniyPlus​Plus

    Great thanks for the video! I had a lot of fun watching!
    Both speakers are great professionals as it seems. Hope to meet personally such people one day.

Add Your 2 Cents