{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:18Z","timestamp":1750221018745,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,26]],"date-time":"2019-08-26T00:00:00Z","timestamp":1566777600000},"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,8,26]]},"DOI":"10.1145\/3387168.3387257","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:25:51Z","timestamp":1590452751000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Tactics for Proving Separation Logic Assertion in Coq Proof Assistant"],"prefix":"10.1145","author":[{"given":"Siran","family":"Lei","sequence":"first","affiliation":[{"name":"Department of Mathematics, Liaoning Normal University, Dalian, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengqi","family":"Cheng","sequence":"additional","affiliation":[{"name":"Department of Mathematics, Liaoning Normal University, Dalian, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianguo","family":"jiang","sequence":"additional","affiliation":[{"name":"Department of Mathematics, Liaoning Normal University, Dalian, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,5,25]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"ICFP, 391--402.","author":"Chlipala A.","year":"2013","unstructured":"A. Chlipala ( 2013 ). The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier . In ICFP, 391--402. A. Chlipala (2013). The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP, 391--402."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_24"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_18"},{"key":"#cr-split#-e_1_3_2_1_4_1.1","doi-asserted-by":"crossref","unstructured":"A. W. Appel R. Dockins A. Hobor L. Beringer J. Dodds G. Stewart S. Blazy and X. Leroy. 2014. Program Logics for Certified Compilers. University of Cambridge Press New York. DOI: http:\/\/dx.doi.org\/10.1017\/CBO9781107256552. 10.1017\/CBO9781107256552","DOI":"10.1017\/CBO9781107256552"},{"key":"#cr-split#-e_1_3_2_1_4_1.2","doi-asserted-by":"crossref","unstructured":"A. W. Appel R. Dockins A. Hobor L. Beringer J. Dodds G. Stewart S. Blazy and X. Leroy. 2014. Program Logics for Certified Compilers. University of Cambridge Press New York. DOI: http:\/\/dx.doi.org\/10.1017\/CBO9781107256552.","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceeding softhe 7th International Conference on Logic for Programming and Automated Reasoning (LPAP'00), 85--95.","author":"Delahaye D.","year":"2000","unstructured":"D. Delahaye ( 2000 ). A tactic Language for the System Coq . In Proceeding softhe 7th International Conference on Logic for Programming and Automated Reasoning (LPAP'00), 85--95. D. Delahaye (2000). A tactic Language for the System Coq. In Proceeding softhe 7th International Conference on Logic for Programming and Automated Reasoning (LPAP'00), 85--95."},{"key":"e_1_3_2_1_7_1","volume-title":"POPL, 97--108.","author":"Tuch H.","year":"2007","unstructured":"H. Tuch , G. Klein , and M. Norrish ( 2007 ). Types, butes, and separation logic . In POPL, 97--108. H. Tuch, G. Klein, and M. Norrish (2007). Types, butes, and separation logic. In POPL, 97--108."},{"key":"e_1_3_2_1_8_1","volume-title":"PLDI, 77--87.","author":"Sergey I.","year":"2015","unstructured":"I. Sergey , A. Nanevski , and A. Banerjee ( 2015 ). Mechanized verification of fine-grained concurrent programs . In PLDI, 77--87. I. Sergey, A. Nanevski, and A. Banerjee (2015). Mechanized verification of fine-grained concurrent programs. In PLDI, 77--87."},{"key":"e_1_3_2_1_9_1","volume-title":"POPL, 301--314.","author":"Jensen J. B.","year":"2013","unstructured":"J. B. Jensen , N. Benton , and A. Kennedy ( 2013 ). High-level separation logic for low-level code . In POPL, 301--314. J. B. Jensen, N. Benton, and A. Kennedy (2013). High-level separation logic for low-level code. In POPL, 301--314."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_21"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_12_1","volume-title":"CPP, 97--108.","author":"Cao J.","year":"2015","unstructured":"J. Cao , M. Fu , and X. Feng ( 2015 ). Practical Tactics for Verifying C Programs in Coq . In: CPP, 97--108. J. Cao, M. Fu, and X. Feng (2015). Practical Tactics for Verifying C Programs in Coq. In: CPP, 97--108."},{"key":"e_1_3_2_1_13_1","volume-title":"Creating Safety Requirement Traceability for Assuring and Recertifying Legacy Safety-Critical Systems[M] IEEE, 297--302","author":"Hill J.","year":"2010","unstructured":"J. Hill , S. Tilley ( 2010 ). Creating Safety Requirement Traceability for Assuring and Recertifying Legacy Safety-Critical Systems[M] IEEE, 297--302 . J. Hill, S. Tilley (2010). Creating Safety Requirement Traceability for Assuring and Recertifying Legacy Safety-Critical Systems[M] IEEE, 297--302."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_1_16_1","volume-title":"The C Standard formalized in Coq. Ph. D. Dissertation","author":"Krebbers R.","year":"2015","unstructured":"R. Krebbers ( 2015 ). The C Standard formalized in Coq. Ph. D. Dissertation . Radboud University . R. Krebbers (2015). The C Standard formalized in Coq. Ph. D. Dissertation. Radboud University."},{"key":"e_1_3_2_1_17_1","unstructured":"The coq development team: The coq proof assistant. http:\/\/coq.inria.fr.  The coq development team: The coq proof assistant. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 33th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 42--54","author":"Leroy X.","year":"2006","unstructured":"X. Leroy ( 2006 ). Formal certification of a complier back-end, or: programming a complier with a proof assistant . In Proceedings of the 33th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 42--54 . X. Leroy (2006). Formal certification of a complier back-end, or: programming a complier with a proof assistant. In Proceedings of the 33th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 42--54."}],"event":{"name":"ICVISP 2019: 3rd International Conference on Vision, Image and Signal Processing","acronym":"ICVISP 2019","location":"Vancouver BC Canada"},"container-title":["Proceedings of the 3rd International Conference on Vision, Image and Signal Processing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387168.3387257","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387168.3387257","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:17Z","timestamp":1750206377000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387168.3387257"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,26]]},"references-count":19,"alternative-id":["10.1145\/3387168.3387257","10.1145\/3387168"],"URL":"https:\/\/doi.org\/10.1145\/3387168.3387257","relation":{},"subject":[],"published":{"date-parts":[[2019,8,26]]},"assertion":[{"value":"2020-05-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}