{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:06Z","timestamp":1776333426629,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662460801","type":"print"},{"value":"9783662460818","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_15","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T09:25:44Z","timestamp":1418289944000},"page":"263-281","source":"Crossref","is-referenced-by-count":25,"title":["Property Directed Polyhedral Abstraction"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-33125-1_21","volume-title":"Static Analysis","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Craig Interpretation. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 300\u2013316. Springer, Heidelberg (2012)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, Veith (eds.) [27], pp. 313\u2013329","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"15_CR3","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. CoRR, abs\/cs\/0612085 (2006)"},{"issue":"3-4","key":"15_CR4","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/s10009-007-0029-y","volume":"9","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT\u00a09(3-4), 413\u2013414 (2007)","journal-title":"STTT"},{"issue":"1-2","key":"15_CR5","first-page":"259","volume":"5","author":"F. Benoy","year":"2005","unstructured":"Benoy, F., King, A., Mesnard, F.: Computing Convex Hulls with a Linear Solver. TPLP\u00a05(1-2), 259\u2013271 (2005)","journal-title":"TPLP"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"2014","unstructured":"Biere, A., Bloem, R. (eds.): CAV 2014. LNCS, vol.\u00a08559. Springer, Heidelberg (2014)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, Bloem (eds.) [6], pp. 831\u2013848","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"15_CR8","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":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"15_CR9","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.\u00a07358, pp. 277\u2013293. Springer, Heidelberg (2012)"},{"key":"15_CR10","doi-asserted-by":"crossref","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. LNCS, vol.\u00a08413, pp. 46\u201361. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_4"},{"issue":"1","key":"15_CR11","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories. ACM Trans. Comput. Log.\u00a012(1), 7 (2010)","journal-title":"ACM Trans. Comput. Log."},{"issue":"4","key":"15_CR12","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. J. Log. Comput.\u00a02(4), 511\u2013547 (1992)","journal-title":"J. Log. Comput."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) POPL, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A Model-Constructing Satisfiability Calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 1\u201312. Springer, Heidelberg (2013)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"issue":"16","key":"15_CR16","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2010.05.021","volume":"110","author":"B.S. Gulavani","year":"2010","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Refining abstract interpretations. Inf. Process. Lett.\u00a0110(16), 666\u2013671 (2010)","journal-title":"Inf. Process. Lett."},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-15769-1_18","volume-title":"Static Analysis","author":"A. Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Boxes: A Symbolic Abstract Domain of Boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 287\u2013303. Springer, Heidelberg (2010)"},{"key":"15_CR18","unstructured":"Halbwachs, N.: D\u00e9termination automatique de relations lin\u00e9aires v\u00e9rifi\u00e9es par les variables d\u2019un programme. PhD thesis, Grenoble (1979)"},{"key":"15_CR19","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.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-33365-1_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R. Kindermann","year":"2012","unstructured":"Kindermann, R., Junttila, T., Niemel\u00e4, I.: SMT-Based Induction Methods for Timed Systems. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol.\u00a07595, pp. 171\u2013187. Springer, Heidelberg (2012)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-Based Model Checking for Recursive Programs. In: Biere, Bloem (eds.) [6], pp. 17\u201334","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In: Sharygina, Veith (eds.) [27], pp. 846\u2013862","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"15_CR23","series-title":"LNCS(LNAI)","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-22438-6_28","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Korovin","year":"2011","unstructured":"Korovin, K., Voronkov, A.: Solving Systems of Linear Inequalities by Bound Propagation. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS(LNAI), vol.\u00a06803, pp. 369\u2013383. Springer, Heidelberg (2011)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-08867-9_16","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2014","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 243\u2013259. Springer, Heidelberg (2014)"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275501"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P. R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"2013","unstructured":"Sharygina, N., Veith, H. (eds.): CAV 2013. LNCS, vol.\u00a08044. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T00:31:50Z","timestamp":1559089910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}