{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:37:30Z","timestamp":1770291450185,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662545768","type":"print"},{"value":"9783662545775","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54577-5_5","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"76-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Bounded Quantifier Instantiation for Checking Inductive Invariants"],"prefix":"10.1007","author":[{"given":"Yotam M. Y.","family":"Feldman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"5_CR1","unstructured":"Extended version. http:\/\/www.cs.tau.ac.il\/research\/yotam.feldman\/papers\/tacas17\/tacas17_extended.pdf"},{"key":"5_CR2","unstructured":"Full code materials. http:\/\/www.cs.tau.ac.il\/research\/yotam.feldman\/papers\/tacas17\/examples_code.zip"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 1\u201322 (2015). http:\/\/dx.doi.org\/10.1007\/s10009-015-0406-x","DOI":"10.1007\/s10009-015-0406-x"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476\u2013495. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-35873-9_28"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10936-7_1","volume-title":"Static Analysis","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: Block me if you can!. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 1\u201317. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-10936-7_1"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: VeriCon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09\u201311 June 2014, pp. 31 (2014)","DOI":"10.1145\/2594291.2594317"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-21668-3_6","volume-title":"Computer Aided Verification","author":"K Bansal","year":"2015","unstructured":"Bansal, K., Reynolds, A., King, T., Barrett, C., Wies, T.: Deciding local theory extensions via E-matching. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 87\u2013105. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_6"},{"key":"5_CR8","unstructured":"Bj\u00f8rner, N.: Personal communication (2017)"},{"key":"5_CR9","series-title":"Perspectives in Mathematical Logic","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Berlin (1997)"},{"issue":"5","key":"5_CR10","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E Chang","year":"1979","unstructured":"Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979)","journal-title":"Commun. ACM"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"5_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, 17\u201319 June 2002, pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"issue":"1\u20132","key":"5_CR14","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s10472-009-9153-6","volume":"55","author":"Y Ge","year":"2009","unstructured":"Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1\u20132), 101\u2013122 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02658-4_25"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP, pp. 1\u201317 (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). doi:10.1007\/3-540-60630-0_5"},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1015178417181","volume":"70","author":"I Hodkinson","year":"2002","unstructured":"Hodkinson, I.: Loosely guarded fragment of first-order logic has the finite model property. Stud. Logica. 70(2), 205\u2013240 (2002)","journal-title":"Stud. Logica."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: 14th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6 2008. Proceedings, pp. 265\u2013281 (2008)","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160\u2013174. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-30124-0_15"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1007\/978-3-642-39799-8_53","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2013","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756\u2013772. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_53"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-08867-9_3","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2014","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35\u201351. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_3"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-21690-4_40","volume-title":"Computer Aided Verification","author":"A Karbyshev","year":"2015","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 583\u2013602. Springer, Cham (2015). doi:10.1007\/978-3-319-21690-4_40"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11\u201313 January 2006, pp. 115\u2013126 (2006)","DOI":"10.1145\/1111320.1111048"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, 7\u201312 January 2008, pp. 171\u2013182 (2008)","DOI":"10.1145\/1328897.1328461"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-17511-4_20"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-41528-4_20","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2016","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 361\u2013381. Springer, Cham (2016). doi:10.1007\/978-3-319-41528-4_20"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: a system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280\u2013301. Springer, Heidelberg (2000). doi:10.1007\/978-3-540-45099-3_15"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13\u201317 June 2016, pp. 614\u2013630 (2016)","DOI":"10.1145\/2980983.2908118"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, 16\u201319 June 2013, pp. 231\u2013242 (2013)","DOI":"10.1145\/2499370.2462169"},{"issue":"1","key":"5_CR31","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"s2\u201330","author":"FP Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. Lond. Math. Soc. s2\u201330(1), 264\u2013286 (1930)","journal-title":"Proc. Lond. Math. Soc."},{"issue":"6","key":"5_CR32","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/1749608.1749613","volume":"32","author":"TW Reps","year":"2010","unstructured":"Reps, T.W., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. 32(6), 24:1\u201324:55 (2010)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_42"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 377\u2013391. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38574-2_26"},{"issue":"3","key":"5_CR35","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219\u2013234. Springer, Heidelberg (2005). doi:10.1007\/11532231_16"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54577-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T22:43:40Z","timestamp":1692744220000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}