Halfway across the world computer scientists gathered in Singapore on Oct. 30 for the start of the Conference on Automated Software Engineering (ASE) at the University of Illinois at Urbana-Champaign (UIUC), which runs through Nov. 3. This year's general chair of the conference is a former computer-science student at UC San Diego. CSE alumnus Grigore Rosu (Ph.D. '00) is also receiving ASE's Most Influential Paper Award. The honor is a test-of-time award, and in Rosu's case, he is being hailed for the influential role he played with the publication in 2001 of a paper on "Monitoring Programs Using Rewriting." The paper, which grew out of his doctoral research, helped launch the field of runtime verification -- a mathematically rigorous way to monitor and analyze software program execution.
Today Rosu (at right) is a professor of computer science at UIUC, where he leads the Formal Systems Laboratory. Previously, he was a scientist at NASA, where he coined the term 'runtime verification' with colleagues at the agency. In 2010, Rosu also founded a startup, Runtime Verification, Inc., to promote and incorporate the new and promising technology into robust and practical commercial products.
Rosu's award-winning paper, originally presented at ASE 2001, bridged two apparently different software engineering areas: testing (which runs once and checks if software is functioning properly); and formal verification, which uses mathematical techniques to prove a software program implements a specification.
“Formal verification is very intense and it doesn’t scale,” said Rosu in an article appearing on the CS @ Illinois website. “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.”
Rosu was a researcher at NASA when he authored the paper and coined the term “runtime verification” with his colleague Klaus Havelund, and runtime verification is now an established scientific field in its own right. Rosu joined NASA directly from earning his doctorate in computer science at UC San Diego.