{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:48:44Z","timestamp":1764557324889},"reference-count":51,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T00:00:00Z","timestamp":1415750400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:p>Completeness is a key feature of abstract interpretation. It corresponds to exactness of the abstraction of fix-points and relies upon the need of absence of false alarms in static program analysis. Making abstract interpretation complete is therefore a major problem in approximating the semantics of programming languages. In this paper, we consider the problem of making abstract interpretations complete by minimally modifying the predicate transformer, i.e. the semantics, of a program. We study the mathematical properties of complete functions on complete lattices and prove the existence of minimal transformations of monotone functions to achieve completeness. We then apply minimal complete transformers to prove the minimality of standard program transformations in security, such as static program monitoring.<\/jats:p>","DOI":"10.1017\/s0960129514000358","type":"journal-article","created":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T08:36:16Z","timestamp":1415781376000},"page":"658-701","source":"Crossref","is-referenced-by-count":8,"title":["Making abstract models complete"],"prefix":"10.1017","volume":"26","author":[{"given":"ROBERTO","family":"GIACOBAZZI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ISABELLA","family":"MASTROENI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,12]]},"reference":[{"key":"S0960129514000358_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"S0960129514000358_ref46","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl035"},{"key":"S0960129514000358_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90074-J"},{"key":"S0960129514000358_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30114-1_15"},{"key":"S0960129514000358_ref36","first-page":"221","article-title":"Residuated closure operators.","volume":"26","author":"Janowitz","year":"1967","journal-title":"Portuguese Mathematical"},{"key":"S0960129514000358_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_20"},{"key":"S0960129514000358_ref9","first-page":"238","volume-title":"Proceedings of Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL'77)","author":"Cousot","year":"1977"},{"key":"S0960129514000358_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00313-3"},{"key":"S0960129514000358_ref40","first-page":"147","article-title":"Deriving bisimulations by simplifying partitions.","volume":"4905","author":"Mastroeni","year":"2008","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129514000358_ref37","first-page":"101","volume-title":"ICIP 2007: IEEE International Conference on Image Processing","author":"Kihara","year":"2007"},{"key":"S0960129514000358_ref20","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0345"},{"key":"S0960129514000358_ref16","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1145\/964001.964016","volume-title":"Conference Record of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Venice, Italy","author":"Cousot","year":"2004"},{"key":"S0960129514000358_ref11","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"S0960129514000358_ref44","first-page":"177","article-title":"A functional taxonomy for software watermarking.","volume":"24","author":"Nagra","year":"2002","journal-title":"Australian Computer Science Communications"},{"key":"S0960129514000358_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_12"},{"key":"S0960129514000358_ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027797"},{"key":"S0960129514000358_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"S0960129514000358_ref51","doi-asserted-by":"publisher","DOI":"10.2307\/1968865"},{"key":"S0960129514000358_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"S0960129514000358_ref32","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2724"},{"key":"S0960129514000358_ref31","first-page":"177","volume-title":"Science of Computer Programming","volume":"32","author":"Giacobazzi","year":"1998"},{"key":"S0960129514000358_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63165-8_230"},{"key":"S0960129514000358_ref5","volume-title":"Surreptitious Software","author":"Collberg","year":"2010"},{"key":"S0960129514000358_ref41","first-page":"665","article-title":"An abstract interpretation-based model for safety semantics.","volume":"88","author":"Mastroeni","year":"2011","journal-title":"Journal of Computer Mathematics"},{"key":"S0960129514000358_ref13","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"S0960129514000358_ref39","first-page":"299","article-title":"Algebraic power analysis by abstract interpretation.","volume":"17","author":"Mastroeni","year":"2004","journal-title":"Higher-Order and Symbolic Computation (HOSC)"},{"key":"S0960129514000358_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45496-9_12"},{"key":"S0960129514000358_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_1"},{"key":"S0960129514000358_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190270"},{"key":"S0960129514000358_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"S0960129514000358_ref42","first-page":"179","volume-title":"Proceedings of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM'93)","author":"Mycroft","year":"1993"},{"key":"S0960129514000358_ref15","first-page":"178","volume-title":"Proceedings of Conference Record of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Cousot","year":"2002"},{"key":"S0960129514000358_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"S0960129514000358_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_24"},{"key":"S0960129514000358_ref49","first-page":"327","volume-title":"Proceedings of the 37th ACM SIGPLAN-SIGACT POPL 2010","author":"Vechev","year":"2010"},{"key":"S0960129514000358_ref25","first-page":"7","volume-title":"Proceedings of The 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08)","author":"Giacobazzi","year":"2008"},{"key":"S0960129514000358_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6"},{"key":"S0960129514000358_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964017"},{"key":"S0960129514000358_ref17","first-page":"1","article-title":"Combination of abstractions in the Astr\u00e9e static analyzer.","volume":"4435","author":"Cousot","year":"2007","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"S0960129514000358_ref26","first-page":"179","volume-title":"Proceedings of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM'12)","author":"Giacobazzi","year":"2012"},{"key":"S0960129514000358_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292569"},{"key":"S0960129514000358_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_34"},{"key":"S0960129514000358_ref22","volume-title":"Introduction to Lattices and Order","author":"Davey","year":"1990"},{"key":"S0960129514000358_ref1","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky","year":"1994"},{"key":"S0960129514000358_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_21"},{"key":"S0960129514000358_ref23","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/335169.335201","volume-title":"NSPW'99","author":"Erlingsson","year":"1999"},{"key":"S0960129514000358_ref12","first-page":"269","volume-title":"Proceedings of Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL'79)","author":"Cousot","year":"1979"},{"key":"S0960129514000358_ref3","volume-title":"Residuation Theory","author":"Blyth","year":"1972"},{"key":"S0960129514000358_ref10","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","year":"1979","journal-title":"Portuguese Mathematical"},{"key":"S0960129514000358_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"S0960129514000358_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234742"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000358","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T02:23:38Z","timestamp":1689647018000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000358\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,12]]},"references-count":51,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["S0960129514000358"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000358","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,12]]}}}