Automated Assume-guarantee Verification

Опубликовано 6 сентября 2016, 17:33

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)