{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,14]],"date-time":"2025-11-14T07:34:56Z","timestamp":1763105696967,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:00:00Z","timestamp":1574035200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NWO\/TTW","award":["14319"],"award-info":[{"award-number":["14319"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,11,18]]},"DOI":"10.1145\/3375258.3375265","type":"proceedings-article","created":{"date-parts":[[2020,3,7]],"date-time":"2020-03-07T12:07:50Z","timestamp":1583582870000},"page":"50-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Is Deductive Program Verification Mature Enough to be Taught to Software Engineers?"],"prefix":"10.1145","author":[{"given":"Marc","family":"Schoolderman","sequence":"first","affiliation":[{"name":"Radboud University, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[{"name":"Open University of the Netherlands, Heerlen, The Netherlands and Radboud University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,3,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0070-y"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/358234.381162"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein Bernard van Gastel Wesley Janssen Tanja Lange Peter Schwabe and Sjaak Smetsers . TweetNaCl: A crypto library in 100 tweets. In Diego Aranha and Alfred Menezes editors Progress in Cryptology - LATINCRYPT 2014 volume 8895 of Lecture Notes in Computer Science pages 64 -- 83 . Springer-Verlag Berlin Heidelberg 2015. Daniel J. Bernstein Bernard van Gastel Wesley Janssen Tanja Lange Peter Schwabe and Sjaak Smetsers. TweetNaCl: A crypto library in 100 tweets. In Diego Aranha and Alfred Menezes editors Progress in Cryptology - LATINCRYPT 2014 volume 8895 of Lecture Notes in Computer Science pages 64--83. Springer-Verlag Berlin Heidelberg 2015.","DOI":"10.1007\/978-3-319-16295-9_4"},{"key":"e_1_3_2_1_5_1","unstructured":"Francois Bobot. MPRI lecture 2-36-1. http:\/\/francois.bobot.eu\/mpri2018\/ 2018. Francois Bobot. MPRI lecture 2-36-1. http:\/\/francois.bobot.eu\/mpri2018\/ 2018."},{"key":"e_1_3_2_1_6_1","unstructured":"Sebastian B\u00f6hne and Christoph Kreitz . Learning how to prove: From the coq proof assistant to textbook style. In Pedro Quaresma and Walther Neuper editors Proceedings 6th International Workshop on Theorem proving components for Educational software ThEdu@CADE 2017 Gothenburg Sweden 6 Aug 2017. volume 267 of EPTCS pages 1 -- 18 2017. Sebastian B\u00f6hne and Christoph Kreitz. Learning how to prove: From the coq proof assistant to textbook style. In Pedro Quaresma and Walther Neuper editors Proceedings 6th International Workshop on Theorem proving components for Educational software ThEdu@CADE 2017 Gothenburg Sweden 6 Aug 2017. volume 267 of EPTCS pages 1--18 2017."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2143"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933419"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich . Why3 --- where programs meet provers. In Matthias Felleisen and Philippa Gardner editors Proceedings of the 22nd European Symposium on Programming volume 7792 of Lecture Notes in Computer Science pages 125 -- 128 . Springer March 2013 . Jean-Christophe Filli\u00e2tre and Andrei Paskevich. Why3 --- where programs meet provers. In Matthias Felleisen and Philippa Gardner editors Proceedings of the 22nd European Symposium on Programming volume 7792 of Lecture Notes in Computer Science pages 125--128. Springer March 2013.","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_12_1","first-page":"2018","article-title":"Deductive program verification with why3: A tutorial. UniGR Summer School on Verification Technology","author":"Filli\u00e2tre Jean-Christophe","year":"2018","journal-title":"Systems & Applications"},{"key":"e_1_3_2_1_13_1","first-page":"35","article-title":"Teaching logic using a state-of-the-art proof assistant","volume":"3","author":"Hendriks Maxim","year":"2010","journal-title":"Acta Didactica Napocensia"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1564\/tme_v25.2.03","article-title":"Using automated reasoning tools in geogebra in the teaching and learning of proving in geometry","volume":"25","author":"Kov\u00e1cs Zolt\u00e1n","year":"2018","journal-title":"International Journal for Technology in Mathematics Education"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.15388\/infedu.2010.07"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1984.10017"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01966091"},{"volume-title":"Inc.","year":"1992","author":"Nielson Hanne Riis","key":"e_1_3_2_1_19_1"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and Gerwin Klein. Concrete Semantics - With Isabelle\/HOL. Springer International Publishing 2014. Tobias Nipkow and Gerwin Klein. Concrete Semantics - With Isabelle\/HOL. Springer International Publishing 2014.","DOI":"10.1007\/978-3-319-10542-0"},{"key":"e_1_3_2_1_21_1","first-page":"748","volume-title":"Automated Deduction---CADE-11","author":"Owre S.","year":"1992"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411260.1411264"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04912-5_7"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSEET.2016.28"},{"key":"e_1_3_2_1_25_1","unstructured":"Ed Schouten. CloudABI cloud computing meets fine-grained capabilites. https:\/\/www.bsdcan.org\/2015\/schedule\/track\/Security\/524.en.html 2015. Ed Schouten. CloudABI cloud computing meets fine-grained capabilites. https:\/\/www.bsdcan.org\/2015\/schedule\/track\/Security\/524.en.html 2015."},{"key":"e_1_3_2_1_26_1","unstructured":"Wolfgang Schreiner . Theorem and algorithm checking for courses on logic and formal methods. In Pedro Quaresma and Walther Neuper editors Proceedings 7th International Workshop on Theorem proving components for Educational software THedu@FLoC 2018 Oxford United Kingdom 18 july 2018. volume 290 of EPTCS pages 56 -- 75 2018. Wolfgang Schreiner. Theorem and algorithm checking for courses on logic and formal methods. In Pedro Quaresma and Walther Neuper editors Proceedings 7th International Workshop on Theorem proving components for Educational software THedu@FLoC 2018 Oxford United Kingdom 18 july 2018. volume 290 of EPTCS pages 56--75 2018."}],"event":{"name":"CSERC '19: The 8th Computer Science Education Research Conference","sponsor":["University of Cyprus"],"location":"Larnaca Cyprus","acronym":"CSERC '19"},"container-title":["Proceedings of the 8th Computer Science Education Research Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3375258.3375265","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3375258.3375265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:48Z","timestamp":1750199568000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3375258.3375265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,18]]},"references-count":25,"alternative-id":["10.1145\/3375258.3375265","10.1145\/3375258"],"URL":"https:\/\/doi.org\/10.1145\/3375258.3375265","relation":{},"subject":[],"published":{"date-parts":[[2019,11,18]]},"assertion":[{"value":"2020-03-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}