University of Minnesota
Software Engineering Center

You are here

SEng Seminar Series: Guest, Grigore Rosu

Date of Event: 
Saturday, December 3, 2016 - 12:15pm to 3:30pm
Keller Hall room 3-210
Campus Map

All Software Engineering Industrial Seminars are open to public

Title: Automatic Error Detection Using Runtime Verification

Speaker: Grigore Rosu

Presented by the University of Minnesota Software Engineering Center

Abstract: What does this C program return?

int main() {
    int x = 0;
    return (x = 1) + (x = 2);

Could it return 17? Believe it or not, the answer is yes. Because the program is "undefined" according to the ISO C11 standard, C compilers are free to optimize it however they wish, for instance by returning 17. Incidentally, when compiled with gcc it yields 4 while with clang 3. C programs that contain undefined behavior can have non-deterministic behavior or can crash when you change compiler or compilation options. Therefore, if portability is important, you must be able to verify compliance with the ISO C standard.

In this talk I will describe and demonstrate the runtime verification tools RV-Match and RV-Predict. RV-Match provides an ISO C11-compliant compiler for C that detects more undefinedness errors (e.g., buffer overflows and underflows, stack overflows, etc.) than the best commercial static analysis tools, for instance on the Toyota ITC benchmark test-suite. RV-Predict is a data-race detection tool that can detect buggy patterns in an execution trace by using the SMT solver Z3. Both tools are completely automatic and report no false positives.

Lecture slides

Bio Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the founder and president of Runtime Verification, Inc (RV). 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. He was offered the CAREER award by the NSF, the Dean's award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper that helped shape the runtime verification field), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002. He was ranked a UIUC excellent teacher in Spring 2013, Fall 2012, Spring 2008 and Fall 2004.
Sign up for event: 
The email to associate with this registration.
This question is for testing whether or not you are a human visitor and to prevent automated spam submissions.
20 + 0 =
Solve this simple math problem and enter the result. E.g. for 1+3, enter 4.