@inbook {IOPORT.01956591,
    author       = {Cobleigh, Jamieson M. and Giannakopoulou, Dimitra and P\u{a}s\u{a}reanu, Corina S.},
    title        = {Learning assumptions for compositional verification.},
    year         = {2003},
    booktitle    = {Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7--11, 2003. Proceedings},
    isbn         = {3-540-00898-5},
    pages        = {331-346},
    publisher    = {Berlin: Springer},
    abstract     = {Summary: Compositional verification is a promising approach to addressing the state explosion problem associated with model checking. One compositional technique advocates proving properties of a system by checking properties of its components in an assume-guarantee style. However, the application of this technique is difficult because it involves non-trivial human input. This paper presents a novel framework for performing assume-guarantee reasoning in an incremental and fully automated fashion. To check a component against a property, our approach generates assumptions that the environment needs to satisfy for the property to hold. These assumptions are then discharged on the rest of the system. Assumptions are computed by a learning algorithm. They are initially approximate, but become gradually more precise by means of counterexamples obtained by model checking the component and its environment, alternately. This iterative process may at any stage conclude that the property is either true or false in the system. We have implemented our approach in the LTSA tool and applied it to a NASA system.},
    msc2010      = {F.3.1 (F.1.2 I.2.6)},
    identifier   = {01956591},
}