{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:39:42Z","timestamp":1780115982440,"version":"3.54.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,20]],"date-time":"2018-09-20T00:00:00Z","timestamp":1537401600000},"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":[[2018,9,20]]},"DOI":"10.1145\/3264637.3264649","type":"proceedings-article","created":{"date-parts":[[2018,9,10]],"date-time":"2018-09-10T12:11:35Z","timestamp":1536581495000},"page":"90-97","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards progressive program verification in Dafny"],"prefix":"10.1145","author":[{"given":"Ismael","family":"Figueroa","sequence":"first","affiliation":[{"name":"Pontificia Universidad, Valpara\u00edso, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno","family":"Garc\u00eda","sequence":"additional","affiliation":[{"name":"Pontificia Universidad, Valpara\u00edso, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Leger","sequence":"additional","affiliation":[{"name":"Universidad Cat\u00f3lica del Norte, Coquimbo, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2018. The Java Modeling Language (JML). https:\/\/www.eecs.ucf.edu\/leavens\/JML\/index.shtml.  2018. The Java Modeling Language (JML). https:\/\/www.eecs.ucf.edu\/leavens\/JML\/index.shtml."},{"key":"e_1_3_2_1_2_1","volume-title":"Jorge Sousa Pinto, and Sim\u00e3o Melo de Sousa.","author":"Almeida Jos\u00e9 Bacelar","year":"2011","unstructured":"Jos\u00e9 Bacelar Almeida , Maria Jo\u00e3o Frade , Jorge Sousa Pinto, and Sim\u00e3o Melo de Sousa. 2011 . Rigorous Software Development: An Introduction to Program Verification (1st ed.). Springer-Verlag . Jos\u00e9 Bacelar Almeida, Maria Jo\u00e3o Frade, Jorge Sousa Pinto, and Sim\u00e3o Melo de Sousa. 2011. Rigorous Software Development: An Introduction to Program Verification (1st ed.). Springer-Verlag."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"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","unstructured":"Clark W Barrett Roberto Sebastiani Sanjit A Seshia Cesare Tinelli etal 2009. Satisfiability modulo theories. Handbook of satisfiability 185 (2009) 825--885.  Clark W Barrett Roberto Sebastiani Sanjit A Seshia Cesare Tinelli et al. 2009. Satisfiability modulo theories. Handbook of satisfiability 185 (2009) 825--885."},{"key":"e_1_3_2_1_6_1","unstructured":"Patrick Baudin Pascal Cuoq Jean-Cristophe Filli\u00e2tre Claude March\u00e9 Benjamin Monate Yannick Moy and Virgile Prevosto. 2018. The ANSI\/ISO C Specification Language (ACSL). https:\/\/frama-c.com\/acsl.html.  Patrick Baudin Pascal Cuoq Jean-Cristophe Filli\u00e2tre Claude March\u00e9 Benjamin Monate Yannick Moy and Virgile Prevosto. 2018. The ANSI\/ISO C Specification Language (ACSL). https:\/\/frama-c.com\/acsl.html."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_9_1","unstructured":"Dart Team. 2013. Dart Programming Language Specification. Version 0.41.  Dart Team. 2013. Dart Programming Language Specification. Version 0.41."},{"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","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480593"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/6294.846201"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774531"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0211-0"},{"key":"e_1_3_2_1_15_1","unstructured":"M\u00f6ssenb\u00f6ck Hanspeter L\u00f6berbauer Markus and W\u00f6\u00dfAlbrecht. 2018. The Compiler Generator Coco\/R. http:\/\/www.ssw.uni-linz.ac.at\/Coco\/.  M\u00f6ssenb\u00f6ck Hanspeter L\u00f6berbauer Markus and W\u00f6\u00dfAlbrecht. 2018. The Compiler Generator Coco\/R. http:\/\/www.ssw.uni-linz.ac.at\/Coco\/."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2005.314"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"G. Kiczales J. Irwin J. Lamping J. Loingtier C.V. Lopes C. Maeda and A. Mendhekar. 1996. Aspect Oriented Programming. In Special Issues in Object-Oriented Programming. Max Muehlhaeuser (general editor) et al.  G. Kiczales J. Irwin J. Lamping J. Loingtier C.V. Lopes C. Maeda and A. Mendhekar. 1996. Aspect Oriented Programming. In Special Issues in Object-Oriented Programming. Max Muehlhaeuser (general editor) et al.","DOI":"10.1007\/BFb0053381"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_3_2_1_19_1","unstructured":"J. Lehtosalo and contributors. 2018. MyPy - optional static typing for Python. http:\/\/mypy-lang.org.  J. Lehtosalo and contributors. 2018. MyPy - optional static typing for Python. http:\/\/mypy-lang.org."},{"key":"e_1_3_2_1_20_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness . Springer Berlin Heidelberg , Berlin, Heidelberg , 348--370. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. Springer Berlin Heidelberg, Berlin, Heidelberg, 348--370."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_1_23_1","volume-title":"Behavior Modification: The evolution of behavior-driven development. Better Software 8, 3","author":"North D","year":"2006","unstructured":"D North . 2006 . Behavior Modification: The evolution of behavior-driven development. Better Software 8, 3 (2006). D North. 2006. Behavior Modification: The evolution of behavior-driven development. Better Software 8, 3 (2006)."},{"key":"e_1_3_2_1_24_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press , Cambridge, MA, USA . Benjamin C. Pierce. 2002. Types and programming languages. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Benjamin C. Pierce (Ed.). 2005. Advanced Topics in Types and Programming Languages. MIT Press Cambridge MA USA.   Benjamin C. Pierce (Ed.). 2005. Advanced Topics in Types and Programming Languages. MIT Press Cambridge MA USA.","DOI":"10.7551\/mitpress\/1104.001.0001"},{"key":"e_1_3_2_1_26_1","volume-title":"Software Engineering: A Practitioner's Approach (7 ed.)","author":"Pressman Roger","year":"2010","unstructured":"Roger Pressman . 2010 . Software Engineering: A Practitioner's Approach (7 ed.) . McGraw-Hill, Inc. , New York, NY, USA . Roger Pressman. 2010. Software Engineering: A Practitioner's Approach (7 ed.). McGraw-Hill, Inc., New York, NY, USA."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2577080.2577084"},{"key":"e_1_3_2_1_28_1","unstructured":"MicrosoftResearch. 2018. Dafny - guide. https:\/\/rise4fun.com\/Dafny\/tutorial.  MicrosoftResearch. 2018. Dafny - guide. https:\/\/rise4fun.com\/Dafny\/tutorial."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882362.1882432"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. 81--92","author":"Siek Jeremy","year":"2006","unstructured":"Jeremy Siek and Walid Taha . 2006 . Gradual Typing for Functional Languages . In Proceedings of the Scheme and Functional Programming Workshop. 81--92 . Jeremy Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the Scheme and Functional Programming Workshop. 81--92."},{"key":"e_1_3_2_1_31_1","volume-title":"Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs))","volume":"32","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek , Michael M. Vitousek , Matteo Cimini , and John Tang Boyland . 2015 . Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)) , Vol. 32 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Asilomar, California, USA, 274--293. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Asilomar, California, USA, 274--293."},{"key":"e_1_3_2_1_32_1","volume-title":"Software Engineering: (Update)","author":"Sommerville Ian","unstructured":"Ian Sommerville . 2006. Software Engineering: (Update) ( 8 th Edition) (International Computer Science). Addison-Wesley Longman Publishing Co. , Inc., Boston, MA, USA. Ian Sommerville. 2006. Software Engineering: (Update) (8th Edition) (International Computer Science). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.","edition":"8"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.03.003"},{"key":"e_1_3_2_1_34_1","volume-title":"Stamelos and Panagiotis Sfetsos","author":"Ioannis","year":"2007","unstructured":"Ioannis G. Stamelos and Panagiotis Sfetsos . 2007 . Agile Software Development Quality Assurance. IGI Global, Hershey, PA, USA. Ioannis G. Stamelos and Panagiotis Sfetsos. 2007. Agile Software Development Quality Assurance. IGI Global, Hershey, PA, USA."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2816707.2816710"},{"key":"e_1_3_2_1_36_1","unstructured":"The Coq Development Team. 2015. The Coq proof assistant reference manual. http:\/\/coq.inria.fr Version 8.5.  The Coq Development Team. 2015. The Coq proof assistant reference manual. http:\/\/coq.inria.fr Version 8.5."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"event":{"name":"SBLP 2018: XXII Brazilian Symposium on Programming Languages","location":"Sao Carlos Brazil","acronym":"SBLP 2018"},"container-title":["Proceedings of the XXII Brazilian Symposium on Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3264637.3264649","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3264637.3264649","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:10:54Z","timestamp":1750212654000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3264637.3264649"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,20]]},"references-count":37,"alternative-id":["10.1145\/3264637.3264649","10.1145\/3264637"],"URL":"https:\/\/doi.org\/10.1145\/3264637.3264649","relation":{},"subject":[],"published":{"date-parts":[[2018,9,20]]},"assertion":[{"value":"2018-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}