{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:04Z","timestamp":1776305284580,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"8","license":[{"start":{"date-parts":[[2021,7,26]],"date-time":"2021-07-26T00:00:00Z","timestamp":1627257600000},"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":["Commun. ACM"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:p>A panoramic view of a popular platform for C program analysis and verification.<\/jats:p>","DOI":"10.1145\/3470569","type":"journal-article","created":{"date-parts":[[2021,7,26]],"date-time":"2021-07-26T16:09:42Z","timestamp":1627315782000},"page":"56-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":56,"title":["The dogged pursuit of bug-free C programs"],"prefix":"10.1145","volume":"64","author":[{"given":"Patrick","family":"Baudin","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Fran\u00e7ois","family":"Bobot","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"David","family":"B\u00fchler","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Lo\u00efc","family":"Correnson","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Florent","family":"Kirchner","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[{"name":"Thales Research and Technology, Palaiseau, France"}]},{"given":"Andr\u00e9","family":"Maroneze","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Valentin","family":"Perrelle","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Julien","family":"Signoles","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]},{"given":"Nicky","family":"Williams","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CEA, List, Palaiseau, France"}]}],"member":"320","published-online":{"date-parts":[[2021,7,26]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proc. of the 2017 Conf. on Logic-based Program Synthesis and Transformation.","author":"Alberti M.","unstructured":"Alberti , M. and Signoles , J . Context generation from formal specifications for C analysis tools . In Proc. of the 2017 Conf. on Logic-based Program Synthesis and Transformation. Alberti, M. and Signoles, J. Context generation from formal specifications for C analysis tools. In Proc. of the 2017 Conf. on Logic-based Program Synthesis and Transformation."},{"key":"e_1_2_1_2_1","volume-title":"Proc. of the 2004 Conf. on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Alur R.","unstructured":"Alur , R. , Etessami , K. , and Madhusudan , P . A temporal logic of nested calls and returns . In Proc. of the 2004 Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Alur, R., Etessami, K., and Madhusudan, P. A temporal logic of nested calls and returns. In Proc. of the 2004 Conf. on Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_3_1","volume-title":"Proc. of the 2017 Conf. on Tests and Proofs.","author":"Barany G.","unstructured":"Barany , G. and Signoles , J . Hybrid information flow analysis for real-world C code . In Proc. of the 2017 Conf. on Tests and Proofs. Barany, G. and Signoles, J. Hybrid information flow analysis for real-world C code. In Proc. of the 2017 Conf. on Tests and Proofs."},{"key":"e_1_2_1_4_1","volume-title":"Proc. of the 2014 Conf. on Tests and Proofs.","author":"Bardin S.","unstructured":"Bardin , S. , Chebaro , O. , Delahaye , M. , and Kosmatov , N . An All-in-One Toolkit for Automated White-Box Testing . In Proc. of the 2014 Conf. on Tests and Proofs. Bardin, S., Chebaro, O., Delahaye, M., and Kosmatov, N. An All-in-One Toolkit for Automated White-Box Testing. In Proc. of the 2014 Conf. on Tests and Proofs."},{"key":"e_1_2_1_5_1","volume-title":"Proc. of the 2018 Conf. on Leveraging Applications of Formal Methods, Verification and Validation.","author":"Bardin S.","unstructured":"Bardin , S. , Kosmatov , N. , Marre , B. , Mentr\u00e9 , D. , and Williams , N . Test case generation with PathCrawler\/LTest: How to automate an industrial testing process . In Proc. of the 2018 Conf. on Leveraging Applications of Formal Methods, Verification and Validation. Bardin, S., Kosmatov, N., Marre, B., Mentr\u00e9, D., and Williams, N. Test case generation with PathCrawler\/LTest: How to automate an industrial testing process. In Proc. of the 2018 Conf. on Leveraging Applications of Formal Methods, Verification and Validation."},{"key":"e_1_2_1_6_1","first-page":"6","author":"Barthe G.","year":"2011","unstructured":"Barthe , G. , D'Argenio , P. , and Rezk , T. Secure information flow by self-composition. Mathematical Structures in Computer Science 6 ( 2011 ). Barthe, G., D'Argenio, P., and Rezk, T. Secure information flow by self-composition. Mathematical Structures in Computer Science 6 (2011).","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_2_1_7_1","volume-title":"Proc. of the 2016 Conf. on Source Code Analysis and Manipulation.","author":"Blanchard A.","unstructured":"Blanchard , A. , Kosmatov , N. , Lemerre , M. , and Loulergue , F . Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs . In Proc. of the 2016 Conf. on Source Code Analysis and Manipulation. Blanchard, A., Kosmatov, N., Lemerre, M., and Loulergue, F. Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. In Proc. of the 2016 Conf. on Source Code Analysis and Manipulation."},{"key":"e_1_2_1_8_1","volume-title":"Proc. of the 2017 Conf. on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Blatter L.","unstructured":"Blatter , L. , Kosmatov , N. , Gall , P. , and Prevosto , V . RPP: Automatic proof of relational properties by self-composition . In Proc. of the 2017 Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Blatter, L., Kosmatov, N., Gall, P., and Prevosto, V. RPP: Automatic proof of relational properties by self-composition. In Proc. of the 2017 Conf. on Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_9_1","volume-title":"Proc. of the 2020 Conf. on Embedded Real Time Softw. and Systems.","author":"Brahmi A.","unstructured":"Brahmi , A. , Carolus , M. , Delmas , D. , Essoussi , M. , Lacabanne , P. , Lamiel , V. , Randimbivololona , F. , and Souyris , J . Industrial use of a safe and efficient formal method based software engineering process in avionics . In Proc. of the 2020 Conf. on Embedded Real Time Softw. and Systems. Brahmi, A., Carolus, M., Delmas, D., Essoussi, M., Lacabanne, P., Lamiel, V., Randimbivololona, F., and Souyris, J. Industrial use of a safe and efficient formal method based software engineering process in avionics. In Proc. of the 2020 Conf. on Embedded Real Time Softw. and Systems."},{"key":"e_1_2_1_10_1","volume-title":"Proc. of the 2010 Int. Conf. on Softw. Testing, Verification and Validation.","author":"Ceara D.","unstructured":"Ceara , D. , Mounier , L. , and Potet , M . Taint dependency Ssquences: A characterization of insecure execution paths based on input-sensitive cause sequences . In Proc. of the 2010 Int. Conf. on Softw. Testing, Verification and Validation. Ceara, D., Mounier, L., and Potet, M. Taint dependency Ssquences: A characterization of insecure execution paths based on input-sensitive cause sequences. In Proc. of the 2010 Int. Conf. on Softw. Testing, Verification and Validation."},{"key":"e_1_2_1_11_1","volume-title":"Proc. of the 2007 Int. Conf. on Softw. Engineering.","author":"Chalin P.","unstructured":"Chalin , P. A sound assertion semantics for the dependable systems evolution verifying compiler . In Proc. of the 2007 Int. Conf. on Softw. Engineering. Chalin, P. A sound assertion semantics for the dependable systems evolution verifying compiler. In Proc. of the 2007 Int. Conf. on Softw. Engineering."},{"key":"e_1_2_1_12_1","volume-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications. Trans. Programming Languages and Systems","author":"Clarke E.","year":"1986","unstructured":"Clarke , E. , Emerson , E. , and Sistla , A . Automatic verification of finite-state concurrent systems using temporal logic specifications. Trans. Programming Languages and Systems ( 1986 ). Clarke, E., Emerson, E., and Sistla, A. Automatic verification of finite-state concurrent systems using temporal logic specifications. Trans. Programming Languages and Systems (1986)."},{"key":"e_1_2_1_13_1","volume-title":"Proc. of the 2014 Conf. on NASA Formal Methods.","author":"Correnson L.","unstructured":"Correnson , L. Computing what remains to be proved . In Proc. of the 2014 Conf. on NASA Formal Methods. Correnson, L. Computing what remains to be proved. In Proc. of the 2014 Conf. on NASA Formal Methods."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_8"},{"key":"e_1_2_1_15_1","volume-title":"Proc. of the 2012 Conf. on Embedded Real Time Softw. and Systems.","author":"Cuoq P.","unstructured":"Cuoq , P. , Delmas , D. , Duprat , S. , and Lamiel , V . Fan-C, a Frama-C plug-in for data flow verification . In Proc. of the 2012 Conf. on Embedded Real Time Softw. and Systems. Cuoq, P., Delmas, D., Duprat, S., and Lamiel, V. Fan-C, a Frama-C plug-in for data flow verification. In Proc. of the 2012 Conf. on Embedded Real Time Softw. and Systems."},{"key":"e_1_2_1_16_1","volume-title":"Proc. of the 2016 Conf. on Automated Technology for Verification and Analysis.","author":"de Oliveira S.","unstructured":"de Oliveira , S. , Bensalem , S. , and Prevosto , V . Polynomial invariants by linear algebra . In Proc. of the 2016 Conf. on Automated Technology for Verification and Analysis. de Oliveira, S., Bensalem, S., and Prevosto, V. Polynomial invariants by linear algebra. In Proc. of the 2016 Conf. on Automated Technology for Verification and Analysis."},{"key":"e_1_2_1_17_1","volume-title":"Proc. of the 2013 Int. Symp. on Static Analysis.","author":"Dragoi C.","unstructured":"Dragoi , C. , Enea , C. , and Sighireanu , M . Local shape analysis for overlaid data structures . In Proc. of the 2013 Int. Symp. on Static Analysis. Dragoi, C., Enea, C., and Sighireanu, M. Local shape analysis for overlaid data structures. In Proc. of the 2013 Int. Symp. on Static Analysis."},{"key":"e_1_2_1_18_1","volume-title":"Formal verification with Frama-C: A case study in the space software domain. Trans. Reliability","author":"Silva R.","year":"2016","unstructured":"e Silva , R. , Arai , N. , Burgareli , L. , de Oliveira , J. , and Pinto , J . Formal verification with Frama-C: A case study in the space software domain. Trans. Reliability ( 2016 ). e Silva, R., Arai, N., Burgareli, L., de Oliveira, J., and Pinto, J. Formal verification with Frama-C: A case study in the space software domain. Trans. Reliability (2016)."},{"key":"e_1_2_1_19_1","volume-title":"Proc. of the 2019 Symp. sur la S\u00e9curit\u00e9 des Technologies de l'information et des Communications.","author":"Ebalard A.","unstructured":"Ebalard , A. , Mouy , P. , and Benadjila , R . Journey to a RTEfree X.509 parser . In Proc. of the 2019 Symp. sur la S\u00e9curit\u00e9 des Technologies de l'information et des Communications. Ebalard, A., Mouy, P., and Benadjila, R. Journey to a RTEfree X.509 parser. In Proc. of the 2019 Symp. sur la S\u00e9curit\u00e9 des Technologies de l'information et des Communications."},{"key":"e_1_2_1_20_1","volume-title":"Proc. of the 2015 Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning.","author":"Fava D.","unstructured":"Fava , D. , Signoles , J. , Lemerre , M. , Sch\u00e4f , M. , and Tiwari , A . Gamifying program analysis . In Proc. of the 2015 Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning. Fava, D., Signoles, J., Lemerre, M., Sch\u00e4f, M., and Tiwari, A. Gamifying program analysis. In Proc. of the 2015 Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning."},{"key":"e_1_2_1_21_1","volume-title":"Proc. of the 2004 Int. Conf. on Formal Methods and Softw. Engineering.","author":"Filli\u00e2tre J.","unstructured":"Filli\u00e2tre , J. and March\u00e9 , C . Multi-prover verification of C programs . In Proc. of the 2004 Int. Conf. on Formal Methods and Softw. Engineering. Filli\u00e2tre, J. and March\u00e9, C. Multi-prover verification of C programs. In Proc. of the 2004 Int. Conf. on Formal Methods and Softw. Engineering."},{"key":"e_1_2_1_22_1","volume-title":"Proc. of the 2013 European Symp. on Programming.","author":"Filli\u00e2tre J.","unstructured":"Filli\u00e2tre , J. and Paskevich , A . Why3---Where programs meet provers . In Proc. of the 2013 European Symp. on Programming. Filli\u00e2tre, J. and Paskevich, A. Why3---Where programs meet provers. In Proc. of the 2013 European Symp. on Programming."},{"key":"e_1_2_1_23_1","volume-title":"Proc. of the 2013 Int. Symp. on Static Analysis.","author":"Fouilh\u00e9 A.","unstructured":"Fouilh\u00e9 , A. , Monniaux , D. , and P\u00e9rin , M . Efficient generation of correctness certificates for the abstract domain of polyhedra . In Proc. of the 2013 Int. Symp. on Static Analysis. Fouilh\u00e9, A., Monniaux, D., and P\u00e9rin, M. Efficient generation of correctness certificates for the abstract domain of polyhedra. In Proc. of the 2013 Int. Symp. on Static Analysis."},{"key":"e_1_2_1_24_1","volume-title":"Proc. of the 2013 Conf. on NASA Formal Methods.","author":"Goodloe A.","unstructured":"Goodloe , A. , Mu\u00f1oz , C. , Kirchner , F. , and Correnson , L . Verification of numerical programs: From real numbers to floating point numbers . In Proc. of the 2013 Conf. on NASA Formal Methods. Goodloe, A., Mu\u00f1oz, C., Kirchner, F., and Correnson, L. Verification of numerical programs: From real numbers to floating point numbers. In Proc. of the 2013 Conf. on NASA Formal Methods."},{"key":"e_1_2_1_25_1","volume-title":"Proc. of 2018 Int. Symp. on Static Analysis.","author":"Jacquemin M.","unstructured":"Jacquemin , M. , Putot , S. , and V\u00e9drine , F . A reduced product of absolute and relative error bounds for floating-point analysis . In Proc. of 2018 Int. Symp. on Static Analysis. Jacquemin, M., Putot, S., and V\u00e9drine, F. A reduced product of absolute and relative error bounds for floating-point analysis. In Proc. of 2018 Int. Symp. on Static Analysis."},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Kirchner F. Kosmatov N. Prevosto V. Signoles J. and Yakobowski B. Frama-C: A software analysis perspective. Formal Asp. Comput. (2015).  Kirchner F. Kosmatov N. Prevosto V. Signoles J. and Yakobowski B. Frama-C: A software analysis perspective. Formal Asp. Comput. (2015).","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_1_27_1","volume-title":"Proc. of the 2016 Conf. on Embedded Real Time Softw. and Systems.","author":"Kirchner F.","unstructured":"Kirchner , F. , Sadmi , F. , Flanc , S. , Duboc , L. , Marteau , H. , Prevosto , V. , and Vedrine , F . Safer marine and offshore software with formal-verification-based guidelines . In Proc. of the 2016 Conf. on Embedded Real Time Softw. and Systems. Kirchner, F., Sadmi, F., Flanc, S., Duboc, L., Marteau, H., Prevosto, V., and Vedrine, F. Safer marine and offshore software with formal-verification-based guidelines. In Proc. of the 2016 Conf. on Embedded Real Time Softw. and Systems."},{"key":"e_1_2_1_28_1","volume-title":"Efficient weakest preconditions. Information Processing Letters","author":"Leino K.","year":"2005","unstructured":"Leino , K. Efficient weakest preconditions. Information Processing Letters ( 2005 ). Leino, K. Efficient weakest preconditions. Information Processing Letters (2005)."},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Mandrykin M. and Khoroshilov A. High-level memory model with low-level pointer cast support for Jessie intermediate language. Programming and Computer Softw. (2015).  Mandrykin M. and Khoroshilov A. High-level memory model with low-level pointer cast support for Jessie intermediate language. Programming and Computer Softw. (2015).","DOI":"10.1134\/S0361768815040040"},{"key":"e_1_2_1_30_1","volume-title":"Proc. of the 2005 European Symp. on Programming.","author":"Mauborgne L.","unstructured":"Mauborgne , L. and Rival , X . Trace partitioning in abstract interpretation based static analyzers . In Proc. of the 2005 European Symp. on Programming. Mauborgne, L. and Rival, X. Trace partitioning in abstract interpretation based static analyzers. In Proc. of the 2005 European Symp. on Programming."},{"key":"e_1_2_1_31_1","volume-title":"Design by Contract","author":"Meyer B.","year":"1991","unstructured":"Meyer , B. Design by Contract . Prentice Hall , 1991 . Meyer, B. Design by Contract. Prentice Hall, 1991."},{"key":"e_1_2_1_32_1","volume-title":"Proc. of the 2008 Conf. on Trusted Computing and Trust in Information Technologies.","author":"Monate B.","unstructured":"Monate , B. and Signoles , J . Slicing for security of code . In Proc. of the 2008 Conf. on Trusted Computing and Trust in Information Technologies. Monate, B. and Signoles, J. Slicing for security of code. In Proc. of the 2008 Conf. on Trusted Computing and Trust in Information Technologies."},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Ourghanlian A. Evaluation of static analysis tools used to assess software important to nuclear power plant safety. Nucl. Eng. Technol. (2015).  Ourghanlian A. Evaluation of static analysis tools used to assess software important to nuclear power plant safety. Nucl. Eng. Technol. (2015).","DOI":"10.1016\/j.net.2014.12.009"},{"key":"e_1_2_1_34_1","volume-title":"Proc. of the 2017 Symp. sur la S\u00e9curit\u00e9 des Technologies de l'Information et des Communications.","author":"Pariente D.","unstructured":"Pariente , D. and Signoles , J . Static analysis and runtime assertion checking: Contribution to security countermeasures . In Proc. of the 2017 Symp. sur la S\u00e9curit\u00e9 des Technologies de l'Information et des Communications. Pariente, D. and Signoles, J. Static analysis and runtime assertion checking: Contribution to security countermeasures. In Proc. of the 2017 Symp. sur la S\u00e9curit\u00e9 des Technologies de l'Information et des Communications."},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Petiot G. Kosmatov N. Botella B. Giorgetti A. and Julliand J. How testing helps to diagnose proof failures. Formal Asp. Comput. (2018).  Petiot G. Kosmatov N. Botella B. Giorgetti A. and Julliand J. How testing helps to diagnose proof failures. Formal Asp. Comput. (2018).","DOI":"10.1007\/s00165-018-0456-4"},{"key":"e_1_2_1_36_1","volume-title":"Proc. of the 2013 Int. Conf. on Industrial Informatics.","author":"Prevosto V.","unstructured":"Prevosto , V. , Burghardt , J. , Gerlach , J. , Hartig , K. , Pohl , H. , and V\u00f6llinger , K . Formal specification and automated verification of railway software with Frama-C . In Proc. of the 2013 Int. Conf. on Industrial Informatics. Prevosto, V., Burghardt, J., Gerlach, J., Hartig, K., Pohl, H., and V\u00f6llinger, K. Formal specification and automated verification of railway software with Frama-C. In Proc. of the 2013 Int. Conf. on Industrial Informatics."},{"key":"e_1_2_1_37_1","volume-title":"Proc. of the Conf. on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Robles V.","unstructured":"Robles , V. , Kosmatov , N. , Prevosto , V. , Rilling , L. , and Gall , P . MetAcsl: Specification and verification of high-level properties . In Proc. of the Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., and Gall, P. MetAcsl: Specification and verification of high-level properties. In Proc. of the Conf. on Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_38_1","volume-title":"Tool Paper. In Proc. of the 2017 Int. Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardization for Runtime Verification Tools.","author":"Signoles J.","unstructured":"Signoles , J. , Kosmatov , N. , and Vorobyov , K . E-ACSL, a runtime verification tool for safety and security of C programs . Tool Paper. In Proc. of the 2017 Int. Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardization for Runtime Verification Tools. Signoles, J., Kosmatov, N., and Vorobyov, K. E-ACSL, a runtime verification tool for safety and security of C programs. Tool Paper. In Proc. of the 2017 Int. Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardization for Runtime Verification Tools."},{"key":"e_1_2_1_39_1","volume-title":"Proc. of the 2012 Conf. on Computer Aided Verification.","author":"Venet A.","unstructured":"Venet , A. The Gauge domain: Scalable analysis of linear inequality invariants . In Proc. of the 2012 Conf. on Computer Aided Verification. Venet, A. The Gauge domain: Scalable analysis of linear inequality invariants. In Proc. of the 2012 Conf. on Computer Aided Verification."},{"key":"e_1_2_1_40_1","volume-title":"Proc. of the 2005 European Dependable Computing Conf.","author":"Williams N.","unstructured":"Williams , N. , Marre , B. , Mouy , P. , and Roger , M . PathCrawler: Automatic generation of path tests by combining static and dynamic analysis . In Proc. of the 2005 European Dependable Computing Conf. Williams, N., Marre, B., Mouy, P., and Roger, M. PathCrawler: Automatic generation of path tests by combining static and dynamic analysis. In Proc. of the 2005 European Dependable Computing Conf."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3470569","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3470569","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:54Z","timestamp":1750191534000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3470569"}},"subtitle":["the Frama-C software analysis platform"],"short-title":[],"issued":{"date-parts":[[2021,7,26]]},"references-count":40,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1145\/3470569"],"URL":"https:\/\/doi.org\/10.1145\/3470569","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,26]]},"assertion":[{"value":"2021-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}