Abstract
Despite significant advances in the development of model checking, it remains a difficult task in the hands of experts to make it scale to the size of industrial systems. A key step in achieving scalability is to “divide-and-conquer”, that is, to break up the veri.cation of a system into smaller tasks that involve the verification of its components. Assume-guarantee reasoning [9, 11] is a widespread “divide-and-conquer” approach that uses assumptions when checking individual components of a system. Assumptions essentially encode expectations that each component has from the rest the system in order to operate correctly. Coming up with the right assumptions is typically a non-trivial manual process, which limits the applicability of this type of reasoning in practice.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Barringer, H., Giannakopoulou, D., Păsăreanu, C.S.: Proof rules for automated compositional verification through learning. In: Proc. SAVCBS Workshop (2003)
Chaki, S., Clarke, E., Giannakopoulou, D., Păsăreanu, C.: Abstraction and assume-guarantee reasoning for automated software verification. RIACS TR 05.02 (October 2004)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE TSE 30(6), 388–402 (2004)
Chatley, R., Eisenbach, S., Magee, J.: Magicbeans: a Platform for Deploying Plugin Components. In: Emmerich, W., Wolf, A.L. (eds.) CD 2004. LNCS, vol. 3083, pp. 97–112. Springer, Heidelberg (2004)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Păsăreanu, C., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: ICSE 2000 (2000)
Giannakopoulou, D., Păsăreanu, C.S., Cobleigh, J.M.: Assume-guarantee verification of source code with design-level assumptions. In: Proc. of ICSE 2004 (2004)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Prog. Lang. and Sys. 5(4), 596–619 (1983)
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems, 123–144 (1985)
Visser, W., Havelund, K., Brat, G., Park, S.-J.: Model checking programs. In: Proc. of the Fifteenth IEEE Int. Conf. on Auto. Soft. Eng., September 2000, pp. 3–12 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giannakopoulou, D., Păsăreanu, C.S. (2005). Learning-Based Assume-Guarantee Verification (Tool Paper). In: Godefroid, P. (eds) Model Checking Software. SPIN 2005. Lecture Notes in Computer Science, vol 3639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11537328_24
Download citation
DOI: https://doi.org/10.1007/11537328_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28195-5
Online ISBN: 978-3-540-31899-6
eBook Packages: Computer ScienceComputer Science (R0)