{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T08:56:20Z","timestamp":1766048180228},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_24","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"331-346","source":"Crossref","is-referenced-by-count":219,"title":["Learning Assumptions for Compositional Verification"],"prefix":"10.1007","author":[{"given":"Jamieson M.","family":"Cobleigh","sequence":"first","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Corina S.","family":"P\u0102s\u0102reanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Compositionality: The Significant Difference-An International Symposium, 1997.","DOI":"10.1109\/SFCS.1997.646098"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proc. of the 10th Int. Conf. on Computer-Aided Verification, pages 521\u2013525, June 28\u2013July 2, 1998.","DOI":"10.1007\/BFb0028774"},{"issue":"2","key":"24_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87\u2013106, Nov. 1987.","journal-title":"Information and Computation"},{"issue":"4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"S. C. Cheung","year":"1996","unstructured":"S. C. Cheung and J. Kramer. Context constraints for compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 5(4):334\u2013377, Oct. 1996.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"1","key":"24_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/295558.295570","volume":"8","author":"S. C. Cheung","year":"1999","unstructured":"S. C. Cheung and J. Kramer. Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology, 8(1):49\u201378, Jan. 1999.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"3","key":"24_CR6","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"T. S. Chow","year":"1978","unstructured":"T. S. Chow. Testing software design modeled by finite-state machines. IEEE Transactions on Software Engineering, SE-4(3):178\u2013187, May 1978.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proc. of the 4th Symp. on Logic in Computer Science, pages 353\u2013362, June 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"24_CR8","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"L. de Alfaro and T. A. Henzinger. Interface automata. In Proc. of the 8th European Software Engineering Conf. held jointly with the 9th ACM SIGSOFT Symp. on the Foundations of Software Engineering, pages 109\u2013120, Sept. 2001.","DOI":"10.1145\/503209.503226"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"L. de Alfaro and T. A. Henzinger. Interface theories for component-based design. In Proc. of the 1st Int. Workshop on Embedded Software, pages 148\u2013165, Oct. 2001.","DOI":"10.1007\/3-540-45449-7_11"},{"key":"24_CR11","unstructured":"T. Dean and M. S. Boddy. An analysis of time-dependent planning. In Proc. of the 7th National Conf. on Artificial Intelligence, pages 49\u201354, Aug. 1988."},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for sharedmemory programs. In Proc. of the 11th European Symp. on Programming, pages 262\u2013277, Apr. 2002.","DOI":"10.1007\/3-540-45927-8_19"},{"issue":"1","key":"24_CR13","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008645800955","volume":"6","author":"D. Giannakopoulou","year":"1999","unstructured":"D. Giannakopoulou, J. Kramer, and S. C. Cheung. Behaviour analysis of distributed systems using the Tracta approach. Automated Software Engineering, 6(1):7\u201335, July 1999.","journal-title":"Automated Software Engineering"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"D. Giannakopoulou, C. S. P\u0103s\u0103reanu, and H. Barringer. Assumption generation for software component verification. In Proc. of the 17th IEEE Int. Conf. on Automated Software Engineering, Sept. 2002.","DOI":"10.1109\/ASE.2002.1114984"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"A. Groce, D. Peled, and M. Yannakakis.Adaptive model checking. In Proc. of the 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 357\u2013370, Apr. 2002.","DOI":"10.1007\/3-540-46002-0_25"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. of the 2nd Int. Conf. on Concurrency Theory, pages 250\u2013265, Aug. 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, S. Qadeer, and S. K. Rajamani. You assume, we guarantee: Methodology and case studies. In Proc. of the 10th Int. Conf. on Computer-Aided Verification, pages 440\u2013451, June 28\u2013July 2, 1998.","DOI":"10.1007\/BFb0028765"},{"key":"24_CR18","unstructured":"C. B. Jones. Specification and design of (parallel) programs. In R. Mason, editor, Information Processing 83: Proc. of the IFIP 9th World Congress, pages 321\u2013332. IFIP: North Holland, 1983."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"J.-P. Krimm and L. Mounier. Compositional state space generation from Lotos programs. In Proc. of the 3rd Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 239\u2013258, Apr. 1997.","DOI":"10.1007\/BFb0035392"},{"key":"24_CR20","unstructured":"J. Magee and J. Kramer. Concurrency: State Models & Java Programs. John Wiley & Sons, 1999."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logic and Models of Concurrent Systems, volume 13, pages 123\u2013144, New York, 1984. Springer-Verlag.","DOI":"10.1007\/978-3-642-82453-1_5"},{"issue":"2","key":"24_CR22","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"R. L. Rivest","year":"1993","unstructured":"R. L. Rivest and R. E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299\u2013347, Apr. 1993.","journal-title":"Information and Computation"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat, and S.-J. Park. Model checking programs. In Proc. of the 15th IEEE Int. Conf. on Automated Software Engineering, Sept. 2000.","DOI":"10.1109\/ASE.2000.873645"},{"issue":"2","key":"24_CR24","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Q. Xu, W. P. de Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149\u2013174, 1997.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:45:28Z","timestamp":1558982728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}