ICSE 2011: Grigore Rosu - The Art and Science of Program Verification
- Posted: Jun 22, 2011 at 7:00 AM
- 54,086 Views
- 3 Comments
Download
How do I download the videos?
- To download, right click the file type you would like and pick “Save target as…” or “Save link as…”
Why should I download videos from Channel9?
- It's an easy way to save the videos you like locally.
- You can save the videos in order to watch them offline.
- If all you want is to hear the audio, you can download the MP3!
Which version should I choose?
- If you want to view the video on your PC, Xbox or Media Center, download the High Quality WMV file (this is the highest quality version we have available).
- If you'd like a lower bitrate version, to reduce the download time or cost, then choose the Medium Quality WMV file.
- If you have a Zune, WP7, iPhone, iPad, or iPod device, choose the low or medium MP4 file.
- If you just want to hear the audio of the video, choose the MP3 file.
Right click “Save as…”
- High Quality WMV (PC, Xbox, MCE)
- MP3 (Audio only)
- Mid Quality WMV (Lo-band, Mobile)
- High Quality MP4 (iPad, PC)
- MP4 (iPod, Zune HD)
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.
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.
Follow the Discussion
How does this compare to something like TAL?
http://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.
http://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.
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.
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
close