{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:26Z","timestamp":1767929306977,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,7,2]],"date-time":"2013-07-02T00:00:00Z","timestamp":1372723200000},"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":[[2013,7,2]]},"DOI":"10.1145\/2489837.2489838","type":"proceedings-article","created":{"date-parts":[[2013,7,24]],"date-time":"2013-07-24T13:26:51Z","timestamp":1374672411000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["An overview of the Leon verification system"],"prefix":"10.1145","author":[{"given":"R\u00e9gis","family":"Blanc","sequence":"first","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (EPFL), Switzerland"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (EPFL), Switzerland"}]},{"given":"Etienne","family":"Kneuss","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (EPFL), Switzerland"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (EPFL), Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2013,7,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00007-6"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/800022.808306"},{"key":"e_1_3_2_1_3_1","volume-title":"Automatic predicate abstraction of C programs","author":"Ball T.","year":"2001","unstructured":"T. Ball , R. Majumdar , T. Millstein , and S. K. Rajamani . Automatic predicate abstraction of C programs . 2001 . T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. 2001."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_6_1","first-page":"171","volume-title":"CAV","author":"Barrett C.","year":"2011","unstructured":"C. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . CVC4 . In CAV , pages 171 -- 177 , 2011 . C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In CAV, pages 171--177, 2011."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development -- Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development -- Coq'Art: The Calculus of Inductive Constructions . Springer , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development -- Coq'Art: The Calculus of Inductive Constructions. Springer, 2004."},{"key":"e_1_3_2_1_8_1","volume-title":"EPFL","author":"Blanc R. W.","year":"2012","unstructured":"R. W. Blanc . Verification of Imperative Programs in Scala. Master's thesis , EPFL , 2012 . R. W. Blanc. Verification of Imperative Programs in Scala. Master's thesis, EPFL, 2012."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines","author":"B\u00f6rger E.","year":"2003","unstructured":"E. B\u00f6rger and R. St\u00e4rk . Abstract State Machines . 2003 . E. B\u00f6rger and R. St\u00e4rk. Abstract State Machines. 2003."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_11_1","volume-title":"A discipline of programming","author":"Dijkstra E. W.","year":"1976","unstructured":"E. W. Dijkstra . A discipline of programming . Prentice-Hall , Englewood Cliffs , N.J, 1976 . E. W. Dijkstra. A discipline of programming. Prentice-Hall, Englewood Cliffs, N.J, 1976."},{"key":"e_1_3_2_1_12_1","volume-title":"The Yices SMT solver","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. M. de Moura . The Yices SMT solver , 2006 . B. Dutertre and L. M. de Moura. The Yices SMT solver, 2006."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"e_1_3_2_1_15_1","first-page":"102","volume-title":"Reflections on the Work of C. A. R. Hoare, History of Computing","author":"Gordon M.","year":"2010","unstructured":"M. Gordon and H. Collavizza . Forward with Hoare . In A. Roscoe, C. B. Jones, and K. R. Wood, editors, Reflections on the Work of C. A. R. Hoare, History of Computing , pages 102 -- 121 . Springer , 2010 . M. Gordon and H. Collavizza. Forward with Hoare. In A. Roscoe, C. B. Jones, and K. R. Wood, editors, Reflections on the Work of C. A. R. Hoare, History of Computing, pages 102--121. Springer, 2010."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_3_2_1_18_1","volume-title":"Higher-Order Workshop on Automated Runtime Verification and Debugging","author":"Havelund K.","year":"2011","unstructured":"K. Havelund . Closing the gap between specification and programming: VDM++ and Scala . In Higher-Order Workshop on Automated Runtime Verification and Debugging , 2011 . K. Havelund. Closing the gap between specification and programming: VDM++ and Scala. In Higher-Order Workshop on Automated Runtime Verification and Debugging, 2011."},{"key":"e_1_3_2_1_19_1","volume-title":"Systematic Software Development using VDM","author":"Jones C. B.","year":"1986","unstructured":"C. B. Jones . Systematic Software Development using VDM . Prentice Hall , 1986 . C. B. Jones. Systematic Software Development using VDM. Prentice Hall, 1986."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/555902"},{"key":"e_1_3_2_1_21_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann M.","year":"2000","unstructured":"M. Kaufmann , P. Manolios , and J. S. Moore . Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , 2000 . M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000."},{"key":"e_1_3_2_1_23_1","volume-title":"EPFL","author":"K\u00f6ksal A. S.","year":"2011","unstructured":"A. S. K\u00f6ksal . Constraint programming in Scala. Master's thesis , EPFL , 2011 . A. S. K\u00f6ksal. Constraint programming in Scala. Master's thesis, EPFL, 2011."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032296"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2402676.2402682"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260921"},{"key":"e_1_3_2_1_27_1","volume-title":"Eiffel: the language","author":"Meyer B.","year":"1991","unstructured":"B. Meyer . Eiffel: the language . Prentice-Hall , 1991 . B. Meyer. Eiffel: the language. Prentice-Hall, 1991."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277752"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_3_2_1_30_1","series-title":"LNCS","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939399.1939405"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003494"},{"key":"e_1_3_2_1_33_1","volume-title":"VSTTE","author":"Pham T.-H.","year":"2013","unstructured":"T.-H. Pham and M. Whalen . An improved unrolling-based decision procedure for algebraic data types . In VSTTE , 2013 . To appear. T.-H. Pham and M. Whalen. An improved unrolling-based decision procedure for algebraic data types. In VSTTE, 2013. To appear."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041575"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_28"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103767"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"}],"event":{"name":"ECOOP '13: European Conference on Object-Oriented Programming","location":"Montpellier France","acronym":"ECOOP '13","sponsor":["CNRS Centre National De La Rechercue Scientifique","UM2 University Montpellier 2","AITO Assoc Internationale por les Technologies Objects","SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 4th Workshop on Scala"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2489837.2489838","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2489837.2489838","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:39:26Z","timestamp":1750235966000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2489837.2489838"}},"subtitle":["verification by translation to recursive functions"],"short-title":[],"issued":{"date-parts":[[2013,7,2]]},"references-count":38,"alternative-id":["10.1145\/2489837.2489838","10.1145\/2489837"],"URL":"https:\/\/doi.org\/10.1145\/2489837.2489838","relation":{},"subject":[],"published":{"date-parts":[[2013,7,2]]},"assertion":[{"value":"2013-07-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}