{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:42Z","timestamp":1751660502758,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T00:00:00Z","timestamp":1295827200000},"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":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2011,1,24]]},"abstract":"<jats:p>Formal methods are increasingly used to help ensuring the correctness of complex, critical embedded software systems. We show how sound semantic static analyses based on Abstract Interpretation may be used to check properties at various levels of a software design: from high level models to low level binary code. After a short introduction to the Abstract Interpretation theory, we present a few current applications: checking for run-time errors at the C level, translation validation from C to assembly, and analyzing SAO models of communicating synchronous systems with imperfect clocks. We conclude by briey proposing some requirements to apply Abstract Interpretation to modeling languages such as UML.<\/jats:p>","DOI":"10.1145\/1921532.1921553","type":"journal-article","created":{"date-parts":[[2011,2,8]],"date-time":"2011-02-08T13:21:01Z","timestamp":1297171261000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Static analysis by abstract interpretation of embedded critical software"],"prefix":"10.1145","volume":"36","author":[{"given":"Julien","family":"Julien Bertrane","sequence":"first","affiliation":[{"name":"ENS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Cousot","sequence":"additional","affiliation":[{"name":"ENS &amp; CIMS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[{"name":"CNRS &amp; ENS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00f4me","family":"Feret","sequence":"additional","affiliation":[{"name":"INRIA &amp; ENS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[{"name":"IMDEA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[{"name":"CNRS &amp; ENS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[{"name":"INRIA &amp; ENS"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,1,24]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"AbsInt Angewandte Informatik. Astr\u00e9e run-time error analyzer. http:\/\/www.absint.com\/astree\/.  AbsInt Angewandte Informatik. Astr\u00e9e run-time error analyzer. http:\/\/www.absint.com\/astree\/."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_24"},{"key":"e_1_2_1_3_1","unstructured":"Bertrane J. Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. and Rival X. Static analysis  Bertrane J. Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. and Rival X. Static analysis"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D","author":"Blanchet B.","year":"2002","unstructured":"Blanchet , B. , Cousot , P. , Cousot , R. , Feret , J. , Mauborgne , L. , Min\u00e9 , A. , Monniaux , D. , and Rival , X . Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter . In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D . Jones, T. Mogensen, D. Schmidt, and I. Sudborough, Eds., LNCS 2566. Springer , 2002 , pp. 85 -- 108 . Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., and Rival, X. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen, D. Schmidt, and I. Sudborough, Eds., LNCS 2566. Springer, 2002, pp. 85--108."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_6_1","first-page":"1","volume-title":"Proc. of the Int. Space System Engineering Conference, Data Systems In Aerospace (DASIA'09)","author":"Bouissou O.","year":"2009","unstructured":"Bouissou , O. , Conquet , E. , Cousot , P. , Cousot , R. , Feret , J. , Goubault , E. , Ghorbal , K. , Lesens , D. , Mauborgne , L. , Min\u00e9 , A. , Putot , S. , Rival , X. , and Turin , M . Space software validation using abstract interpretation . In Proc. of the Int. Space System Engineering Conference, Data Systems In Aerospace (DASIA'09) (Istanbul, Turkey, 26- -29 May 2009 ), ESA publications, pp. 1 -- 7 . Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Feret, J., Goubault, E., Ghorbal, K., Lesens, D., Mauborgne, L., Min\u00e9, A., Putot, S., Rival, X., and Turin, M. Space software validation using abstract interpretation. In Proc. of the Int. Space System Engineering Conference, Data Systems In Aerospace (DASIA'09) (Istanbul, Turkey, 26--29 May 2009), ESA publications, pp. 1--7."},{"key":"e_1_2_1_7_1","volume-title":"Series","author":"Cousot P.","year":"1999","unstructured":"Cousot , P. The calculational design of a generic abstract interpreter . In Calculational System Design, M. Broy and R. Steinbr\u00fcggen, Eds. NATO ASI Series F. IOS Press , Amsterdam , 1999 . Cousot, P. The calculational design of a generic abstract interpreter. In Calculational System Design, M. Broy and R. Steinbr\u00fcggen, Eds. NATO ASI Series F. IOS Press, Amsterdam, 1999."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_10_1","volume-title":"Proc. of the 11th Annual Asian Computing Science Conference (ASIAN'06)","author":"Cousot P.","year":"2006","unstructured":"Cousot , P. , Cousot , R. , Feret , J. , Mauborgne , L. , Min\u00e9 , A. , Monniaux , D. , and Rival , X . Combination of abstractions in the Astr\u00e9e static analyzer . In Proc. of the 11th Annual Asian Computing Science Conference (ASIAN'06) (Tokyo, Japan, 6- -8 Dec. 2006 ), M. Okada and I. Satoh, Eds., vol. 4435 of LNCS, Springer, pp. 272--300. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., and Rival, X. Combination of abstractions in the Astr\u00e9e static analyzer. In Proc. of the 11th Annual Asian Computing Science Conference (ASIAN'06) (Tokyo, Japan, 6--8 Dec. 2006), M. Okada and I. Satoh, Eds., vol. 4435 of LNCS, Springer, pp. 272--300."},{"key":"e_1_2_1_11_1","unstructured":"Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. and Rival X. The Astr\u00e9e static analyzer. http:\/\/www.astree.ens.fr.  Cousot P. Cousot R. Feret J. Mauborgne L. Min\u00e9 A. and Rival X. The Astr\u00e9e static analyzer. http:\/\/www.astree.ens.fr."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_13_1","volume-title":"Proc. of the 14th Int. Static Analysis Symposium (SAS'07)","volume":"4634","author":"Delmas D.","unstructured":"Delmas , D. , and Souyris , J . Astr\u00e9e: from research to industry . In Proc. of the 14th Int. Static Analysis Symposium (SAS'07) , G. Fil\u00e9 and H. Riis-Nielson, Eds. , vol. 4634 of LNCS. Springer, Kongens Lyngby, Denmark, 22--24 Aug. 2007, pp. 437--451. Delmas, D., and Souyris, J. Astr\u00e9e: from research to industry. In Proc. of the 14th Int. Static Analysis Symposium (SAS'07), G. Fil\u00e9 and H. Riis-Nielson, Eds., vol. 4634 of LNCS. Springer, Kongens Lyngby, Denmark, 22--24 Aug. 2007, pp. 437--451."},{"key":"e_1_2_1_14_1","unstructured":"Esterel Technologies. Scade suite\u2122 the standard for the development of safety-critical embedded software in the avionics industry. http:\/\/www.esterel-technologies.com\/.  Esterel Technologies. Scade suite\u2122 the standard for the development of safety-critical embedded software in the avionics industry. http:\/\/www.esterel-technologies.com\/."},{"key":"e_1_2_1_15_1","series-title":"LNCS","first-page":"33","volume-title":"Proc. of the 13th European Symp. on Programming Languages and Systems (ESOP'04) (27 Mar.--4","author":"Feret J.","year":"2004","unstructured":"Feret , J. Static analysis of digital filters . In Proc. of the 13th European Symp. on Programming Languages and Systems (ESOP'04) (27 Mar.--4 Apr. 2004 ), D. Schmidt, Ed ., vol. 2986 of LNCS , Springer , pp. 33 -- 48 . Feret, J. Static analysis of digital filters. In Proc. of the 13th European Symp. on Programming Languages and Systems (ESOP'04) (27 Mar.--4 Apr. 2004), D. Schmidt, Ed., vol. 2986 of LNCS, Springer, pp. 33--48."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_3"},{"key":"e_1_2_1_17_1","first-page":"234","volume-title":"Proc. of the 8th Int. Static Analysis Symposium (SAS'01)","volume":"2126","author":"Goubault E.","year":"2001","unstructured":"Goubault , E. Static analyses of oating-point operations . In Proc. of the 8th Int. Static Analysis Symposium (SAS'01) ( 2001 ), vol. 2126 of LNCS, Springer , pp. 234 -- 259 . Goubault, E. Static analyses of oating-point operations. In Proc. of the 8th Int. Static Analysis Symposium (SAS'01) (2001), vol. 2126 of LNCS, Springer, pp. 234--259."},{"key":"e_1_2_1_18_1","first-page":"26","volume-title":"Proc. of the 18th Int. Parallel and Distributed Processing Symposium (IPDPS'04)","author":"Heckmann R.","year":"2004","unstructured":"Heckmann , R. , and Ferdinand , C . Worst-case execution time prediction by static program analysis . In Proc. of the 18th Int. Parallel and Distributed Processing Symposium (IPDPS'04) ( 2004 ), IEEE Computer Society , pp. 26 -- 30 . Heckmann, R., and Ferdinand, C. Worst-case execution time prediction by static program analysis. In Proc. of the 18th Int. Parallel and Distributed Processing Symposium (IPDPS'04) (2004), IEEE Computer Society, pp. 26--30."},{"key":"e_1_2_1_19_1","first-page":"1985","author":"IEEE Computer Society","year":"1985","unstructured":"IEEE Computer Society . IEEE standard for binary floating-point arithmetic. Tech. rep., ANSI\/IEEE Std. 745-- 1985 , 1985 . IEEE Computer Society. IEEE standard for binary floating-point arithmetic. Tech. rep., ANSI\/IEEE Std. 745--1985, 1985.","journal-title":"Tech. rep., ANSI\/IEEE Std. 745--"},{"key":"e_1_2_1_20_1","volume-title":"Tools for Automatic Program AnalysiS (TAPAS","author":"Ioualalen A.","year":"2010","unstructured":"Ioualalen , A. SARDANA: an abstract interpretation based tool for Optimization of numerical expressions in LUSTRE programs . In Tools for Automatic Program AnalysiS (TAPAS 2010 ), Perpignan , France (17 Sep. 2010). Ioualalen, A. SARDANA: an abstract interpretation based tool for Optimization of numerical expressions in LUSTRE programs. In Tools for Automatic Program AnalysiS (TAPAS 2010), Perpignan, France (17 Sep. 2010)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_1_23_1","first-page":"1","volume-title":"Proc. of Embedded Real-Time Software and Systems (ERTS'10)","author":"K\u00e4stner D.","year":"2010","unstructured":"K\u00e4stner , D. , Wilhelm , S. , Nenova , S. , Cousot , P. , Cousot , R. , Feret , J. , Mauborgne , L. , Min\u00e9 , A. , and Rival , X . Astr\u00e9e: Proving the absence of rutime errors . In Proc. of Embedded Real-Time Software and Systems (ERTS'10) (Toulouse, France , May 2010 ), pp. 1 -- 5 . (to appear). K\u00e4stner, D., Wilhelm, S., Nenova, S., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., and Rival, X. Astr\u00e9e: Proving the absence of rutime errors. In Proc. of Embedded Real-Time Software and Systems (ERTS'10) (Toulouse, France, May 2010), pp. 1--5. (to appear)."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134659"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_26_1","volume-title":"Interval Analysis","author":"Moore R. E.","year":"1966","unstructured":"Moore , R. E. Interval Analysis . Prentice Hall , Englewood Cliffs N. J. , USA, 1966 . Moore, R. E. Interval Analysis. Prentice Hall, Englewood Cliffs N. J., USA, 1966."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647545.730777"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964002"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_2_1_30_1","volume-title":"Software Considerations in Airborne Systems and Equipment Certification","author":"Technical Commission on Aviation, R. DO-178B. Tech.","year":"1999","unstructured":"Technical Commission on Aviation, R. DO-178B. Tech. rep ., Software Considerations in Airborne Systems and Equipment Certification , 1999 . Technical Commission on Aviation, R. DO-178B. Tech. rep., Software Considerations in Airborne Systems and Equipment Certification, 1999."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11880240_53"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921553","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1921532.1921553","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:41Z","timestamp":1750248521000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921553"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,24]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1,24]]}},"alternative-id":["10.1145\/1921532.1921553"],"URL":"https:\/\/doi.org\/10.1145\/1921532.1921553","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2011,1,24]]},"assertion":[{"value":"2011-01-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}