{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T20:39:11Z","timestamp":1791146351985,"version":"4.1.0"},"reference-count":12,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"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":[[2010,2]]},"abstract":"<jats:p>A translator framework enables the use of model checking in complex avionics systems and other industrial settings.<\/jats:p>","DOI":"10.1145\/1646353.1646372","type":"journal-article","created":{"date-parts":[[2010,1,26]],"date-time":"2010-01-26T14:01:38Z","timestamp":1264514498000},"page":"58-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":120,"title":["Software model checking takes off"],"prefix":"10.1145","volume":"53","author":[{"given":"Steven P.","family":"Miller","sequence":"first","affiliation":[{"name":"Rockwell Collins, Cedar Rapids, IA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"University of Minnesota Software Engineering Center, Minneapolis, MN"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Darren D.","family":"Cofer","sequence":"additional","affiliation":[{"name":"Rockwell Collins, Cedar Rapids, IA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Model Checking","author":"Clarke E.","year":"2001","unstructured":"Clarke , E. , Grumberg , O. and Peled , D . Model Checking . The MIT Press , Cambridge, MA , 2001 . Clarke, E., Grumberg, O. and Peled, D. Model Checking. The MIT Press, Cambridge, MA, 2001."},{"key":"e_1_2_1_2_1","unstructured":"Esterel Technologies. SCADE Suite Product Description; http:\/\/www.estereltechnolgies.com\/  Esterel Technologies. SCADE Suite Product Description; http:\/\/www.estereltechnolgies.com\/"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_2_1_4_1","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann G.","year":"2003","unstructured":"Holzmann , G. The SPIN Model Checker: Primer and Reference Manual . Addison-Wesley Professional , 2003 . Holzmann, G. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003."},{"key":"e_1_2_1_5_1","unstructured":"IRST. The NuSMV Model Checker; http:\/\/nusmv.irst.itc.it\/  IRST. The NuSMV Model Checker; http:\/\/nusmv.irst.itc.it\/"},{"key":"e_1_2_1_6_1","unstructured":"The Mathworks Simulink Product Description; http:\/\/www.mathworks.com\/  The Mathworks Simulink Product Description; http:\/\/www.mathworks.com\/"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2005-6431"},{"key":"e_1_2_1_8_1","volume-title":"International Journal on Software Tools for Technology Transfer (Feb.","author":"Miller S.","year":"2006","unstructured":"Miller , S. , Tribble , A. , Whalen , M. and Heimdahl , M.P.E . Proving the Shalls . International Journal on Software Tools for Technology Transfer (Feb. 2006 ). Miller, S., Tribble, A., Whalen, M. and Heimdahl, M.P.E. Proving the Shalls. International Journal on Software Tools for Technology Transfer (Feb. 2006)."},{"key":"e_1_2_1_9_1","unstructured":"Prover Technology. Prover Plug-In Product Description; http:\/\/www.prover.com\/  Prover Technology. Prover Plug-In Product Description; http:\/\/www.prover.com\/"},{"key":"e_1_2_1_10_1","unstructured":"Reactive Systems Inc.; http:\/\/www.reactive-systems.com\/  Reactive Systems Inc.; http:\/\/www.reactive-systems.com\/"},{"key":"e_1_2_1_11_1","unstructured":"SRI International. Symbolic Analysis Laboratory; http:\/\/sal.csl.sri.com\/  SRI International. Symbolic Analysis Laboratory; http:\/\/sal.csl.sri.com\/"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems","author":"Whalen M.","year":"2007","unstructured":"Whalen , M. , Cofer , D. , Miller , S. Krogh , B. , and Storm , W . Integration of formal analysis into a model-based software development process . In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems ( Berlin, Germany, July 1--2 , 2007 ). Whalen, M., Cofer, D., Miller, S. Krogh, B., and Storm, W. Integration of formal analysis into a model-based software development process. In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (Berlin, Germany, July 1--2, 2007)."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1646353.1646372","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1646353.1646372","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:40:56Z","timestamp":1750250456000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1646353.1646372"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2]]},"references-count":12,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["10.1145\/1646353.1646372"],"URL":"https:\/\/doi.org\/10.1145\/1646353.1646372","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2]]},"assertion":[{"value":"2010-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}