{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:12:01Z","timestamp":1763968321028,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294103","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"196-208","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions"],"prefix":"10.1145","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}]},{"given":"R\u00e9mi","family":"Hutin","sequence":"additional","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Christian Collberg (Ed.). ACM SIGPLAN","author":"Blazy Sandrine","year":"2012","unstructured":"Sandrine Blazy and Roberto Giacobazzi . 2012 . Towards a formally verified obfuscating compiler . In SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Christian Collberg (Ed.). ACM SIGPLAN , Beijing, China. Sandrine Blazy and Roberto Giacobazzi. 2012. Towards a formally verified obfuscating compiler. In SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Christian Collberg (Ed.). ACM SIGPLAN, Beijing, China."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854082"},{"key":"e_1_3_2_1_4_1","unstructured":"Christian Collberg. 2014-2015. The Tigress C Diversifier\/Obfuscator. http:\/\/tigress.cs.arizona.edu\/  Christian Collberg. 2014-2015. The Tigress C Diversifier\/Obfuscator. http:\/\/tigress.cs.arizona.edu\/"},{"key":"e_1_3_2_1_5_1","volume-title":"Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection","author":"Collberg Christian","year":"2009","unstructured":"Christian Collberg and Jasvir Nagra . 2009 . Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection . Addison-Wesley . Christian Collberg and Jasvir Nagra. 2009. Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027797"},{"key":"e_1_3_2_1_7_1","unstructured":"Companion website 2018. http:\/\/people.irisa.fr\/Remi.Hutin\/mbaobf  Companion website 2018. http:\/\/people.irisa.fr\/Remi.Hutin\/mbaobf"},{"key":"e_1_3_2_1_8_1","volume-title":"10th International Conference, ISC 2007, Valpara\u00edso, Chile, October 9-12, 2007, Proceedings. 299\u2013314","author":"Drape Stephen","year":"2007","unstructured":"Stephen Drape , Clark D. Thomborson , and Anirban Majumdar . 2007 . Specifying Imperative Data Obfuscations. In Information Security , 10th International Conference, ISC 2007, Valpara\u00edso, Chile, October 9-12, 2007, Proceedings. 299\u2013314 . Stephen Drape, Clark D. Thomborson, and Anirban Majumdar. 2007. Specifying Imperative Data Obfuscations. In Information Security, 10th International Conference, ISC 2007, Valpara\u00edso, Chile, October 9-12, 2007, Proceedings. 299\u2013314."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2995306.2995308"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPRO.2015.10"},{"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","unstructured":"The CompCert development team. 2008-2018. The CompCert formally verified compiler. Inria. http:\/\/compcert.inria.fr Version 3.4.  The CompCert development team. 2008-2018. The CompCert formally verified compiler. Inria. http:\/\/compcert.inria.fr Version 3.4."},{"key":"e_1_3_2_1_15_1","unstructured":"The Coq development team. 2018. The Coq proof assistant reference manual. Inria. http:\/\/coq.inria.fr Version 8.8.1.  The Coq development team. 2018. The Coq proof assistant reference manual. Inria. http:\/\/coq.inria.fr Version 8.8.1."},{"key":"e_1_3_2_1_16_1","volume-title":"Hacker\u2019s Delight","author":"Warren Henry S.","unstructured":"Henry S. Warren . 2012. Hacker\u2019s Delight ( 2 nd ed.). Addison-Wesley Professional . Henry S. Warren. 2012. Hacker\u2019s Delight (2nd ed.). Addison-Wesley Professional.","edition":"2"},{"volume-title":"Diversity via Code Transformations: A Solution for NGNA Renewable Security","author":"Zhou Yongxin","key":"e_1_3_2_1_17_1","unstructured":"Yongxin Zhou and Alec Main . 2006. Diversity via Code Transformations: A Solution for NGNA Renewable Security . In The National Cable and Telecommunications Association Show . 173\u2013182. Yongxin Zhou and Alec Main. 2006. Diversity via Code Transformations: A Solution for NGNA Renewable Security. In The National Cable and Telecommunications Association Show. 173\u2013182."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1784964.1784971"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294103","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":17,"alternative-id":["10.1145\/3293880.3294103","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294103","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}