{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:23:32Z","timestamp":1750307012551,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,6,15]],"date-time":"2012-06-15T00:00:00Z","timestamp":1339718400000},"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":[],"published-print":{"date-parts":[[2012,6,15]]},"DOI":"10.1145\/2336717.2336726","type":"proceedings-article","created":{"date-parts":[[2012,7,26]],"date-time":"2012-07-26T14:41:14Z","timestamp":1343313674000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment"],"prefix":"10.1145","author":[{"given":"Damien","family":"Doligez","sequence":"first","affiliation":[{"name":"Gallium, Inria, Rocquencourt, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathieu","family":"Jaume","sequence":"additional","affiliation":[{"name":"Univ. P. & M. Curie, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renaud","family":"Rioboo","sequence":"additional","affiliation":[{"name":"CPR CEDRIC, ENSIIE, Evry, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02949-3_3"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.003"},{"key":"e_1_3_2_1_5_1","first-page":"151","volume-title":"14th Int. Conf., LPAR","volume":"4790","author":"Bonichon R.","year":"2007","unstructured":"R. Bonichon , D. Delahaye , and D. Doligez . Zenon: An extensible automated theorem prover producing checkable proofs. In Logic for Programming, Artificial Intelligence, and Reasoning , 14th Int. Conf., LPAR , volume 4790 of LNCS, pages 151 -- 165 . Springer , 2007 . R. Bonichon, D. Delahaye, and D. Doligez. Zenon: An extensible automated theorem prover producing checkable proofs. In Logic for Programming, Artificial Intelligence, and Reasoning, 14th Int. Conf., LPAR, volume 4790 of LNCS, pages 151--165. Springer, 2007."},{"key":"e_1_3_2_1_6_1","volume-title":"9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2001","author":"Boulm\u00e9 S.","year":"2001","unstructured":"S. Boulm\u00e9 , T. Hardin , and R. Rioboo . Some hints for polynomials in the Foc project . In 9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2001 , 2001 . S. Boulm\u00e9, T. Hardin, and R. Rioboo. Some hints for polynomials in the Foc project. In 9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2001, 2001."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27901-0_12"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_9_1","first-page":"84","volume-title":"Second Int. Conf., TAP 2008, Proceedings","volume":"4966","author":"Carlier M.","year":"2008","unstructured":"M. Carlier and C. Dubois . Functional testing in the Focal environment. In Tests and Proofs , Second Int. Conf., TAP 2008, Proceedings , volume 4966 of LNCS, pages 84 -- 98 . Springer , 2008 . M. Carlier and C. Dubois. Functional testing in the Focal environment. In Tests and Proofs, Second Int. Conf., TAP 2008, Proceedings, volume 4966 of LNCS, pages 84--98. Springer, 2008."},{"key":"e_1_3_2_1_10_1","first-page":"82","volume-title":"ICSOFT 2010 - Proceedings of the Fifth Int. Conf. on Software and Data Technologies","volume":"2","author":"Carlier M.","year":"2010","unstructured":"M. Carlier , C. Dubois , and A. Gotlieb . Constraint reasoning in FocalTest . In ICSOFT 2010 - Proceedings of the Fifth Int. Conf. on Software and Data Technologies , Volume 2 , pages 82 -- 91 . SciTePress , 2010 . M. Carlier, C. Dubois, and A. Gotlieb. Constraint reasoning in FocalTest. In ICSOFT 2010 - Proceedings of the Fifth Int. Conf. on Software and Data Technologies, Volume 2, pages 82--91. SciTePress, 2010."},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. of the LPAR Workshop Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA'08)","author":"Chaudhuri K.","year":"2008","unstructured":"K. Chaudhuri , D. Doligez , L. Lamport , and S. Merz . A TLA+ proof system. In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz, editors , Proc. of the LPAR Workshop Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA'08) , number 418 in CEUR Workshop Proceedings, pages 17--37 , 2008 . K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz. A TLA+ proof system. In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz, editors, Proc. of the LPAR Workshop Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA'08), number 418 in CEUR Workshop Proceedings, pages 17--37, 2008."},{"key":"e_1_3_2_1_12_1","volume-title":"Norme ISO 15408 -- Version 3.0 Rev 2","author":"Criteria Common","year":"2005","unstructured":"Common Criteria . Common Criteria for Information Technology Security Evaluation , Norme ISO 15408 -- Version 3.0 Rev 2 , 2005 . Common Criteria. Common Criteria for Information Technology Security Evaluation, Norme ISO 15408 -- Version 3.0 Rev 2, 2005."},{"volume-title":"The Coq Proof Assistant, Tutorial and reference manual. INRIA -- LIP -- LRI -- LIX -- PPS","year":"2010","key":"e_1_3_2_1_13_1","unstructured":"Coq. The Coq Proof Assistant, Tutorial and reference manual. INRIA -- LIP -- LRI -- LIX -- PPS , 2010 . Distribution available at: http:\/\/coq.inria.fr\/. Coq. The Coq Proof Assistant, Tutorial and reference manual. INRIA -- LIP -- LRI -- LIX -- PPS, 2010. Distribution available at: http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_4"},{"key":"e_1_3_2_1_15_1","volume-title":"21th Journ\u00e9es Francophones des Langages Applicatifs","author":"Delahaye D.","year":"2010","unstructured":"D. Delahaye , C. Dubois , and P. Tollite . G\u00e9n\u00e9ration de code fonctionnel certifi\u00e9 \u00e0 partir de sp\u00e9cifications inductives dans l'environnement Focalize . In 21th Journ\u00e9es Francophones des Langages Applicatifs , 2010 . D. Delahaye, C. Dubois, and P. Tollite. G\u00e9n\u00e9ration de code fonctionnel certifi\u00e9 \u00e0 partir de sp\u00e9cifications inductives dans l'environnement Focalize. In 21th Journ\u00e9es Francophones des Langages Applicatifs, 2010."},{"key":"e_1_3_2_1_16_1","volume-title":"National Institute for Standards and Technology","author":"Security FIPS.","year":"2009","unstructured":"FIPS. Security Requirements for Cryptographic Modules , FIPS 140--3. National Institute for Standards and Technology , 2009 . FIPS. Security Requirements for Cryptographic Modules, FIPS 140--3. National Institute for Standards and Technology, 2009."},{"volume-title":"Tutorial and reference manual. LIP6 -- INRIA -- CEDRIC","year":"2010","key":"e_1_3_2_1_17_1","unstructured":"Focalize. Focalize , Tutorial and reference manual. LIP6 -- INRIA -- CEDRIC , 2010 . Distribution available at: http:\/\/focalize.inria.fr. Focalize. Focalize, Tutorial and reference manual. LIP6 -- INRIA -- CEDRIC, 2010. Distribution available at: http:\/\/focalize.inria.fr."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360303.360333"},{"key":"e_1_3_2_1_19_1","first-page":"231","volume-title":"Conf., ICISS","volume":"6503","author":"Jaume M.","year":"2010","unstructured":"M. Jaume . Security rules versus security properties. In Information Systems Security - 6th Int . Conf., ICISS , volume 6503 of LNCS, pages 231 -- 245 . Springer , 2010 . M. Jaume. Security rules versus security properties. In Information Systems Security - 6th Int. Conf., ICISS, volume 6503 of LNCS, pages 231--245. Springer, 2010."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25560-1_5"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1995.12004627"},{"key":"e_1_3_2_1_22_1","volume-title":"The Objective Caml system, Documentation and user's manual, release 3.07 edition","author":"Leroy X.","year":"2003","unstructured":"X. Leroy , D. Doligez , J. Garrigue , D. R\u00e9my , and J. Vouillon . The Objective Caml system, Documentation and user's manual, release 3.07 edition , 2003 . X. Leroy, D. Doligez, J. Garrigue, D. R\u00e9my, and J. Vouillon. The Objective Caml system, Documentation and user's manual, release 3.07 edition, 2003."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021979218446"},{"key":"e_1_3_2_1_24_1","first-page":"89","volume-title":"11th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2003","author":"Prevosto V.","year":"2003","unstructured":"V. Prevosto and M. Jaume . Making proofs in a hierarchy of mathematical structures . In 11th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2003 , pages 89 -- 100 . Aracne , 2003 . V. Prevosto and M. Jaume. Making proofs in a hierarchy of mathematical structures. In 11th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2003, pages 89--100. Aracne, 2003."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9156-3"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11955757_18"}],"event":{"name":"PLDI '12: ACM SIGPLAN Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Beijing China","acronym":"PLDI '12"},"container-title":["Proceedings of the 7th Workshop on Programming Languages and Analysis for Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2336717.2336726","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2336717.2336726","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:49:03Z","timestamp":1750236543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2336717.2336726"}},"subtitle":["a case study within the FoCaLiZe environment"],"short-title":[],"issued":{"date-parts":[[2012,6,15]]},"references-count":25,"alternative-id":["10.1145\/2336717.2336726","10.1145\/2336717"],"URL":"https:\/\/doi.org\/10.1145\/2336717.2336726","relation":{},"subject":[],"published":{"date-parts":[[2012,6,15]]},"assertion":[{"value":"2012-06-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}