{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:03Z","timestamp":1772164023841,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,9,27]],"date-time":"2010-09-27T00:00:00Z","timestamp":1285545600000},"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":[[2010,9,27]]},"DOI":"10.1145\/1863543.1863590","type":"proceedings-article","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T13:41:50Z","timestamp":1285681310000},"page":"321-332","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Program verification through characteristic formulae"],"prefix":"10.1145","author":[{"given":"Arthur","family":"Chargu\u00e9raud","sequence":"first","affiliation":[{"name":"INRIA, Rocquencourt, France"}]}],"member":"320","published-online":{"date-parts":[[2010,9,27]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Verification of object-oriented programs with invariants. JOT, 3(6)","author":"Barnett Mike","year":"2004","unstructured":"}} Mike Barnett , Rob DeLine , Manuel F\u00e4hndrich , K. Rustan M. Leino , and Wolfram Schulte . Verification of object-oriented programs with invariants. JOT, 3(6) , 2004 . }}Mike Barnett, Rob DeLine, Manuel F\u00e4hndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. JOT, 3(6), 2004."},{"key":"e_1_3_2_2_2_1","unstructured":"}}Arthur Chargu\u00e9raud. Verification of call-by-value functional programs through a deep embedding. Unpublished. http:\/\/arthur.chargueraud.org\/research\/2009\/deep\/ March 2009.  }}Arthur Chargu\u00e9raud. Verification of call-by-value functional programs through a deep embedding. Unpublished. http:\/\/arthur.chargueraud.org\/research\/2009\/deep\/ March 2009."},{"key":"e_1_3_2_2_3_1","unstructured":"}}Arthur Chargu\u00e9raud. Technical appendix to the current paper. http:\/\/arthur.chargueraud.org\/research\/2010\/cfml\/ April 2010.  }}Arthur Chargu\u00e9raud. Technical appendix to the current paper. http:\/\/arthur.chargueraud.org\/research\/2010\/cfml\/ April 2010."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_2_5_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/11542384_9","volume-title":"Freek Wiedijk","author":"Coquand Thierry","year":"2006","unstructured":"}} Thierry Coquand . Alfa\/agda. In Freek Wiedijk , editor, The Seventeen Provers of the World, volume 3600 of Lecture Notes in Computer Science , pages 50 -- 54 . Springer , 2006 . }}Thierry Coquand. Alfa\/agda. In Freek Wiedijk, editor, The Seventeen Provers of the World, volume 3600 of Lecture Notes in Computer Science, pages 50--54. Springer, 2006."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134028"},{"key":"e_1_3_2_2_7_1","first-page":"15","volume-title":"6th ICFEM 2004","volume":"3308","author":"Filli\u00e2tre Jean-Christophe","year":"2004","unstructured":"}} Jean-Christophe Filli\u00e2tre and Claude March\u00e9 . Multi-prover verification of C programs. In Formal Methods and Software Engineering , 6th ICFEM 2004 , volume 3308 of LNCS, pages 15 -- 29 . Springer-Verlag , 2004 . }}Jean-Christophe Filli\u00e2tre and Claude March\u00e9. Multi-prover verification of C programs. In Formal Methods and Software Engineering, 6th ICFEM 2004, volume 3308 of LNCS, pages 15--29. Springer-Verlag, 2004."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_31"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596627.1596634"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"crossref","unstructured":"}}\n      Henri\n      Korver\n    .\n  Computing distinguishing formulas for branching bisimulation\n  . In Kim Guldstrand Larsen and Arne Skou editors CAV volume \n  575\n   of \n  LNCS pages \n  13\n  --\n  23\n  . \n  Springer 1991\n  .   }}Henri Korver. Computing distinguishing formulas for branching bisimulation. In Kim Guldstrand Larsen and Arne Skou editors CAV volume 575 of LNCS pages 13--23. Springer 1991.","DOI":"10.1007\/3-540-55179-4_3"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"issue":"1","key":"e_1_3_2_2_14_1","first-page":"89","article-title":"The Krakatoa tool for certification of Java\\slash JavaCard programs annotated","volume":"58","author":"March\u00e9 Claude","year":"2004","unstructured":"}} Claude March\u00e9 , Christine Paulin Mohring , and Xavier Urbain . The Krakatoa tool for certification of Java\\slash JavaCard programs annotated in JML. JLAP , 58 ( 1-2 ): 89 -- 106 , 2004 . }}Claude March\u00e9, Christine Paulin Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java\\slash JavaCard programs annotated in JML. JLAP, 58(1-2):89--106, 2004.","journal-title":"JML. JLAP"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"crossref","unstructured":"}}\n      Farhad\n      Mehta\n     and \n      Tobias\n      Nipkow\n    .\n  Proving pointer programs in higher-order logic\n  . In Franz Baader editor CADE volume \n  2741\n   of \n  LNCS pages \n  121\n  --\n  135\n  . \n  Springer 2003\n  .  }}Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. In Franz Baader editor CADE volume 2741 of LNCS pages 121--135. Springer 2003.","DOI":"10.1007\/978-3-540-45085-6_10"},{"key":"e_1_3_2_2_17_1","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989","unstructured":"}} R. Milner . Communication and Concurrency . Prentice-Hall , 1989 . }}R. Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517444"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_2_2_22_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","year":"1999","unstructured":"}} Chris Okasaki . Purely Functional Data Structures . Cambridge University Press , 1999 . }}Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999."},{"key":"e_1_3_2_2_23_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science: 5th GI-Conference, Karlsruhe","author":"Park David","year":"1981","unstructured":"}} David Park . Concurrency and automata on infinite sequences . In Peter Deussen, editor, Theoretical Computer Science: 5th GI-Conference, Karlsruhe , volume 104 of LNCS , pages 167 -- 183 , Berlin, Heidelberg , and New York, March 1981 . Springer-Verlag . }}David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science: 5th GI-Conference, Karlsruhe, volume 104 of LNCS, pages 167--183, Berlin, Heidelberg, and New York, March 1981. Springer-Verlag."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_17"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291220.1291156"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542514"}],"event":{"name":"ICFP '10: ACM SIGPLAN International Conference on Functional Programming","location":"Baltimore Maryland USA","acronym":"ICFP '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 15th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863543.1863590","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1863543.1863590","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:39:52Z","timestamp":1750232392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863543.1863590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,27]]},"references-count":25,"alternative-id":["10.1145\/1863543.1863590","10.1145\/1863543"],"URL":"https:\/\/doi.org\/10.1145\/1863543.1863590","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1932681.1863590","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,9,27]]},"assertion":[{"value":"2010-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}