{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:28:03Z","timestamp":1750307283981,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,11,7]],"date-time":"2010-11-07T00:00:00Z","timestamp":1289088000000},"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,11,7]]},"DOI":"10.1145\/1882362.1882424","type":"proceedings-article","created":{"date-parts":[[2010,11,12]],"date-time":"2010-11-12T14:38:38Z","timestamp":1289572718000},"page":"299-302","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Writing and using program specifications"],"prefix":"10.1145","author":[{"given":"Steven P.","family":"Reiss","sequence":"first","affiliation":[{"name":"Brown University, Providence, RI, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Godmar Back and Dawson Engler \"MJ - a system for constructing bug-finding analyses for Java \" Stanford University Computer Systems Laboratory (2003). Godmar Back and Dawson Engler \"MJ - a system for constructing bug-finding analyses for Java \" Stanford University Computer Systems Laboratory (2003)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_3_1","first-page":"2004","article-title":"The spec# programming language: an overview","author":"Barnett Mike","year":"2004","journal-title":"CASSIS"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806860"},{"key":"e_1_3_2_1_6_1","unstructured":"Edmund M. Clarke Jr. Orna Grumberg and Doron A. Peled Model Checking The MIT Press (1999). Edmund M. Clarke Jr. Orna Grumberg and Doron A. Peled Model Checking The MIT Press (1999)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.411.0140"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810319"},{"key":"e_1_3_2_1_10_1","first-page":"01","article-title":"Model driven architecture (MDA)","volume":"2001","author":"Object Management Group","year":"2001","journal-title":"Document ormsc\/"},{"key":"e_1_3_2_1_11_1","unstructured":"Yuri Gurevich Benjamin Rossman and Wolfram Shulte \"Semantic Essence of AsmL \" Microsoft Research Technical Report MSR-TR-2004-27 (2004). Yuri Gurevich Benjamin Rossman and Wolfram Shulte \"Semantic Essence of AsmL \" Microsoft Research Technical Report MSR-TR-2004-27 (2004)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.231756"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1145735.1145737"},{"key":"e_1_3_2_1_14_1","first-page":"216","volume-title":"5th and 6th SPIN Workshop, Lecture Notes in Computer Science","volume":"1680","author":"Havelund Klaus","year":"1999"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/362452.362489"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806125"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_1_22_1","unstructured":"Sun Microsystems ADL Design Specification Version 0.1 Sun Microsystems (1993). Sun Microsystems ADL Design Specification Version 0.1 Sun Microsystems (1993)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101908.1101917"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070525"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806672.1806675"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.58"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Ehud Y. Shapiro Algorithmic Program Debugging MIT Press (1983). Ehud Y. Shapiro Algorithmic Program Debugging MIT Press (1983).","DOI":"10.7551\/mitpress\/1192.001.0001"},{"key":"e_1_3_2_1_28_1","first-page":"46","volume-title":"4th Intl. Software Architecture Workshop","author":"Shaw Mary","year":"2000"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/356596.356598"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/222132.222148"},{"key":"e_1_3_2_1_31_1","unstructured":"J. B. Wordsworth Software Development with Z Addison-Wesley (1992). J. B. Wordsworth Software Development with Z Addison-Wesley (1992)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321659"}],"event":{"name":"SIGSOFT\/FSE'10: 18th ACM SIGSOFT Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Santa Fe New Mexico USA","acronym":"SIGSOFT\/FSE'10"},"container-title":["Proceedings of the FSE\/SDP workshop on Future of software engineering research"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1882362.1882424","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1882362.1882424","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:34Z","timestamp":1750244374000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1882362.1882424"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11,7]]},"references-count":32,"alternative-id":["10.1145\/1882362.1882424","10.1145\/1882362"],"URL":"https:\/\/doi.org\/10.1145\/1882362.1882424","relation":{},"subject":[],"published":{"date-parts":[[2010,11,7]]},"assertion":[{"value":"2010-11-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}