Corina Pasareanu, Dimitra Giannakopoulou: Automated assume-guarantee reasoning for component verification

Abstract: Assume-guarantee reasoning is a divide and conquer approach to the verification of large systems that makes use of "assumptions" about the environment of a system component. Although aimed at scalability, such reasoning has not been widely applied, because coming up with appropriate assumptions is a difficult manual process. In the first part of our talk, we will present two novel techniques for generating assumptions automatically for finite-state software models. The first technique synthesizes the weakest assumption that a component needs to make about its environment for a given property to be satisfied. The second technique defines a framework for incremental, and fully automated assume-guarantee reasoning, based on learning. Our techniques have been successfully applied to a number of NASA case studies. In the second part of the talk we will describe recent extensions of our work towards automated circular assume-guarantee reasoning and modular verification of actual source code. We will also discuss possible avenues for integrating the MAGIC tool with our framework.

CV: Corina Pasareanu is a Kestrel 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. More information can be found at http://ase.arc.nasa.gov/people/pcorina/, and she can be contacted on pcorina@email.arc.nasa.gov.

CV: Dimitra Giannakopoulou is a RIACS research scientist at the NASA Ames Research Center. Her research focuses on scalable specification and verification techniques for NASA systems. In particular, she is interested in incremental and compositional model checking based on software components and architectures. Prior to that, she was employed on UK and European Union projects by Imperial College, University of London. Her work involved the development of methods and tools for the verification of concurrent systems based on their software architecture. Dr Giannakopoulou graduated from the Dept. of Computer Engineering and Informatics, University of Patras, Greece. She holds an MSc with distinction and a PhD, both from the Dept of Computing, Imperial College, University of London. More information can be found at http://ase.arc.nasa.gov/people/dimitra/, and she can be contacted on dimitra@email.arc.nasa.gov.