{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:33:20Z","timestamp":1774838000863,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2011,6,1]],"date-time":"2011-06-01T00:00:00Z","timestamp":1306886400000},"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":["Commun. ACM"],"published-print":{"date-parts":[[2011,6]]},"abstract":"<jats:p>Can a programming language really help programmers write better programs?<\/jats:p>","DOI":"10.1145\/1953122.1953145","type":"journal-article","created":{"date-parts":[[2011,6,6]],"date-time":"2011-06-06T11:51:38Z","timestamp":1307361098000},"page":"81-91","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":126,"title":["Specification and verification"],"prefix":"10.1145","volume":"54","author":[{"given":"Mike","family":"Barnett","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]},{"given":"Manuel","family":"F\u00e4hndrich","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology (ETH), Z\u00fcrich, Switzerland"}]},{"given":"Wolfram","family":"Schulte","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]},{"given":"Herman","family":"Venter","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]}],"member":"320","published-online":{"date-parts":[[2011,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"High-Integrity Software: The SPARK Approach to Safety and Security","author":"Barnes J.","year":"2003","unstructured":"Barnes , J. High-Integrity Software: The SPARK Approach to Safety and Security . Addison-Wesley , 2003 . Barnes, J. High-Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, 2003."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_5_1","first-page":"33","article-title":"A reachability predicate for analyzing low-level software. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems, Volume 4424 LNCS (Braga","volume":"19","author":"Chatterjee S.","year":"2007","unstructured":"Chatterjee , S. , Lahiri , S. K. , Qadeer , S. , and Rakamaric , Z . A reachability predicate for analyzing low-level software. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems, Volume 4424 LNCS (Braga , Portugal, Mar. 24--Apr. 1). Springer , 2007 , 19 -- 33 . Chatterjee, S., Lahiri, S. K., Qadeer, S., and Rakamaric, Z. A reachability predicate for analyzing low-level software. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems, Volume 4424 LNCS (Braga, Portugal, Mar. 24--Apr. 1). Springer, 2007, 19--33.","journal-title":"Portugal, Mar. 24--Apr. 1). Springer"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of Tools and Algorithms for Construction and Analysis of Systems","author":"de Moura L.","unstructured":"de Moura , L. and Bj\u00f8rner , N . Z3: An efficient SMT solver . In Proceedings of Tools and Algorithms for Construction and Analysis of Systems , Volume 4963 LNCS (Budapest, Mar . 29--Apr. 6). Springer , 337--340. de Moura, L. and Bj\u00f8rner, N. Z3: An efficient SMT solver. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems, Volume 4963 LNCS (Budapest, Mar. 29--Apr. 6). Springer, 337--340."},{"key":"e_1_2_1_8_1","volume-title":"Compaq Systems Research Center","author":"Detlefs D. L.","year":"1998","unstructured":"Detlefs , D. L. , Leino , K.R.M. , Nelson , G. , and Saxe , J. B . Extended Static Checking Research Report 159 . Compaq Systems Research Center , Palo Alto, CA , 1998 . Detlefs, D. L., Leino, K.R.M., Nelson, G., and Saxe, J. B. Extended Static Checking Research Report 159. Compaq Systems Research Center, Palo Alto, CA, 1998."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/227726.227772"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949332"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297052"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770379"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592439"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452045"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_20_1","volume-title":"Using the Spec# language, methodology, and tools to write bug-free programs. Advanced Lectures on Software Engineering: LASER Summer School 2007\/2008","author":"Leino K.R.M.","year":"2010","unstructured":"Leino , K.R.M. and M\u00fcller , P . Using the Spec# language, methodology, and tools to write bug-free programs. Advanced Lectures on Software Engineering: LASER Summer School 2007\/2008 , Volume 6029 LNCS. Springer , 2010 . Leino, K.R.M. and M\u00fcller, P. Using the Spec# language, methodology, and tools to write bug-free programs. Advanced Lectures on Software Engineering: LASER Summer School 2007\/2008, Volume 6029 LNCS. Springer, 2010."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767748"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1953122.1953145","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1953122.1953145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:41Z","timestamp":1750244381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1953122.1953145"}},"subtitle":["the Spec# experience"],"short-title":[],"issued":{"date-parts":[[2011,6]]},"references-count":23,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["10.1145\/1953122.1953145"],"URL":"https:\/\/doi.org\/10.1145\/1953122.1953145","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6]]},"assertion":[{"value":"2011-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}