{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:35Z","timestamp":1763468255870,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_40","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"583-602","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Property-Directed Inference of Universal Invariants or Proving Their Absence"],"prefix":"10.1007","author":[{"given":"A.","family":"Karbyshev","sequence":"first","affiliation":[]},{"given":"N.","family":"Bj\u00f8rner","sequence":"additional","affiliation":[]},{"given":"S.","family":"Itzhaky","sequence":"additional","affiliation":[]},{"given":"N.","family":"Rinetzky","sequence":"additional","affiliation":[]},{"given":"S.","family":"Shoham","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"40_CR1","unstructured":"The Open Networking Foundation. http:\/\/opennetworking.org"},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. CoRR, abs\/1501.04100 (2015)","DOI":"10.1007\/978-3-662-46669-8_26"},{"key":"40_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-642-31424-7_49","volume-title":"Computer Aided Verification","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679\u2013685. Springer, Heidelberg (2012)"},{"key":"40_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"40_CR5","first-page":"118","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 118\u2013149 (2003)","journal-title":"Adv. Comput."},{"key":"40_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"40_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"831","DOI":"10.1007\/978-3-319-08867-9_55","volume-title":"Computer Aided Verification","author":"J Birgmeier","year":"2014","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831\u2013848. Springer, Heidelberg (2014)"},{"key":"40_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013)"},{"key":"40_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"40_CR10","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Model Theory","author":"C Chang","year":"1990","unstructured":"Chang, C., Keisler, H.: Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, New York (1990)"},{"key":"40_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277\u2013293. Springer, Heidelberg (2012)"},{"key":"40_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014)"},{"key":"40_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of the 40th Annual Design Automation Conference, DAC 2003, pp. 368\u2013371. ACM, New York, NY, USA (2003)","DOI":"10.1145\/775832.775928"},{"key":"40_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012)"},{"key":"40_CR15","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Mebsout, A., Za\u00efdi, F.: Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 61\u201368. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"40_CR16","volume-title":"Introduction To Algorithms","author":"T Cormen","year":"1990","unstructured":"Cormen, T., Leiserson, C., Rivest, R.: Introduction To Algorithms. MIT Press, Cambridge (1990)"},{"key":"40_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"40_CR18","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. 2517, pp. 19\u201332. Springer, Heidelberg (2002)"},{"key":"40_CR19","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 Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"40_CR20","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Symbolic heap abstraction with demand-driven axiomatization of memory invariants. In: Cook, W.R., Clarke, S.. Rinard, M.C. (eds.) ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 397\u2013410. ACM (2010)","DOI":"10.1145\/1932682.1869493"},{"key":"40_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"40_CR22","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: FMCAD (2011)"},{"key":"40_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., M. Leino, K.R.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"issue":"1","key":"40_CR24","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/565816.503291","volume":"37","author":"C Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. SIGPLAN Not. 37(1), 191\u2013202 (2002)","journal-title":"SIGPLAN Not."},{"key":"40_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1007\/978-3-642-39799-8_57","volume-title":"Computer Aided Verification","author":"P Garg","year":"2013","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: Learning\u00a0universally\u00a0quantified\u00a0invariants of linear\u00a0data\u00a0structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 813\u2013829. Springer, Heidelberg (2013)"},{"key":"40_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-38856-9_11","volume-title":"Static Analysis","author":"P Garg","year":"2013","unstructured":"Garg, P., Madhusudan, P., Parlato, G.: Quantified data automata on skinny trees: an abstract domain for lists. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 172\u2013193. Springer, Heidelberg (2013)"},{"issue":"4","key":"40_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-6(4:10)2010","volume":"6","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4), 1\u201348 (2010)","journal-title":"Log. Methods Comput. Sci."},{"key":"40_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 22\u201329. Springer, Heidelberg (2010)"},{"key":"40_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"40_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-19835-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Invariant generation in vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 60\u201364. Springer, Heidelberg (2011)"},{"key":"40_CR31","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)"},{"key":"40_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"issue":"1","key":"40_CR33","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1297658.1297662","volume":"9","author":"SK Lahiri","year":"2007","unstructured":"Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Logic 9(1), 4 (2007). doi: 10.1145\/1297658.1297662","journal-title":"ACM Trans. Comput. Logic"},{"key":"40_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/11817963_49","volume-title":"Computer Aided Verification","author":"T Lev-Ami","year":"2006","unstructured":"Lev-Ami, T., Immerman, N., Sagiv, M.: Abstraction for shape analysis with fast and precise transformers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 547\u2013561. Springer, Heidelberg (2006)"},{"key":"40_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"40_CR36","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: POPL (2010)","DOI":"10.1145\/1706299.1706330"},{"issue":"3","key":"40_CR37","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"40_CR38","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI, pp. 223\u2013234 (2009)","DOI":"10.1145\/1543135.1542501"},{"key":"40_CR39","unstructured":"Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: attaining most-precise inductive invariants. TR-1790, Computer Science Department, University of Wisconsin, Madison, WI, April 2013"},{"key":"40_CR40","unstructured":"Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: automating abstract interpretation. Electronic Notes in Theoretical Computer Science (2013)"},{"key":"40_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"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-319-21690-4_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T03:09:37Z","timestamp":1652843377000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}