Abstract: In the first part of the talk, we will describe some of the research work that was done at Kansas State University, as part of the Bandera project. This work is aimed at abstraction and modular reasoning for the verification of concurrent programs. We will present Bandera's approach to data abstraction, counter-example analysis and environment generation for Java programs. In the second part of the talk, we will describe two on-going projects at NASA Ames. One project involves the combination of symbolic execution with (explicit-state) model checking; the second project involves synthesis of assumptions about the environments of software components, such that these components satisfy given properties.

CV: Corina Pasareanu is a research scientist at NASA Ames Research Center, the Automated Software Engineering Group. Her research interests are in using abstraction techniques and automated tools, such as model checkers and theorem provers, as a base for efficient verification and validation of software. She is also interested in synthesis of code from temporal logic specifications and in modular reasoning for verification of partially specified software. She received her PhD degree from Kansas State University, the Department of Computing and Information Sciences.