16. D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Component verification with automatically generated
assumptions. Autom. Softw. Eng., 12(3):297–320, 2005.
17. A. Gupta, K. L. McMillan, and Z. Fu. Automated assumption generation for compositional verification. Formal
Methods in System Design, 32(3):285–301, 2008.
18. B. Li, I. Dillig, T. Dillig, K. L. McMillan, and M. Sagiv. Synthesis of circular compositional program proofs via
abduction. In TACAS, 2013.
19. S. Lin and P. Hsiung. Compositional synthesis of concurrent systems through causal model checking and learning.
In FM, 2014.
20. J. Magee and J. Kramer. Concurrency - state models and Java programs. Wiley, 1999.
21. K. L. McMillan. Circular compositional reasoning about liveness. In CHARME, 1999.
22. J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Trans. Software Eng., 7(4):417–426, 1981.
23. K. S. Namjoshi and R. J. Trefler. On the competeness of compositional reasoning. In CAV, 2000.
24. C. S. Pasareanu, D. Giannakopoulou, M. G. Bobaru, J. M. Cobleigh, and H. Barringer. Learning to divide and
conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design,
2008.
25. C. Peirce and C. Hartshorne. Collected Papers of Charles Sanders Peirce. Belknap Press, 1932.
26. A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of
Concurrent Systems, NATO ASI Series, 1985.
27. R. Singh, D. Giannakopoulou, and C. S. Pasareanu. Learning component interfaces with may and must abstractions.
In CAV, 2010.
28. V. Weispfenning. Quantifier elimination and decision procedures for valued fields. Models and Sets.Lecture Notes
in Mathematics (LNM), 1103:419––472, 1984.
Assume, Guarantee or Repair
227
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits
use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you
give appropriate credit to the original author(s) and the source, provide a link to the Creative
Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter’s Creative
Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain
permission directly from the copyright holder.
assumptions. Autom. Softw. Eng., 12(3):297–320, 2005.
17. A. Gupta, K. L. McMillan, and Z. Fu. Automated assumption generation for compositional verification. Formal
Methods in System Design, 32(3):285–301, 2008.
18. B. Li, I. Dillig, T. Dillig, K. L. McMillan, and M. Sagiv. Synthesis of circular compositional program proofs via
abduction. In TACAS, 2013.
19. S. Lin and P. Hsiung. Compositional synthesis of concurrent systems through causal model checking and learning.
In FM, 2014.
20. J. Magee and J. Kramer. Concurrency - state models and Java programs. Wiley, 1999.
21. K. L. McMillan. Circular compositional reasoning about liveness. In CHARME, 1999.
22. J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Trans. Software Eng., 7(4):417–426, 1981.
23. K. S. Namjoshi and R. J. Trefler. On the competeness of compositional reasoning. In CAV, 2000.
24. C. S. Pasareanu, D. Giannakopoulou, M. G. Bobaru, J. M. Cobleigh, and H. Barringer. Learning to divide and
conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design,
2008.
25. C. Peirce and C. Hartshorne. Collected Papers of Charles Sanders Peirce. Belknap Press, 1932.
26. A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of
Concurrent Systems, NATO ASI Series, 1985.
27. R. Singh, D. Giannakopoulou, and C. S. Pasareanu. Learning component interfaces with may and must abstractions.
In CAV, 2010.
28. V. Weispfenning. Quantifier elimination and decision procedures for valued fields. Models and Sets.Lecture Notes
in Mathematics (LNM), 1103:419––472, 1984.
Assume, Guarantee or Repair
227
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits
use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you
give appropriate credit to the original author(s) and the source, provide a link to the Creative
Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter’s Creative
Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain
permission directly from the copyright holder.