{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:09:45Z","timestamp":1763968185591,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"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":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854082","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T13:18:57Z","timestamp":1452604737000},"page":"176-187","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Formal verification of control-flow graph flattening"],"prefix":"10.1145","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[{"name":"IRISA, France \/ Universit\u00e9 Rennes 1, France"}]},{"given":"Alix","family":"Trieu","sequence":"additional","affiliation":[{"name":"IRISA, France \/ ENS Rennes, France"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"URL http:\/\/www.irisa.fr\/celtique\/ext\/cfg-flatten. Companion website.  URL http:\/\/www.irisa.fr\/celtique\/ext\/cfg-flatten. Companion website."},{"key":"e_1_3_2_1_2_1","volume-title":"20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007","volume":"4732","author":"Appel A. W.","year":"2007","unstructured":"A. W. Appel and S. Blazy . Separation Logic for Small-step Cminor. In Springer-Verlag, editor , 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007 ), volume 4732 of Lecture Notes in Computer Science, pages 5\u201321, Kaiserslautern, Germany , Sept. 2007 . A. W. Appel and S. Blazy. Separation Logic for Small-step Cminor. In Springer-Verlag, editor, 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of Lecture Notes in Computer Science, pages 5\u201321, Kaiserslautern, Germany, Sept. 2007."},{"key":"e_1_3_2_1_3_1","first-page":"18","volume-title":"Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology","author":"Barak B.","unstructured":"B. Barak , O. Goldreich , R. Impagliazzo , S. Rudich , A. Sahai , S. P. Vadhan , and K. Yang . On the (im)possibility of obfuscating programs. In CRYPTO \u201901 : Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology , pages 1\u2013 18 . Springer-Verlag, 2001. ISBN 3-540-42456-3. B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. P. Vadhan, and K. Yang. On the (im)possibility of obfuscating programs. In CRYPTO \u201901: Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology, pages 1\u201318. Springer-Verlag, 2001. ISBN 3-540-42456-3."},{"key":"e_1_3_2_1_4_1","volume-title":"SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop","author":"Blazy S.","year":"2012","unstructured":"S. Blazy and R. Giacobazzi . Towards a formally verified obfuscating compiler. In C. Collberg, editor , SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop , Beijing, China , June 2012 . ACM SIGPLAN. S. Blazy and R. Giacobazzi. Towards a formally verified obfuscating compiler. In C. Collberg, editor, SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Beijing, China, June 2012. ACM SIGPLAN."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_3_2_1_7_1","volume-title":"The tigress C diversifier\/obfuscator","author":"Collberg C.","year":"2014","unstructured":"C. Collberg . The tigress C diversifier\/obfuscator , 2014 -2015. URL http:\/\/tigress.cs.arizona.edu\/. C. Collberg. The tigress C diversifier\/obfuscator, 2014-2015. URL http:\/\/tigress.cs.arizona.edu\/."},{"key":"e_1_3_2_1_8_1","volume-title":"Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection","author":"Collberg C.","year":"2009","unstructured":"C. Collberg and J. Nagra . Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection . Addison-Wesley Software Security Series. Addison-Wesley , 2009 . C. Collberg and J. Nagra. Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley Software Security Series. Addison-Wesley, 2009."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027797"},{"key":"e_1_3_2_1_10_1","first-page":"314","volume-title":"10th International Conference, ISC 2007, Valpara\u00b4\u0131so, Chile, October 9-12, 2007","author":"Drape S.","year":"2007","unstructured":"S. Drape , C. D. Thomborson , and A. Majumdar . Specifying imperative data obfuscations. In Information Security , 10th International Conference, ISC 2007, Valpara\u00b4\u0131so, Chile, October 9-12, 2007 , Proceedings , pages 299\u2013 314 , 2007 . S. Drape, C. D. Thomborson, and A. Majumdar. Specifying imperative data obfuscations. In Information Security, 10th International Conference, ISC 2007, Valpara\u00b4\u0131so, Chile, October 9-12, 2007, Proceedings, pages 299\u2013314, 2007."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2821429.2821434"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_14_1","volume-title":"10th Asian Symposium, APLAS 2012","volume":"7705","author":"Leroy X.","year":"2012","unstructured":"X. Leroy . Mechanized semantics for compiler verification. In R. Jhala and A. Igarashi, editors, Programming Languages and Systems , 10th Asian Symposium, APLAS 2012 , volume 7705 of Lecture Notes in Computer Science, pages 386\u2013388. Springer , 2012 . X. Leroy. Mechanized semantics for compiler verification. In R. Jhala and A. Igarashi, editors, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of Lecture Notes in Computer Science, pages 386\u2013388. Springer, 2012."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375696.1375702"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948149"},{"volume-title":"The CompCert formally verified compiler. Inria","year":"2008","key":"e_1_3_2_1_18_1","unstructured":"The CompCert development team. The CompCert formally verified compiler. Inria , 2008 -2015. URL http:\/\/compcert.inria.fr. Version 2.5. The CompCert development team. The CompCert formally verified compiler. Inria, 2008-2015. URL http:\/\/compcert.inria.fr. Version 2.5."},{"volume-title":"Inria","year":"2012","key":"e_1_3_2_1_19_1","unstructured":"The Coq development team. The Coq proof assistant reference manual . Inria , 2012 . URL http:\/\/coq.inria.fr. Version 8.4. The Coq development team. The Coq proof assistant reference manual. Inria, 2012. URL http:\/\/coq.inria.fr. Version 8.4."},{"key":"e_1_3_2_1_20_1","volume-title":"University of Virginia","author":"Wang C.","year":"2001","unstructured":"C. Wang . A security architecture for survivability mechanisms. PhD thesis , University of Virginia , 2001 . C. Wang. A security architecture for survivability mechanisms. PhD thesis, University of Virginia, 2001."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1984.1659158"}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854082","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854082","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:47Z","timestamp":1750225727000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":21,"alternative-id":["10.1145\/2854065.2854082","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854082","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}