{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:54:31Z","timestamp":1725544471728},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540331025"},{"type":"electronic","value":"9783540331032"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691617_14","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T09:14:13Z","timestamp":1143537253000},"page":"234-251","source":"Crossref","is-referenced-by-count":5,"title":["Towards a Compositional SPIN"],"prefix":"10.1007","author":[{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"first","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Cerny, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: Proc. of 32nd POPL, pp. 98\u2013109 (2005)","DOI":"10.1145\/1040305.1040314"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 548\u2013562. Springer, Heidelberg (2005)"},{"key":"14_CR4","unstructured":"Barringer, H., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Proof rules for automated compositional verification through learning. In: Int. Workshop on Specification and Verification of Component-Based Sys. (September 2003)"},{"key":"14_CR5","unstructured":"Chaki, S., Clarke, E., Giannakopoulou, D., Pasareanu, C.: Abstraction and assume-guarantee reasoning for automated software verification. Technical report, RIACS (2004)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/11513988_51","volume-title":"Computer Aided Verification","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E.M., Sinha, N., Thati, P.: Automated assume-guarantee reasoning for simulation conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 534\u2013547. Springer, Heidelberg (2005)"},{"issue":"4","key":"14_CR7","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"S.C. Cheung","year":"1996","unstructured":"Cheung, S.C., Kramer, J.: Context constraints for compositional reachability analysis. ACM Trans. on Soft. Eng. and Methodology\u00a05(4), 334\u2013377 (1996)","journal-title":"ACM Trans. on Soft. Eng. and Methodology"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Proc. of the Fourth Symp. on Logic in Comp. Sci, pp. 353\u2013362 (1989)","DOI":"10.1109\/LICS.1989.39190"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. of the 22nd Int. Conf. on Soft. Eng. (June 2000)","DOI":"10.1145\/337180.337234"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for sharedmemory programs. In: Proc. of the Eleventh European Symp. on Prog., April 2002, pp. 262\u2013277 (2002)","DOI":"10.1007\/3-540-45927-8_19"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11537328_24","volume-title":"Model Checking Software","author":"D. Giannakopoulou","year":"2005","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning-based assume-guarantee verification (Tool paper). In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 282\u2013287. Springer, Heidelberg (2005)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proc. of the Seventeenth IEEE Int. Conf. on Auto. Soft. Eng. (September 2002)","DOI":"10.1109\/ASE.2002.1114984"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Cobleigh, J.M.: Assume-guarantee verification of source code with design-level assumptions. In: Int. Conf. on Soft. Eng., May 2004, pp. 211\u2013220 (2004)","DOI":"10.1109\/ICSE.2004.1317443"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Proc. of the Eighth Int. Conf. on Tools and Alg. for the Construction and Analysis of Sys., April 2002, pp. 357\u2013370 (2002)","DOI":"10.1007\/3-540-46002-0_25"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. In: Proc. of the Second Int. Conf. on Concurrency Theory, August 1991, pp. 250\u2013265 (1991)","DOI":"10.1007\/3-540-54430-5_93"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Proc. of PLDI, pp. 1\u201313 (2004)","DOI":"10.1145\/996841.996844"},{"issue":"5","key":"14_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Soft. Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"14_CR19","volume-title":"The SPIN Model Checker : Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-540-24732-6_6","volume-title":"Model Checking Software","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 76\u201391. Springer, Heidelberg (2004)"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-45069-6_31","volume-title":"Computer Aided Verification","author":"H. Hungar","year":"2003","unstructured":"Hungar, H., Niese, O., Steffen, B.: Domain-specific optimization in automata learning. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 315\u2013327. Springer, Heidelberg (2003)"},{"key":"14_CR22","first-page":"321","volume-title":"Information Processing 83: Proceedings of the IFIP 9th World Congress","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Mason, R. (ed.) Information Processing 83: Proceedings of the IFIP 9th World Congress, pp. 321\u2013332. North Holland, IFIP (1983)"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Krimm, J.-P., Mounier, L.: Compositional state space generation from Lotos programs. In: Proc. of the Third Int. Workshop on Tools and Alg. for the Construction and Analysis of Sys., April 1997, pp. 239\u2013258 (1997)","DOI":"10.1007\/BFb0035392"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T.W., Sagiv, S.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"14_CR25","volume-title":"Concurrency: State Models & Java Programs","author":"J. Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Maler, O., Pnueli, A.: On the Learnability of Infinitary Regular Sets. Information and Computation\u00a0118(2) (1995)","DOI":"10.1006\/inco.1995.1070"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-48234-2_14","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C.S. P\u0103s\u0103reanu","year":"1999","unstructured":"P\u0103s\u0103reanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: A comparative case study. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 168\u2013183. Springer, Heidelberg (1999)"},{"key":"14_CR28","first-page":"123","volume-title":"Logic and Models of Concurrent Systems","author":"A. Pnueli","year":"1984","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K. (ed.) Logic and Models of Concurrent Systems, vol.\u00a013, pp. 123\u2013144. Springer, Heidelberg (1984)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-540-31980-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Vardhan","year":"2005","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Using language inference to verify omega-regular properties. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 45\u201360. Springer, Heidelberg (2005)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"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\u201312 (2000)","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T13:18:45Z","timestamp":1555507125000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11691617_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}