{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:33:52Z","timestamp":1750221232509,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209169","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"175-184","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Sound up-to techniques and Complete abstract domains"],"prefix":"10.1145","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[{"name":"University of Pisa, Pisa, Italy"}]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Pozuelo de Alarc\u00f3n, Spain"}]},{"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Pozuelo de Alarc\u00f3n, Spain and University of Verona, Verona, Italy"}]},{"given":"Dusko","family":"Pavlovic","sequence":"additional","affiliation":[{"name":"University of Hawaii, Honolulu, Hawaii, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Hopcroft","author":"Aho Alfred V.","year":"1974","unstructured":"Alfred V. Aho and John E . Hopcroft . 1974 . The Design and Analysis of Computer Algorithms (1st ed.). Addison-Wesley Longman Publishing Co. , Inc. Alfred V. Aho and John E. Hopcroft. 1974. The Design and Analysis of Computer Algorithms (1st ed.). Addison-Wesley Longman Publishing Co., Inc."},{"volume-title":"Language Engineering and Rigorous Software Development. LNCS","author":"Bertot Yves","key":"e_1_3_2_1_2_1","unstructured":"Yves Bertot . 2009. Structural abstract interpretation: A formal study using Coq . In Language Engineering and Rigorous Software Development. LNCS , Vol. 5520 . Springer , 153--194. Yves Bertot. 2009. Structural abstract interpretation: A formal study using Coq. In Language Engineering and Rigorous Software Development. LNCS, Vol. 5520. Springer, 153--194."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209169"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_3_2_1_5_1","first-page":"339","article-title":"Graphes canoniques de graphes alg\u00e9briques","volume":"24","author":"Caucal Didier","year":"1990","unstructured":"Didier Caucal . 1990 . Graphes canoniques de graphes alg\u00e9briques . ITA 24 , 4 (1990), 339 -- 352 . http:\/\/www.numdam.org\/item?id=ITA_1990_24_4_339_0 Didier Caucal. 1990. Graphes canoniques de graphes alg\u00e9briques. ITA 24, 4 (1990), 339--352. http:\/\/www.numdam.org\/item?id=ITA_1990_24_4_339_0","journal-title":"ITA"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263744"},{"key":"e_1_3_2_1_7_1","volume-title":"Partial Completeness of Abstract Fixpoint Checking. In SARA: Int. Symp. on Abstraction, Reformulation, and Approximation. Springer, 1--25","author":"Cousot Patrick","year":"2000","unstructured":"Patrick Cousot . 2000 . Partial Completeness of Abstract Fixpoint Checking. In SARA: Int. Symp. on Abstraction, Reformulation, and Approximation. Springer, 1--25 . Patrick Cousot. 2000. Partial Completeness of Abstract Fixpoint Checking. In SARA: Int. Symp. on Abstraction, Reformulation, and Approximation. Springer, 1--25."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_9_1","first-page":"185","article-title":"A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice","volume":"38","author":"Cousot Patrick","year":"1979","unstructured":"Patrick Cousot and Radhia Cousot . 1979 . A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice . Portug. Math. 38 , 2 (1979), 185 -- 198 . Patrick Cousot and Radhia Cousot. 1979. A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice. Portug. Math. 38, 2 (1979), 185--198.","journal-title":"Portug. Math."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008649901864"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_1_13_1","volume-title":"Fixpoint-Guided Abstraction Refinements. In SAS:14th Int. Static Analysis Symp. (LNCS)","volume":"4634","author":"Cousot Patrick","year":"2007","unstructured":"Patrick Cousot , Pierre Ganty , and Jean-Fran\u00e7ois Raskin . 2007 . Fixpoint-Guided Abstraction Refinements. In SAS:14th Int. Static Analysis Symp. (LNCS) , Vol. 4634 . Springer, 333--348. Patrick Cousot, Pierre Ganty, and Jean-Fran\u00e7ois Raskin. 2007. Fixpoint-Guided Abstraction Refinements. In SAS:14th Int. Static Analysis Symp. (LNCS), Vol. 4634. Springer, 333--348."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158131"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"B. A. Davey and H. A. Priestley. 2002. Introduction to Lattices and Order (2 ed.). Cambridge University Press.  B. A. Davey and H. A. Priestley. 2002. Introduction to Lattices and Order (2 ed.). Cambridge University Press.","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_3_2_1_16_1","volume-title":"Static Contract Checking with Abstract Interpretation. In Int. Conf. on Formal Verification of Object-oriented Software (FoVeOOS'10)","author":"F\u00e4hndrich Manuel","year":"2011","unstructured":"Manuel F\u00e4hndrich and Francesco Logozzo . 2011 . Static Contract Checking with Abstract Interpretation. In Int. Conf. on Formal Verification of Object-oriented Software (FoVeOOS'10) . Springer-Verlag, Berlin, Heidelberg, 10--30. Manuel F\u00e4hndrich and Francesco Logozzo. 2011. Static Contract Checking with Abstract Interpretation. In Int. Conf. on Formal Verification of Object-oriented Software (FoVeOOS'10). Springer-Verlag, Berlin, Heidelberg, 10--30."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718288"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_3_2_1_23_1","volume-title":"Types-The 2014 Types Meeting.","author":"Leroy Xavier","year":"2014","unstructured":"Xavier Leroy . 2014 . Formal verification of a static analyzer: abstract interpretation in type theory . In Types-The 2014 Types Meeting. Xavier Leroy. 2014. Formal verification of a static analyzer: abstract interpretation in type theory. In Types-The 2014 Types Meeting."},{"volume-title":"Communication and Concurrency","author":"Milner Robert","key":"e_1_3_2_1_24_1","unstructured":"Robert Milner . 1989. Communication and Concurrency . Prentice Hall . Robert Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.11"},{"volume-title":"Machine Intelligence","author":"Park David M.R.","key":"e_1_3_2_1_26_1","unstructured":"David M.R. Park . 1969. Fixpoint induction and proofs of program properties . In Machine Intelligence , Vol. 5 . Edinburgh Univ. Press , 59--78. David M.R. Park. 1969. Fixpoint induction and proofs of program properties. In Machine Intelligence, Vol. 5. Edinburgh Univ. Press, 59--78."},{"key":"e_1_3_2_1_27_1","volume-title":"The largest respectful function. arXiv preprint arXiv:1605.04136","author":"Parrow Joachim","year":"2016","unstructured":"Joachim Parrow and Tjark Weber . 2016. The largest respectful function. arXiv preprint arXiv:1605.04136 ( 2016 ). Joachim Parrow and Tjark Weber. 2016. The largest respectful function. arXiv preprint arXiv:1605.04136 (2016)."},{"key":"e_1_3_2_1_28_1","volume-title":"Complete Lattices and Up-To Techniques. In APLAS: Asian Symposium on Programming Languages and Systems (LNCS)","volume":"4807","author":"Pous Damien","year":"2007","unstructured":"Damien Pous . 2007 . Complete Lattices and Up-To Techniques. In APLAS: Asian Symposium on Programming Languages and Systems (LNCS) , Vol. 4807 . Springer, 351--366. Damien Pous. 2007. Complete Lattices and Up-To Techniques. In APLAS: Asian Symposium on Programming Languages and Systems (LNCS), Vol. 4807. Springer, 351--366."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934564"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Damien Pous. 2016. Coq libraries for \"Coinduction all the way up\". http:\/\/perso.ens-lyon.fr\/damien.pous\/cawu\/. (2016).  Damien Pous. 2016. Coq libraries for \"Coinduction all the way up\". http:\/\/perso.ens-lyon.fr\/damien.pous\/cawu\/. (2016).","DOI":"10.1145\/2933575.2934564"},{"volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous Damien","key":"e_1_3_2_1_31_1","unstructured":"Damien Pous and Davide Sangiorgi . 2012. Enhancements of the bisimulation proof method . In Advanced Topics in Bisimulation and Coinduction . Cambridge University Press , 233--289. Damien Pous and Davide Sangiorgi. 2012. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 233--289."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787548"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl035"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.8"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"e_1_3_2_1_36_1","unstructured":"VERASCO. 2015. A Formally-Verified Static Analyzer for C. http:\/\/compcert.inria.fr\/verasco\/. (2015).  VERASCO. 2015. A Formally-Verified Static Analyzer for C. http:\/\/compcert.inria.fr\/verasco\/. (2015)."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968865"}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Oxford United Kingdom","acronym":"LICS '18"},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209169","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209169","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:08Z","timestamp":1750212428000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209169"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":35,"alternative-id":["10.1145\/3209108.3209169","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209169","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}