Blog Post

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

Play ICSE 2011: Grigore Rosu - The Art and Science of Program Verification
Sign in to queue

The Discussion

  • User profile image

    How does this compare to something like 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.

    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.

     This was a great talk, thanks.

  • User profile image
    Chucky Ellison

    I should add the K project page can be found at and the semantics of C in K (mentioned in the talk) can be found at .

    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 ( but the focus hasn't been on performance yet.

  • User profile image

    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