{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:56:54Z","timestamp":1725490614419},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_8","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"39-54","source":"Crossref","is-referenced-by-count":17,"title":["SAT-Based Compositional Verification Using Lazy Learning"],"prefix":"10.1007","author":[{"given":"Nishant","family":"Sinha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Foci: An interpolating prover, http:\/\/www.kenmcmil.com\/foci.html"},{"key":"8_CR2","unstructured":"http:\/\/vlsi.coloradu.edu\/~vis\/"},{"key":"8_CR3","unstructured":"Yices: An smt solver, http:\/\/yices.csl.sri.com\/"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2005)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/11560548_20","volume-title":"Correct Hardware Design and Verification Methods","author":"N. Amla","year":"2005","unstructured":"Amla, N.: An analysis of sat-based model checking techniques in an industrial environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 254\u2013268. Springer, Heidelberg (2005)"},{"issue":"2","key":"8_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation\u00a075(2), 87\u2013106 (1987)","journal-title":"Information and Computation"},{"key":"8_CR7","unstructured":"Barringer, H., Giannakopoulou, D., Pasareanu, C.S.: Proof rules for automated compositional verification. In: SAVCBS (2003)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/11693017_10","volume-title":"FASE 2006","author":"T. Berg","year":"2006","unstructured":"Berg, T., Jonsson, B., Raffelt, H.: Regular inference for state machines with parameters. In: Baresi, L., Heckel, R. (eds.) FASE 2006 and ETAPS 2006. LNCS, vol.\u00a03922, pp. 107\u2013121. Springer, Heidelberg (2006)"},{"key":"8_CR9","first-page":"117","volume-title":"Advances in Computers","author":"Armin Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zue, Y.: Bounded Model Checking. In: Zelkowitz, M. (ed.) Advances in computers, vol.\u00a058 (2003)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Sagar Chaki and Ofer Strichman. Optimized L* for assume-guarantee reasoning. In: TACAS (to appear, 2007)","DOI":"10.1109\/FMCAD.2006.8"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cobleigh, J., Avrunin, G., Clarke, L.: Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: ISSTA, pp. 97\u2013108 (2006)","DOI":"10.1145\/1146238.1146250"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, Springer, Heidelberg (2003)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"4","key":"8_CR14","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"Niklas E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental sat solving. Electr. Notes Theor. Comput. Sci.\u00a089(4) (2003)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2","key":"8_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.12.021","volume":"119","author":"R. Armoni","year":"2005","unstructured":"Armoni, R., et al.: Sat-based induction for temporal safety properties. Electr. Notes Theor. Comput. Sci.\u00a0119(2), 3\u201316 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Gheorghiu, M., Giannakopoulou, D., Pasareanu, C.S.: Refining interface alphabets for compositional verification. In: TACAS (to Appear)","DOI":"10.1007\/978-3-540-71209-1_23"},{"key":"8_CR17","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Massachusetts (1979)"},{"issue":"4","key":"8_CR18","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1007\/3-540-48224-5_67","volume-title":"Automata, Languages and Programming","author":"P. Maier","year":"2001","unstructured":"Maier, P.: A set-theoretic framework for assume-guarantee reasoning. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 821\u2013834. Springer, Heidelberg (2001)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"4","key":"8_CR21","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng.\u00a07(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Software Eng."},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11901914_15","volume-title":"Automated Technology for Verification and Analysis","author":"W. Nam","year":"2006","unstructured":"Nam, W., Alur, R.: Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 170\u2013185. Springer, Heidelberg (2006)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/10722167_14","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 139\u2013153. Springer, Heidelberg (2000)"},{"key":"8_CR24","volume-title":"Logics and models of concurrent systems","author":"A. Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems, Springer, Heidelberg (1985)"},{"issue":"2","key":"8_CR25","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M.R. Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. STTT\u00a07(2), 156\u2013173 (2005)","journal-title":"STTT"},{"issue":"2","key":"8_CR26","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"R.L. Rivest","year":"1993","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. In: Inf. Comp. vol.\u00a0103(2), pp. 299\u2013347 (1993)","journal-title":"Information and Computation"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a sat-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"8_CR28","unstructured":"Sinha, N., Clarke, E.: SAT-based compositional verification using lazy learning. Technical report CMU-CS-07-109, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA (February 2007)"},{"key":"8_CR29","unstructured":"Tinelli, C., Ranise, S.: SMT-LIB: The Satisfiability Modulo Theories Library (2005), http:\/\/goedel.cs.uiowa.edu\/smtlib\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:41Z","timestamp":1619518121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_8","relation":{},"subject":[]}}