{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:46:56Z","timestamp":1768002416638,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T00:00:00Z","timestamp":1554681600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Union","award":["731453"],"award-info":[{"award-number":["731453"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,4,8]]},"DOI":"10.1145\/3297280.3297495","type":"proceedings-article","created":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T12:18:47Z","timestamp":1556713127000},"page":"2186-2195","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Logic against ghosts"],"prefix":"10.1145","author":[{"given":"Allan","family":"Blanchard","sequence":"first","affiliation":[{"name":"Inria Lille, Villeneuve d'Ascq, France"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[{"name":"Software Reliability Lab, Gif-sur-Yvette, France"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[{"name":"Northern Arizona University"}]}],"member":"320","published-online":{"date-parts":[[2019,4,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987212"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_2_1_4_1","volume-title":"ACSL: ANSI\/ISO C Specification Language","author":"Baudin Patrick","year":"2018","unstructured":"Patrick Baudin, Pascal Cuoq, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2018. ACSL: ANSI\/ISO C Specification Language. http:\/\/frama-c.com\/acsl.html"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Springer.","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_3"},{"key":"e_1_3_2_1_7_1","unstructured":"Jochen Burghardt and Jens Gerlach. 2018. ACSL by Example. https:\/\/github.com\/fraunhoferfokus\/acsl-by-example"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_16"},{"key":"e_1_3_2_1_9_1","volume-title":"NFM 2017, Moffett Field, CA, USA, May 16--18, 2017, Proceedings. 68--83","author":"Dross Claire","year":"2017","unstructured":"Claire Dross and Yannick Moy. 2017. Auto-Active Proof of Red-Black Trees in SPARK. In NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16--18, 2017, Proceedings. 68--83."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCN.2004.38"},{"key":"e_1_3_2_1_11_1","volume-title":"Where Programs Meet Provers. In ESOP","author":"Filli\u00e2tre Jean-Christophe","year":"2013","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. {n. d.}. Why3 - Where Programs Meet Provers. In ESOP 2013."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2793736.2794063"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986314"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_2_1_16_1","volume-title":"Runtime Verification (RV) (September 24--27) (LNCS)","author":"Kosmatov Nikolai","unstructured":"Nikolai Kosmatov and Julien Signoles. 2013. A Lesson on Runtime Assertion Checking with Frama-C. In Runtime Verification (RV) (September 24--27) (LNCS), Vol. 8174. Springer, 386--399."},{"key":"e_1_3_2_1_17_1","volume-title":"Leino and Micha\u0142 Moskal","author":"K. Rustan","year":"2010","unstructured":"K. Rustan M. Leino and Micha\u0142 Moskal. 2010. Usable Auto-Active Verification. http:\/\/fm.csl.sri.com\/UV10\/"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-92994-1_11"},{"key":"e_1_3_2_1_19_1","volume-title":"CRiSIS 2016 (LNCS)","volume":"10158","author":"Mangano Fr\u00e9d\u00e9ric","year":"2016","unstructured":"Fr\u00e9d\u00e9ric Mangano, Simon Duquennoy, and Nikolai Kosmatov. 2016. A Memory Allocation Module of Contiki Formally Verified with Frama-C. A Case Study. In CRiSIS 2016 (LNCS), Vol. 10158. Springer."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133911"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3234847.3234910"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.01.006"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1884866.1884880"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_25_1","unstructured":"The Coq Development Team. {n. d.}. The Coq Proof Assistant. http:\/\/coq.inria.fr ."},{"key":"e_1_3_2_1_26_1","volume-title":"Logical Methods in Computer Science 11, 3","author":"Vogels Fr\u00e9d\u00e9ric","year":"2015","unstructured":"Fr\u00e9d\u00e9ric Vogels, Bart Jacobs, and Frank Piessens. 2015. Featherweight Veri-Fast. Logical Methods in Computer Science 11, 3 (2015)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"}],"event":{"name":"SAC '19: The 34th ACM\/SIGAPP Symposium on Applied Computing","location":"Limassol Cyprus","acronym":"SAC '19","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"]},"container-title":["Proceedings of the 34th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3297280.3297495","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3297280.3297495","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:54:15Z","timestamp":1750204455000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3297280.3297495"}},"subtitle":["comparison of two proof approaches for a list module"],"short-title":[],"issued":{"date-parts":[[2019,4,8]]},"references-count":27,"alternative-id":["10.1145\/3297280.3297495","10.1145\/3297280"],"URL":"https:\/\/doi.org\/10.1145\/3297280.3297495","relation":{},"subject":[],"published":{"date-parts":[[2019,4,8]]},"assertion":[{"value":"2019-04-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}