{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:48Z","timestamp":1751660508178,"version":"3.40.5"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_11","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T09:25:44Z","timestamp":1418289944000},"page":"190-208","source":"Crossref","is-referenced-by-count":6,"title":["Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Caterina","family":"Urban","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static Analysis and Verification of Aerospace Software by Abstract Interpretation. In: AIAA (2010)","DOI":"10.2514\/6.2010-3385"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"T.A. Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving Existentially Quantified Horn Clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"issue":"2","key":"11_CR3","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A. Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. Electronic Notes in Theoretical Computer Science\u00a066(2), 160\u2013177 (2002)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"11_CR4","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An Incremental Approach to Model Checking Progress Properties. In: FMCAD, pp. 144\u2013153 (2011)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation Invariants for Probabilistic Program Loops as Fixed Points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 85\u2013100. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that Programs Eventually do Something Good. In: POPL, pp. 265\u2013276 (2007)","DOI":"10.1145\/1190215.1190257"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E.: Reasoning About Nondeterminism in Programs. In: PLDI, pp. 219\u2013230 (2013)","DOI":"10.1145\/2499370.2491969"},{"key":"11_CR8","first-page":"77","volume":"6","author":"P. Cousot","year":"1997","unstructured":"Cousot, P.: Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. ENTCS\u00a06, 77\u2013102 (1997)","journal-title":"ENTCS"},{"key":"11_CR9","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":"11_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Higher Order Abstract Interpretation and Application to Comportment Analysis Generalizing Strictness, Termination, Projection, and PER Analysis. In: ICCL, pp. 95\u2013112 (1994)","DOI":"10.1109\/ICCL.1994.288389"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An Abstract Interpretation Framework for Termination. In: POPL, pp. 245\u2013258 (2012)","DOI":"10.1145\/2103621.2103687"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning Meanings to Programs. In: Proceedings of Symposium on Applied Mathematics, vol.\u00a019, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Francez, N.: Fairness. Springer (1986)","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A Hierarchy of Temporal Properties. In: PODC, pp. 377\u2013410 (1990)","DOI":"10.1145\/93385.93442"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/3-540-36384-X_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Mass\u00e9","year":"2002","unstructured":"Mass\u00e9, D.: Property Checking Driven Abstract Interpretation-Based Static Analysis. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 56\u201369. Springer, Heidelberg (2002)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-27815-3_28","volume-title":"Algebraic Methodology and Software Technology","author":"D. Mass\u00e9","year":"2004","unstructured":"Mass\u00e9, D.: Abstract Domains for Property Checking Driven Analysis of Temporal Properties. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 349\u2013363. Springer, Heidelberg (2004)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations. In: NSAD. ENTCS, vol.\u00a0287, pp. 89\u2013100 (2012)","DOI":"10.1016\/j.entcs.2012.09.009"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition Invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition Predicate Abstraction and Fair Termination. In: POPL, pp. 132\u2013144 (2005)","DOI":"10.1145\/1047659.1040317"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-38856-9_5","volume-title":"Static Analysis","author":"C. Urban","year":"2013","unstructured":"Urban, C.: The Abstract Domain of Segmented Ranking Functions. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol.\u00a07935, pp. 43\u201362. Springer, Heidelberg (2013)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Urban, C., Min\u00e9, A.: An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol.\u00a08410, pp. 412\u2013431. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Urban, C., Min\u00e9, A.: A Decision Tree Abstract Domain for Proving Conditional Termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 302\u2013318. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_19"},{"issue":"1-2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"M.Y. Vardi","year":"1991","unstructured":"Vardi, M.Y.: Verification of Concurrent Programs: The Automata-Theoretic Framework. Annals of Pure and Applied Logic\u00a051(1-2), 79\u201398 (1991)","journal-title":"Annals of Pure and Applied Logic"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T00:37:08Z","timestamp":1747183028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}