{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:54Z","timestamp":1762458594069,"version":"3.41.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"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":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,10]]},"abstract":"<jats:p>One proposal for automatic construction of proofs about programs is to combine Hoare logic and abstract interpretation. Constructing proofs is in Hoare logic. Discovering programs' invariants is done by abstract interpreters.<\/jats:p>\n          <jats:p>One problem of this approach is that abstract interpreters often compute invariants that are not needed for the proof goal. The reason is that the abstract interpreter does not know what the proof goal is, so it simply tries to find as strong invariants as possible. These unnecessary invariants increase the size of the constructed proofs. Unless the proof-construction phase is notified which invariants are not needed, it blindly proves all the computed invariants.<\/jats:p>\n          <jats:p>\n            In this article, we present a framework for designing algorithms, called\n            <jats:italic>abstract-value slicers<\/jats:italic>\n            , that slice out unnecessary invariants from the results of forward abstract interpretation. The framework provides a generic abstract-value slicer that can be instantiated into a slicer for a particular abstract interpretation. Such an instantiated abstract-value slicer works as a post-processor to an abstract interpretation in the whole proof-construction process, and notifies to the next proof-construction phase which invariants it does not have to prove. Using the framework, we designed an abstract-value slicer for an existing relational analysis and applied it on programs. In this experiment, the slicer identified 62%--81% of the computed invariants as unnecessary, and resulted in 52%--84% reduction in the size of constructed proofs.\n          <\/jats:p>","DOI":"10.1145\/1286821.1286830","type":"journal-article","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T14:26:02Z","timestamp":1195136762000},"page":"39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Goal-directed weakening of abstract interpretation results"],"prefix":"10.1145","volume":"29","author":[{"given":"Sunae","family":"Seo","sequence":"first","affiliation":[{"name":"Korea Advanced Institute of Science and Technology, Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taisook","family":"Han","sequence":"additional","affiliation":[{"name":"Korea Advanced Institute of Science and Technology, Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325727"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science (LNCS)","volume":"2057","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S. K . 2001. Automatically validating temporal safety properties of interfaces . In Proceedings of the SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science (LNCS) , vol. 2057 . Springer-Verlag, 103--122. Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science (LNCS), vol. 2057. Springer-Verlag, 103--122."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science","volume":"4421","author":"Besson F.","unstructured":"Besson , F. , Jensen , T. , and Turphin , T . 2007. Small witnesses for abstract interpretation-based proofs . In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science , vol. 4421 . Springer-Verlag, 268--283. Besson, F., Jensen, T., and Turphin, T. 2007. Small witnesses for abstract interpretation-based proofs. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4421. Springer-Verlag, 268--283."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155095"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science","volume":"1855","author":"Clarke E. M.","unstructured":"Clarke , E. M. , Grumberg , O. , Jha , S. , Lu , Y. , and Veith , H . 2000. Counterexample-Guided abstraction refinement . In Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science , vol. 1855 . Springer-Verlag, 154--169. Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-Guided abstraction refinement. In Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, 154--169."},{"key":"e_1_2_1_8_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00137-0"},{"key":"e_1_2_1_10_1","first-page":"303","article-title":"Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Inc., Englewood Cliffs, NJ","volume":"10","author":"Cousot P.","year":"1981","unstructured":"Cousot , P. 1981 . Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Inc., Englewood Cliffs, NJ , Chapter 10 , 303 -- 342 . Cousot, P. 1981. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Inc., Englewood Cliffs, NJ, Chapter 10, 303--342.","journal-title":"Chapter"},{"volume-title":"Course notes for the NATO International Summer School Marktoberdorf (Germany) on Calculational System Design","author":"Cousot P.","key":"e_1_2_1_11_1","unstructured":"Cousot , P. 1998. The calculational design of a generic abstract interpreter . In Course notes for the NATO International Summer School Marktoberdorf (Germany) on Calculational System Design , M. Broy and R. Steinbr\u00fcggen, Eds. NATO ASI Series F. IOS Press , Amsterdam . Cousot, P. 1998. The calculational design of a generic abstract interpreter. In Course notes for the NATO International Summer School Marktoberdorf (Germany) on Calculational System Design, M. Broy and R. Steinbr\u00fcggen, Eds. NATO ASI Series F. IOS Press, Amsterdam."},{"key":"e_1_2_1_12_1","unstructured":"Cousot P. 2005. Abstract interpretation. MIT course 16.399 http:\/\/web.mit.edu\/16.399\/www\/.  Cousot P. 2005. Abstract interpretation. MIT course 16.399 http:\/\/web.mit.edu\/16.399\/www\/."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008649901864"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"e_1_2_1_17_1","unstructured":"Davey D. A. and Priestley H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.  Davey D. A. and Priestley H. A. 1990. Introduction to Lattices and Order. Cambridge University Press."},{"volume-title":"Functional Programming: Proceedings of the 1989 Glasgow Workshop. Springer-Verlag, 12--30","author":"Davis K.","key":"e_1_2_1_18_1","unstructured":"Davis , K. and Wadler , P. L . 1990. Backwards strictness analysis: Proved and improved . In Functional Programming: Proceedings of the 1989 Glasgow Workshop. Springer-Verlag, 12--30 . Davis, K. and Wadler, P. L. 1990. Backwards strictness analysis: Proved and improved. In Functional Programming: Proceedings of the 1989 Glasgow Workshop. Springer-Verlag, 12--30."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199461"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234742"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964017"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science","volume":"1256","author":"Giacobazzi R.","unstructured":"Giacobazzi , R. and Ranzato , F . 1997. Refining and compressing abstract domains . In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science , vol. 1256 . Springer-Verlag, 771--781. Giacobazzi, R. and Ranzato, F. 1997. Refining and compressing abstract domains. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, 771--781."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00194-7"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/293677.293680"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science","volume":"1254","author":"Graf S.","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with pvs . In Proceedings of the International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science , vol. 1254 . Springer-Verlag, 72--83. Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with pvs. In Proceedings of the International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, 72--83."},{"volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, 89--100","author":"Hamid N.","key":"e_1_2_1_27_1","unstructured":"Hamid , N. , Shaoi , Z. , Trifonov , V. , Monnier , S. , and Ni , Z . 2002. A syntactic approach to foundational proof-carrying code . In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, 89--100 . Hamid, N., Shaoi, Z., Trifonov, V., Monnier, S., and Ni, Z. 2002. A syntactic approach to foundational proof-carrying code. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, 89--100."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science","volume":"2648","author":"Henzinger T.","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , and Sutre , G . 2003. Software verification with blast . In Proceedings of the SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science , vol. 2648 . Springer-Verlag, 235--239. Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with blast. In Proceedings of the SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 2648. Springer-Verlag, 235--239."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_31_1","volume-title":"Program Development in Computational Logic. Lecture Notes in Computer Science","volume":"3049","author":"Howe J. M.","unstructured":"Howe , J. M. , King , A. , and Lu , L . 2004. Analysing logic programs by reasoning backwards . In Program Development in Computational Logic. Lecture Notes in Computer Science , vol. 3049 . Springer-Verlag, 152--188. Howe, J. M., King, A., and Lu, L. 2004. Analysing logic programs by reasoning backwards. In Program Development in Computational Logic. Lecture Notes in Computer Science, vol. 3049. Springer-Verlag, 152--188."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation. Elsevier, 187--208","author":"Hughes J.","year":"1988","unstructured":"Hughes , J. 1988 . Backwards analysis of functional programs . In Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation. Elsevier, 187--208 . Hughes, J. 1988. Backwards analysis of functional programs. In Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation. Elsevier, 187--208."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science","volume":"582","author":"Hughes J.","unstructured":"Hughes , J. and Launchbury , J . 1992. Reversing abstract interpretations . In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science , vol. 582 . Springer-Verlag, 269--286. Hughes, J. and Launchbury, J. 1992. Reversing abstract interpretations. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 582. Springer-Verlag, 269--286."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001436"},{"key":"e_1_2_1_35_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 2nd Symposium on Programs as Data Objects (PADO)","author":"Mass\u00e9 D.","unstructured":"Mass\u00e9 , D. 2001. Combining forward and backward analyses of temporal properties . In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO) . Lecture Notes in Computer Science , vol. 2053 . Springer-Verlag , 103--116. Mass\u00e9, D. 2001. Combining forward and backward analyses of temporal properties. In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO). Lecture Notes in Computer Science, vol. 2053. Springer-Verlag, 103--116."},{"key":"e_1_2_1_36_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 2nd Symposium on Programs as Data Objects (PADO)","author":"Min\u00e9 A.","unstructured":"Min\u00e9 , A. 2001. A new numerical abstract domain based on difference-bound matrices . In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO) . Lecture Notes in Computer Science , vol. 2053 . Springer-Verlag , 155--172. Min\u00e9, A. 2001. A new numerical abstract domain based on difference-bound matrices. In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO). Lecture Notes in Computer Science, vol. 2053. Springer-Verlag, 155--172."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_39_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"1419","author":"Necula G. C.","unstructured":"Necula , G. C. and Lee , P . 1997. Safe, untrusted agents using proof-carrying code. In Special Issue on Mobile Agent Security, G. Vigna , Ed. Lecture Notes in Computer Science , vol. 1419 . Springer-Verlag, 61--91. Necula, G. C. and Lee, P. 1997. Safe, untrusted agents using proof-carrying code. In Special Issue on Mobile Agent Security, G. Vigna, Ed. Lecture Notes in Computer Science, vol. 1419. Springer-Verlag, 61--91."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360216"},{"key":"e_1_2_1_41_1","volume-title":"Software Security---Theories and Systems. Lecture Notes in Computer Science","volume":"2609","author":"Necula G. C.","unstructured":"Necula , G. C. and Schneck , R . 2002. Proof-carrying code with untrusted proof rules . In Software Security---Theories and Systems. Lecture Notes in Computer Science , vol. 2609 . Springer-Verlag, 283--298. Necula, G. C. and Schneck, R. 2002. Proof-carrying code with untrusted proof rules. In Software Security---Theories and Systems. Lecture Notes in Computer Science, vol. 2609. Springer-Verlag, 283--298."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_23"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_21"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science","volume":"2895","author":"Seo S.","unstructured":"Seo , S. , Yang , H. , and Yi , K . 2003. Automatic construction of Hoare proofs from abstract interpretation results . In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science , vol. 2895 . Springer-Verlag, 230--245. Seo, S., Yang, H., and Yi, K. 2003. Automatic construction of Hoare proofs from abstract interpretation results. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science, vol. 2895. Springer-Verlag, 230--245."},{"key":"e_1_2_1_45_1","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","unstructured":"Tip , F. 1995 . A survey of program slicing techniques . J. Program. Lang. 3 , 3, 121 -- 189 . Tip, F. 1995. A survey of program slicing techniques. J. Program. Lang. 3, 3, 121--189.","journal-title":"J. Program. Lang."},{"key":"e_1_2_1_46_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"274","author":"Wadler P.","unstructured":"Wadler , P. and Hughes , R. J. M. 1987. Projections for Strictness Analysis. In Functional Programming Languages and Computer Architecture, G. Kahn , Ed. Lecture Notes in Computer Science , vol. 274 . Springer, Berlin, 385--407. Wadler, P. and Hughes, R. J. M. 1987. Projections for Strictness Analysis. In Functional Programming Languages and Computer Architecture, G. Kahn, Ed. Lecture Notes in Computer Science, vol. 274. Springer, Berlin, 385--407."},{"key":"e_1_2_1_47_1","unstructured":"Yang H. Seo S. Yi K. and Han T. 2006. Off-line semantic slicing from abstract interpretation results. Tech. mem. ROPAS-2006-34 Programming Research Laboratory School of Computer Science & Engineering Seoul National University. Available at http:\/\/ropas.snu.ac.kr\/lib\/dock\/YaSeYiHa2006.pdf.  Yang H. Seo S. Yi K. and Han T. 2006. Off-line semantic slicing from abstract interpretation results. Tech. mem. ROPAS-2006-34 Programming Research Laboratory School of Computer Science & Engineering Seoul National University. Available at http:\/\/ropas.snu.ac.kr\/lib\/dock\/YaSeYiHa2006.pdf."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1286821.1286830","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1286821.1286830","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:57:49Z","timestamp":1750258669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1286821.1286830"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":47,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2007,10]]}},"alternative-id":["10.1145\/1286821.1286830"],"URL":"https:\/\/doi.org\/10.1145\/1286821.1286830","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2007,10]]},"assertion":[{"value":"2007-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}