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.