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


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.




Right click to download this episode

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