{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:42Z","timestamp":1763468022019},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642203978"},{"type":"electronic","value":"9783642203985"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-20398-5_15","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T15:29:49Z","timestamp":1302103789000},"page":"192-206","source":"Crossref","is-referenced-by-count":21,"title":["Instantiation-Based Invariant Discovery"],"prefix":"10.1007","author":[{"given":"Temesghen","family":"Kahsai","sequence":"first","affiliation":[]},{"given":"Yeting","family":"Ge","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des.\u00a015(1), 75\u201392 (1999)","journal-title":"Form. Methods Syst. Des."},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-36126-X_2","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Das","year":"2002","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 19\u201332. Springer, Heidelberg (2002)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Daskalakis, C., Karp, R.M., Mossel, E., Riesenfeld, S., Verbin, E.: Sorting and selection in posets. In: ACM-SIAM Symposium on Discrete Algorithms, pp. 392\u2013401 (2009)","DOI":"10.1137\/1.9781611973068.44"},{"key":"15_CR5","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Technical report, SRI International (2006)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-93900-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 120\u2013135. Springer, Heidelberg (2009)"},{"key":"15_CR7","first-page":"1","volume-title":"FMCAD 2008","author":"G. Hagen","year":"2008","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of lustre programs with SMT-based techniques. In: FMCAD 2008, Piscataway, NJ, USA, 2008, pp. 1\u20139. IEEE Press, Los Alamitos (2008)"},{"issue":"9","key":"15_CR8","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-40922-X","volume-title":"Formal Methods in Computer-Aided Design","author":"W. Hunt","year":"2000","unstructured":"Hunt, W., Johnson, S., Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 409\u2013426. Springer, Heidelberg (2000)"},{"key":"15_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/11560548_24","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Pandav","year":"2005","unstructured":"Pandav, S., Slind, K., Gopalakrishnan, G.: Counterexample guided invariant discovery for parameterized cache coherence verification. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 317\u2013331. Springer, Heidelberg (2005)"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/1543135.1542501","volume":"44","author":"S. Srivastava","year":"2009","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. SIGPLAN Not.\u00a044, 223\u2013234 (2009)","journal-title":"SIGPLAN Not."},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/BFb0031822","volume-title":"Formal Methods in Computer-Aided Design","author":"J.X. Su","year":"1996","unstructured":"Su, J.X., Dill, D.L., Barrett, C.W.: Automatic generation of invariants in processor verification. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 377\u2013388. Springer, Heidelberg (1996)"},{"key":"15_CR14","first-page":"176","volume-title":"DAC 2010","author":"M. Thalmaier","year":"2010","unstructured":"Thalmaier, M., Nguyen, M.D., Wedler, M., Stoffel, D., Bormann, J., Kunz, W.: Analyzing k-step induction to compute invariants for SAT-based property checking. In: DAC 2010, pp. 176\u2013181. ACM, New York (2010)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A., Rue\u00df, H., Sa\u00efdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 113\u2013127. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T14:53:48Z","timestamp":1558536828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}