{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,29]],"date-time":"2026-10-29T09:25:01Z","timestamp":1793265901456,"version":"4.5.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,8,2]],"date-time":"2007-08-02T00:00:00Z","timestamp":1186012800000},"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,8,2]]},"abstract":"<jats:p>In order to achieve better precision of abstract interpretation-based static analysis, we introduce a new generic abstract domain, the trace partitioning abstract domain. We develop a theoretical framework allowing a wide range of instantiations of the domain, proving that all these instantiations give correct results. From this theoretical framework, we go into implementation details of a particular instance developed in the Astr\u00e9e static analyzer. We show how the domain is automatically configured in Astr\u00e9e and the gain and cost in terms of performance and precision.<\/jats:p>","DOI":"10.1145\/1275497.1275501","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":156,"title":["The trace partitioning abstract domain"],"prefix":"10.1145","volume":"29","author":[{"given":"Xavier","family":"Rival","sequence":"first","affiliation":[{"name":"\u00c9cole Normale Sup\u00e9rieure, Paris Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[{"name":"\u00c9cole Normale Sup\u00e9rieure, Paris Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2007,8,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277665"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 8th International SPIN Workshop","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S. K . 2001. Automatically validating temporal safety properties of interfaces . In Proceedings of the 8th International SPIN Workshop ( Toronto, Canada). Lecture Notes in Computer Science. Springer, 103--122. Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the 8th International SPIN Workshop (Toronto, Canada). Lecture Notes in Computer Science. Springer, 103--122."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Annual ACM IEEE International Symposium on Microarchitecture (MICRO). IEEE Computer Society, Washington DC, 46--57","author":"Ball T.","unstructured":"Ball , T. and Larus , J. R . 1996. Efficient path profiling . In Proceedings of the Annual ACM IEEE International Symposium on Microarchitecture (MICRO). IEEE Computer Society, Washington DC, 46--57 . Ball, T. and Larus, J. R. 1996. Efficient path profiling. In Proceedings of the Annual ACM IEEE International Symposium on Microarchitecture (MICRO). IEEE Computer Society, Washington DC, 46--57."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Blanchet B. Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. Monniaux D. and Rival X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity Analysis Transformation. Essays Dedicated to Neil D. Jones T. Mogensen et al. eds. Lecture Notes in Computer Science vol. 2566. Springer 85--108.   Blanchet B. Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. Monniaux D. and Rival X. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity Analysis Transformation. Essays Dedicated to Neil D. Jones T. Mogensen et al. eds. Lecture Notes in Computer Science vol. 2566. Springer 85--108.","DOI":"10.1007\/3-540-36377-7_5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/267895.267921"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Conference on Formal Methods in Programming and Their Applications","author":"Bourdoncle F.","unstructured":"Bourdoncle , F. 1993. Efficient chaotic iteration strategies with widenings . In Proceedings of the International Conference on Formal Methods in Programming and Their Applications . Lecture Notes in Computer Science , vol. 735 , Springer , 128--142. Bourdoncle, F. 1993. Efficient chaotic iteration strategies with widenings. In Proceedings of the International Conference on Formal Methods in Programming and Their Applications. Lecture Notes in Computer Science, vol. 735, Springer, 128--142."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_9_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, Englewood Cliffs","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, 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, Englewood Cliffs, NJ. Chapter 10, 303--342.","journal-title":"NJ. Chapter"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the European Symposium On Programming (ESOP)","volume":"3444","author":"Cousot P.","unstructured":"Cousot , P. , Cousot , R. , Feret , J. , Mauborgne , L. , Min\u00e9 , A. , Monniaux , D. , and Rival , X . 2005. The ASTR\u00c9E analyzer . In Proceedings of the European Symposium On Programming (ESOP) ( Edinburgh, UK). Lecture Notes in Computer Science , vol. 3444 . Springer. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., and Rival, X. 2005. The ASTR\u00c9E analyzer. In Proceedings of the European Symposium On Programming (ESOP) (Edinburgh, UK). Lecture Notes in Computer Science, vol. 3444. Springer."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST)","author":"Halbwachs N.","unstructured":"Halbwachs , N. , Lagnier , F. , and Raymond , P . 1993. Synchronous observers and the verification of reactive systems . In Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST) ( Twente, The Netherlands). Springer, 83--96. Halbwachs, N., Lagnier, F., and Raymond, P. 1993. Synchronous observers and the verification of reactive systems. In Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST) (Twente, The Netherlands). Springer, 83--96."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Handjieva M. and Tzolovski S. 1998. Refining static analyses by trace-based partitioning using control flow. In Proceedings of the 5th International Static Analysis Symposium (SAS). Lecture Notes in Computer Science Springer 200--214.  Handjieva M. and Tzolovski S. 1998. Refining static analyses by trace-based partitioning using control flow. In Proceedings of the 5th International Static Analysis Symposium (SAS). Lecture Notes in Computer Science Springer 200--214.","DOI":"10.1007\/3-540-49727-7_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567454"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.53994"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024480913162"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 6th Static Analysis Symposium (SAS)","volume":"1694","author":"Jeannet B.","unstructured":"Jeannet , B. , Halbwachs , N. , and Raymond , P . 1999. Dynamic partitioning in analyses of numerical properties . In Proceedings of the 6th Static Analysis Symposium (SAS) ( Venice, Italy). Lecture Notes in Computer Science , vol. 1694 . Springer, 39--50. Jeannet, B., Halbwachs, N., and Raymond, P. 1999. Dynamic partitioning in analyses of numerical properties. In Proceedings of the 6th Static Analysis Symposium (SAS) (Venice, Italy). Lecture Notes in Computer Science, vol. 1694. Springer, 39--50."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567776"},{"key":"e_1_2_1_28_1","first-page":"384","article-title":"ASTR\u00c9E: Verification of absence of run-time error. In Building the Information Society. Kluwer Academic, Toulouse, France","volume":"4","author":"Mauborgne L.","year":"2004","unstructured":"Mauborgne , L. 2004 . ASTR\u00c9E: Verification of absence of run-time error. In Building the Information Society. Kluwer Academic, Toulouse, France . Chapter 4 , 384 -- 392 . Mauborgne, L. 2004. ASTR\u00c9E: Verification of absence of run-time error. In Building the Information Society. Kluwer Academic, Toulouse, France. Chapter 4, 384--392.","journal-title":"Chapter"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 12th International Conference on Compiler Construction (CC)","author":"Melski D.","unstructured":"Melski , D. and Reps , T. W . 2003. The interprocedural express-lane transformation . In Proceedings of the 12th International Conference on Compiler Construction (CC) ( Warsaw, Poland). Lecture Notes in Computer Science. Springer, 200--216. Melski, D. and Reps, T. W. 2003. The interprocedural express-lane transformation. In Proceedings of the 12th International Conference on Compiler Construction (CC) (Warsaw, Poland). Lecture Notes in Computer Science. Springer, 200--216."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_21"},{"key":"e_1_2_1_35_1","first-page":"189","article-title":"Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, eds. Prentice-Hall, Englewood Cliffs","volume":"7","author":"Sharir M.","year":"1981","unstructured":"Sharir , M. and Pnueli , A. 1981 . Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, eds. Prentice-Hall, Englewood Cliffs , NJ. Chapter 7 , 189 -- 233 . Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, eds. Prentice-Hall, Englewood Cliffs, NJ. Chapter 7, 189--233.","journal-title":"NJ. Chapter"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/647165.717832"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275501","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1275497.1275501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:30Z","timestamp":1750276830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,2]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,8,2]]}},"alternative-id":["10.1145\/1275497.1275501"],"URL":"https:\/\/doi.org\/10.1145\/1275497.1275501","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8,2]]},"assertion":[{"value":"2007-08-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}