{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:26Z","timestamp":1776305246984,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"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,7]]},"abstract":"<jats:p>SLAM is a program-analysis engine used to check if clients of an API follow the API's stateful usage rules.<\/jats:p>","DOI":"10.1145\/1965724.1965743","type":"journal-article","created":{"date-parts":[[2011,6,28]],"date-time":"2011-06-28T17:31:10Z","timestamp":1309282270000},"page":"68-76","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":141,"title":["A decade of software model checking with SLAM"],"prefix":"10.1145","volume":"54","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Levin","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, WA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[{"name":"Microsoft Research India, Bangalore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1251535.1251543"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057391"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.759192"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672077"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380932"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_19"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/776816.776863"},{"key":"e_1_2_1_14_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"Clarke , E. , Grumberg , O. , and Peled , D . Model Checking . MIT Press , Cambridge, MA , 1999 . Clarke, E., Grumberg, O., and Peled, D. Model Checking. MIT Press, Cambridge, MA, 1999."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_22_1","first-page":"340","article-title":"Z3: an efficient SMT solver. In Proceedings of the 14  th  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Mar. 29--Apr. 6)","volume":"337","author":"de Moura L.","year":"2008","unstructured":"de Moura , L. and Bj\u00f8rner , N . Z3: an efficient SMT solver. In Proceedings of the 14 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Mar. 29--Apr. 6) . Springer , 2008 , 337 -- 340 . de Moura, L. and Bj\u00f8rner, N. Z3: an efficient SMT solver. In Proceedings of the 14 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Mar. 29--Apr. 6). Springer, 2008, 337--340.","journal-title":"Springer"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_24_1","first-page":"16","article-title":"Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operating System Design and Implementation (San Diego, Oct. 23--25)","volume":"1","author":"Engler D.","year":"2000","unstructured":"Engler , D. , Chelf , B. , Chou , A. , and Hallem , S . Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operating System Design and Implementation (San Diego, Oct. 23--25) . Usenix Association , 2000 , 1 -- 16 . Engler, D., Chelf, B., Chou, A., and Hallem, S. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operating System Design and Implementation (San Diego, Oct. 23--25). Usenix Association, 2000, 1--16.","journal-title":"Usenix Association"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.760734"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Network and Distributed System Security Symposium","author":"Godefroid P.","year":"2008","unstructured":"Godefroid , P. , Levin , O.Y. , and Molnar , D.A . Automated whitebox fuzz testing . In Proceedings of the Network and Distributed System Security Symposium ( San Diego, CA, Feb. 10--13). The Internet society , 2008 . Godefroid, P., Levin, O.Y., and Molnar, D.A. Automated whitebox fuzz testing. In Proceedings of the Network and Distributed System Security Symposium (San Diego, CA, Feb. 10--13). The Internet society, 2008."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the Ninth International Conference on Computer-Aided Verification (Haifa, June 22--25)","author":"Graf S.","unstructured":"Graf , S. and Sa\u00efdi , H . Construction of abstract state graphs with PVS . In Proceedings of the Ninth International Conference on Computer-Aided Verification (Haifa, June 22--25) . Springer, 72--83. Graf, S. and Sa\u00efdi, H. Construction of abstract state graphs with PVS. In Proceedings of the Ninth International Conference on Computer-Aided Verification (Haifa, June 22--25). Springer, 72--83."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672083"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.013"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/194184"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542500"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2004.1293079"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/530225"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_43_1","first-page":"233","article-title":"Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, N.D. Jones and S.S. Muchnick, eds","volume":"189","author":"Sharir M.","year":"1981","unstructured":"Sharir , M. and Pnueli , A . Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, N.D. Jones and S.S. Muchnick, eds . Prentice-Hall , 1981 , 189 -- 233 . Sharir, M. and Pnueli, A. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, N.D. Jones and S.S. Muchnick, eds. Prentice-Hall, 1981, 189--233.","journal-title":"Prentice-Hall"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the Symposium Logic in Computer","author":"Vardi M.Y.","year":"1986","unstructured":"Vardi , M.Y. and Wolper , P . An automata theoretic approach to automatic program verification . In Proceedings of the Symposium Logic in Computer Science (Cambridge, MA , June 16--18). IEEE Computer Society Press , 1986 , 332--344. Vardi, M.Y. and Wolper, P. An automata theoretic approach to automatic program verification. In Proceedings of the Symposium Logic in Computer Science (Cambridge, MA, June 16--18). IEEE Computer Society Press, 1986, 332--344."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1965724.1965743","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1965724.1965743","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:22:25Z","timestamp":1750245745000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1965724.1965743"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":42,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["10.1145\/1965724.1965743"],"URL":"https:\/\/doi.org\/10.1145\/1965724.1965743","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7]]},"assertion":[{"value":"2011-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}