Learn to Divide and Conquer
Dimitra Giannakopoulou (NASA)
- Place: E2, Rm 392
- Time: 2-3:10pm, Wednesday, February 22, 2006
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. 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.