Carnegie Mellon Scientist Wins 2010 ICSE Award-Silicon Valley Campus - Carnegie Mellon University

Carnegie Mellon Scientist Wins 2010 ICSE Award-Silicon Valley Campus - Carnegie Mellon University

Carnegie Mellon Scientist Wins 2010 ICSE Award

Dr. Corina Pasareanu, Senior Systems Scientist at Carnegie Mellon Silicon Valley, was awarded The International Conference on Software Engineering (ICSE) 2010 Most Influential Paper Award for co-authoring “Bandera: Extracting Finite-state Models from Java Source Code.” The award, jointly sponsored by ACM/SIGSOFT and IEEE TCSE, is highly regarded by the ICSE software engineering community, since it recognizes work that has had a profound influence on the software engineering field over the preceding ten year period. Dr. Pasareanu also received the ACM SIGSOFT Impact Paper Award for the same paper. The ACM SIGSOFT Impact Paper Award is presented annually to the author(s) of a paper presented at a SIGSOFT sponsored or co-sponsored conference held at least 10 years prior to the award year. In including all of SIGSOFT's conferences in the competition, this award recognizes the breadth and vitality of the software engineering community. The papers are judged by their influence since their publication. The award ceremony will be held at FSE-18 (International Symposium on Foundations of Software Engineering), in Santa Fe, New Mexico.

“I am really excited about these awards because they recognize the pioneering work we have done under the Bandera project for the automated verification of code, using a technique called model checking. Until this work, model checking had been applied mainly to high-level models but not to low-level code. Within Bandera, I worked on abstraction and modular techniques, aimed at increasing the scalability of the verification,” said Dr. Pasareanu.

“Bandera: Extracting Finite-state Models from Java Source Code” describes an integrated collection of program analysis and transformation components, called Bandera, that enables the automatic extraction of safe, compact finite-state models from program source code. Bandera takes Java source code as input and generates a program model in the input language of one of several existing verification tools. It also maps verifier outputs back to the original source code.

Bandera transformed model-checking by providing companies with a highly effective means of finding defects in software implementations. Before Bandara, companies used hand construction of models, which was expensive, prone to errors, and difficult to optimize.

Dr. Pasareanu is a researcher at NASA Ames in the Robust Software Engineering group, with research interests in software verification. She is currently investigating the use of abstraction and symbolic execution in the context of the Java PathFinder verification tool set, with applications in test input generation and error detection. She is also working on using learning techniques for automating assume-guarantee compositional verification and on modeling and analysis of heterogeneous systems. Dr. Pasareanu’s new research interests include parallelization of verification tasks.