Loading user information from Channel 9

Something went wrong getting user information from Channel 9

Latest Achievement:

Loading user information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

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

17 minutes, 49 seconds


Right click “Save as…”

Grigore Rosu is an associate professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering, and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000 and his M.S. at the University of Bucharest, Romania, in 1996. He was offered the CAREER award by the NSF and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won an ACM SIGSOFT distinguished paper award at ASE 2008 as well as the best software science paper award at ETAPS 2002, and he was ranked a UIUC excellent teacher in Spring 2008 and Fall 2004. [source]

Here, Wolfram Schulte and Grigore briefly discuss the potential of K, a term rewriting based executable semantic framework for defining programming languages, and Matching Logic, an executable semantics framework yielding an alternative (to Hoare logic) program verification logic. It's another great conversation from Channel 9's coverage of ICSE 2011. Thanks to Wolfram and Grigore! Tune in.



Follow the discussion

  • Oops, something didn't work.

    Getting subscription
    Subscribe to this conversation
  • Aaron StainbackAceHack AceHack

    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.

  • Chucky EllisonChucky 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.

  • EvgeniyPlusPlusEvgeniyPlus​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.

Remove this comment

Remove this thread


Comments closed

Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums, or Contact Us and let us know.