{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T10:34:31Z","timestamp":1725878071666},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_10","type":"book-chapter","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T04:52:06Z","timestamp":1484110326000},"page":"169-186","source":"Crossref","is-referenced-by-count":0,"title":["Complete Abstractions and Subclassical Modal Logics"],"prefix":"10.1007","author":[{"given":"Vijay","family":"D\u2019Silva","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo","family":"Sousa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"issue":"1\u20132","key":"10_CR1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"PA Abdulla","year":"2000","unstructured":"Abdulla, P.A., \u010cer\u00e4ns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1\u20132), 109\u2013127 (2000)","journal-title":"Inf. Comput."},{"key":"10_CR2","unstructured":"Abramsky, S.: Domain Theory and the Logic of Observable Properties. Ph.d. thesis, University of London (1987)"},{"issue":"1","key":"10_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1305\/ndjfl\/1039700693","volume":"38","author":"SA Celani","year":"1997","unstructured":"Celani, S.A., Jansana, R.: A new semantics for positive modal logic. Notre Dame J. Formal Logic 38(1), 1\u201318 (1997)","journal-title":"Notre Dame J. Formal Logic"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-69850-0_12","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196\u2013215. Springer, Berlin (2008). doi: 10.1007\/978-3-540-69850-0_12"},{"issue":"2\u20133","key":"10_CR5","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2\u20133), 103\u2013179 (1992)","journal-title":"J. Logic Program."},{"key":"10_CR6","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"P Cousot","year":"1981","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, pp. 303\u2013342. Prentice-Hall Inc, Englewood Cliffs (1981). Chap. 10"},{"key":"10_CR7","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: Proceedings of the Principles of Programming Languages, pp. 238\u2013252. ACM, New York (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Principles of Programming Languages, pp. 269\u2013282. ACM, New York (1979)","DOI":"10.1145\/567752.567778"},{"key":"10_CR9","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"V D\u2019Silva","year":"2013","unstructured":"D\u2019Silva, V.: Generalizing simulation to abstract domains. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052. Springer, Heidelberg (2013)"},{"issue":"2","key":"10_CR11","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/BF01061239","volume":"55","author":"JM Dunn","year":"1995","unstructured":"Dunn, J.M.: Positive modal logic. Stud. Logica 55(2), 301\u2013317 (1995)","journal-title":"Stud. Logica"},{"issue":"3","key":"10_CR12","doi-asserted-by":"crossref","first-page":"713","DOI":"10.2178\/jsl\/1122038911","volume":"70","author":"JM Dunn","year":"2005","unstructured":"Dunn, J.M., Gehrke, M., Palmigiano, A.: Canonical extensions and relational completeness of some substructural logics. J. Symbolic Logic 70(3), 713\u2013740 (2005)","journal-title":"J. Symbolic Logic"},{"issue":"1\u20132","key":"10_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10_CR14","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/s11225-006-9008-7","volume":"84","author":"M Gehrke","year":"2006","unstructured":"Gehrke, M.: Generalized Kripke frames. Stud. Logica. 84(2), 241\u2013275 (2006)","journal-title":"Stud. Logica."},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356\u2013373. Springer, Berlin (2001). doi: 10.1007\/3-540-47764-0_20"},{"issue":"1\u20133","key":"10_CR16","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0167-6423(97)00034-8","volume":"32","author":"R Giacobazzi","year":"1998","unstructured":"Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program. 32(1\u20133), 177\u2013210 (1998)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"10_CR17","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361\u2013416 (2000)","journal-title":"J. ACM"},{"issue":"1","key":"10_CR18","doi-asserted-by":"crossref","first-page":"127","DOI":"10.2307\/2372074","volume":"74","author":"B J\u00f3nsson","year":"1952","unstructured":"J\u00f3nsson, B., Tarski, A.: Boolean algebras with operators. Am. J. Math. 74(1), 127\u2013162 (1952)","journal-title":"Am. J. Math."},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the Principles of Programming Languages, pp. 194\u2013206. ACM, New York (1973)","DOI":"10.1145\/512927.512945"},{"issue":"1","key":"10_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S Kripke","year":"1959","unstructured":"Kripke, S.: A completeness theorem in modal logic. J. Symbolic Logic 24(1), 1\u201314 (1959)","journal-title":"J. Symbolic Logic"},{"issue":"1","key":"10_CR21","doi-asserted-by":"crossref","first-page":"46","DOI":"10.2307\/2270619","volume":"31","author":"EJ Lemmon","year":"1966","unstructured":"Lemmon, E.J.: Algebraic semantics for modal logics I. J. Symbolic Logic 31(1), 46\u201365 (1966)","journal-title":"J. Symbolic Logic"},{"issue":"2","key":"10_CR22","doi-asserted-by":"crossref","first-page":"191","DOI":"10.2307\/2269810","volume":"31","author":"EJ Lemmon","year":"1966","unstructured":"Lemmon, E.J.: Algebraic semantics for modal logics II. J. Symbolic Logic 31(2), 191\u2013218 (1966)","journal-title":"J. Symbolic Logic"},{"issue":"2","key":"10_CR23","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/2850413","volume":"63","author":"L Libkin","year":"2016","unstructured":"Libkin, L., Martens, W., Vrgo\u010d, D.: Querying graphs with data. J. ACM 63(2), 14:1\u201314:53 (2016)","journal-title":"J. ACM"},{"issue":"1","key":"10_CR24","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Meth. Syst. Des. 6(1), 11\u201344 (1995)","journal-title":"Formal Meth. Syst. Des."},{"key":"10_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"10_CR26","unstructured":"Nguyen, L.A.: On the complexity of fragments of modal logics. In: Advances in Modal Logic. vol. 5, pp. 249\u2013268. Kings College Publications (2005)"},{"key":"10_CR27","unstructured":"Pratt, V.: Chu spaces. Course notes for the School in Category Theory and Applications, July 1999"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). doi: 10.1007\/3-540-11494-7_22"},{"issue":"1","key":"10_CR29","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1093\/logcom\/exl035","volume":"17","author":"F Ranzato","year":"2007","unstructured":"Ranzato, F., Tapparo, F.: Generalized strong preservation by abstract interpretation. J. Logic Comput. 17(1), 157\u2013197 (2007)","journal-title":"J. Logic Comput."},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-78163-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"DA Schmidt","year":"2008","unstructured":"Schmidt, D.A.: Internal and external logics of abstract interpretations. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 263\u2013278. Springer, Berlin (2008). doi: 10.1007\/978-3-540-78163-9_23"},{"key":"10_CR31","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.tcs.2012.01.002","volume":"430","author":"DA Schmidt","year":"2012","unstructured":"Schmidt, D.A.: Inverse-limit and topological aspects of abstract interpretation. Theor. Comput. Sci. 430, 23\u201342 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-642-27940-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Zufferey","year":"2012","unstructured":"Zufferey, D., Wies, T., Henzinger, T.A.: Ideal abstractions for well-structured transition systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 445\u2013460. Springer, Berlin (2012). doi: 10.1007\/978-3-642-27940-9_29"}],"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-319-52234-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T07:53:54Z","timestamp":1498377234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}