CS @ ILLINOIS Professor Grigore Rosu recently won the Most Influential Paper Award at the 2016 Automated Software Engineering (ASE) conference in Singapore. His 2001 paper, “Monitoring Programs Using Rewriting,” helped launch the field of runtime verification, which is a mathematically rigorous way to monitor and analyze software program execution.

According to Rosu, the significance of the paper is that it bridges two apparently different software engineering areas—testing and formal verification. An ad hoc and informal method, testing runs once and checks to see if a software program is functioning properly. Formal verification, on the other hand, uses mathematical techniques to prove a software program implements a specification.

“Formal verification is very intense and it doesn’t scale,” said Rosu. “What we did is execute the program and test the formal specifications at runtime to see if the program violates any of the specified requirements. We didn’t prove that a program was correct, but we didn’t let the program go wrong, either, so in the end the program behaved correctly.  It can be regarded as an alternative and lighter method to ensure that a program behaves correctly.”

A CS faculty member since 2002, Rosu was working as a researcher at the NASA space agency when he wrote the award-winning paper and coined the term “runtime verification” with his colleague Klaus Havelund. The runtime verification algorithm he introduced in the paper consisted of eight simple, yet elegant equations that described the basic laws of monitoring temporal logic. Today, Runtime Verification has established itself as a scientific field, with its own international conference.

In addition to helping establish runtime verification as a bona fide software analysis approach, the paper demonstrated a system, Java PathExplorer, that could function without access to a software program’s source code. That ability has become critical to industries like automotive manufacturing, where car makers embed third-party, proprietary software into their vehicles to control everything from power windows to brakes to the engine.

In 2010, Rosu founded a company, Runtime Verification, Inc., to commercialize technology developed in his U of I Formal Systems Laboratory (FSL). Located only 1 mile from the FSL, Runtime Verification, Inc., provides cutting-edge products to automatically and accurately detect the rarest, trickiest, and most costly bugs in software code, all based on the runtime verification state-of-the-art technology. The company has partnered with NASA, NSF, Boeing, Toyota, and global automotive supplier DENSO.

While proud to receive this award, Rosu believes it further confirms the excellence of CS @ ILLINOIS faculty in the software engineering area. Last year, Professor Darko Marinov received the same ASE Most Influential Paper award for his research on developing TestEra, a novel framework for automated testing of Java programs.

Rosu’s pride is well founded. According to csrankings.org, Illinois is ranked first in software engineering.

Editor's note: The 2017 ASE conference will be held at the University of Illinois at Urbana-Champaign (Oct. 30 - Nov 3, 2017). Professor Grigore Rosu is the conference general chair, Professor Tao Xie is the conference local arrangements chair, Professor Darko Marinov is the conference finance chair, Professor Sasa Misailovic is the proceedings chair, and CS staff member Donna Coleman is in charge of conference organization.