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. The bottleneck of this type of reasoning is coming up with appropriate assumptions, typically a difficult manual process.
Over the last few years, we have developed frameworks for incremental, and fully automated assume-guarantee reasoning based on an off-the shelf learning algorithm and on model checking. We will discuss these frameworks and their application to NASA case studies.
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.
