{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:33:29Z","timestamp":1750221209392,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,16]],"date-time":"2018-07-16T00:00:00Z","timestamp":1531699200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NWO","award":["639.023.710"],"award-info":[{"award-number":["639.023.710"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,16]]},"DOI":"10.1145\/3236454.3236479","type":"proceedings-article","created":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T18:39:17Z","timestamp":1546972757000},"page":"40-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["An exercise in verifying sequential programs with VerCors"],"prefix":"10.1145","author":[{"given":"Sebastiaan J. C.","family":"Joosten","sequence":"first","affiliation":[{"name":"University of Twente, The Netherlands"}]},{"given":"Wytse","family":"Oortwijn","sequence":"additional","affiliation":[{"name":"University of Twente, The Netherlands"}]},{"given":"Mohsen","family":"Safari","sequence":"additional","affiliation":[{"name":"University of Twente, The Netherlands"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[{"name":"University of Twente, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2018,7,16]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Lecture Notes in Computer Science","volume-title":"Deductive Software Verification - The KeY Book","author":"Ahrendt Wolfgang","unstructured":"Wolfgang Ahrendt , Bernhard Beckert , Richard Bubel , Reiner H\u00e4hnle , Peter H. Schmitt , and Mattias Ulbrich . 2016. Deductive Software Verification - The KeY Book . Lecture Notes in Computer Science , Vol. 10001 . Springer International Publishing . Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, Peter H. Schmitt, and Mattias Ulbrich. 2016. Deductive Software Verification - The KeY Book. Lecture Notes in Computer Science, Vol. 10001. Springer International Publishing."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"A. Amighi S. Blom and M. Huisman. 2014. Resource Protection Using Atomics - Patterns and Verification. In APLAS. 255--274.  A. Amighi S. Blom and M. Huisman. 2014. Resource Protection Using Atomics - Patterns and Verification. In APLAS. 255--274.","DOI":"10.1007\/978-3-319-12736-1_14"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"A. Amighi S. Blom and M. Huisman. 2016. VerCors: A Layered Approach to Practical Verification of Concurrent Software. In PDP. 495--503.  A. Amighi S. Blom and M. Huisman. 2016. VerCors: A Layered Approach to Practical Verification of Concurrent Software. In PDP. 495--503.","DOI":"10.1109\/PDP.2016.107"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"A. Amighi C. Haack M. Huisman and C. Hurlin. 2015. Permission-based separation logic for multithreaded Java programs. LMCS 11 1 (2015).  A. Amighi C. Haack M. Huisman and C. Hurlin. 2015. Permission-based separation logic for multithreaded Java programs. LMCS 11 1 (2015).","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"e_1_3_2_1_5_1","volume-title":"Verification of Shared-Reading Synchronisers. In 1st International Workshop on Methods and Tools for Rigorous System Design","author":"Amighi Afshin","year":"2018","unstructured":"Afshin Amighi , Marieke Huisman , Stefan Blom , Saddek Bensalem , and Simon Bliudze . 2018 . Verification of Shared-Reading Synchronisers. In 1st International Workshop on Methods and Tools for Rigorous System Design 2018. Afshin Amighi, Marieke Huisman, Stefan Blom, Saddek Bensalem, and Simon Bliudze. 2018. Verification of Shared-Reading Synchronisers. In 1st International Workshop on Methods and Tools for Rigorous System Design 2018."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"S. Blom S. Darabi M. Huisman and W. Oortwijn. 2017. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In iFM (LNCS) Vol. 10510. Springer 102--110.  S. Blom S. Darabi M. Huisman and W. Oortwijn. 2017. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In iFM (LNCS) Vol. 10510. Springer 102--110.","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0308-3"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0396-8"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"B. Jacobs J. Smans P. Philippaerts F. Vogels W. Penninckx and F. Piessens. 2011. VeriFast: A powerful sound predictable fast verifier for C and Java. In NFM.   B. Jacobs J. Smans P. Philippaerts F. Vogels W. Penninckx and F. Piessens. 2011. VeriFast: A powerful sound predictable fast verifier for C and Java. In NFM.","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_1_12_1","first-page":"191","article-title":"An Abstraction Technique for Describing Concurrent Program Behaviour","volume":"10712","author":"Oortwijn W.","year":"2017","unstructured":"W. Oortwijn , S. Blom , D. Gurov , M. Huisman , and M. Zaharieva-Stojanovski . 2017 . An Abstraction Technique for Describing Concurrent Program Behaviour . In VSTTE (LNCS) , Vol. 10712. 191 -- 209 . W. Oortwijn, S. Blom, D. Gurov, M. Huisman, and M. Zaharieva-Stojanovski. 2017. An Abstraction Technique for Describing Concurrent Program Behaviour. In VSTTE (LNCS), Vol. 10712. 191--209.","journal-title":"VSTTE (LNCS)"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_53"}],"event":{"name":"ISSTA '18: International Symposium on Software Testing and Analysis","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Amsterdam Netherlands","acronym":"ISSTA '18"},"container-title":["Companion Proceedings for the ISSTA\/ECOOP 2018 Workshops"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236454.3236479","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236454.3236479","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:39Z","timestamp":1750210779000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236454.3236479"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,16]]},"references-count":13,"alternative-id":["10.1145\/3236454.3236479","10.1145\/3236454"],"URL":"https:\/\/doi.org\/10.1145\/3236454.3236479","relation":{},"subject":[],"published":{"date-parts":[[2018,7,16]]},"assertion":[{"value":"2018-07-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}