Automated Assume-guarantee Verification

  • Corina Pasareanu | NASA Ames Research Center

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. Coming up with appropriate assumptions used to be a difficult manual process. We will present recently developed techniques for performing assume-guarantee verification of software in a fully automated fashion. These techniques generate assumptions that model the operational context of a component when checking the component in isolation. We will describe learning-based and abstraction-based techniques that build and update assumptions in a systematic and iterative fashion. We will also discuss the application of the techniques to a number of NASA case studies. (joint work with D. Giannakopoulou and other people)

Speaker Details

Corina Pãsãreanu is a Research Scientist at the NASA Ames Research Center, Robust Software Engineering Group. Her research focuses on using abstraction and symbolic execution in the context of software model checking, with applications to test input generation and error detection. Her research interests also include automating assume-guarantee compositional verification and designing languages for commanding robots. She received her PhD degree from Kansas State University. She has served on program committees for many meetings in the formal analysis area, such as CAV, ISSTA, FSE, and ICSE. She is also an associate editor for the ACM TOSEM journal. More information can be found on her web-page at: http://ti.arc.nasa.gov/people/pcorina/

Watch Next