{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T07:18:35Z","timestamp":1775027915298,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"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":[[2014,2]]},"abstract":"<jats:p>Redundant software (and hardware) ensured Curiosity reached its destination and functioned as its designers intended.<\/jats:p>","DOI":"10.1145\/2560217.2560218","type":"journal-article","created":{"date-parts":[[2014,1,28]],"date-time":"2014-01-28T13:49:22Z","timestamp":1390916962000},"page":"64-73","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Mars code"],"prefix":"10.1145","volume":"57","author":[{"given":"Gerard J.","family":"Holzmann","sequence":"first","affiliation":[{"name":"California Institute of Technology, Pasadena, CA"}]}],"member":"320","published-online":{"date-parts":[[2014,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"TR 2005-001","author":"Chalin P.","year":"2005"},{"key":"e_1_2_1_2_1","volume-title":"Distributed Algorithms, LNCS","author":"Detlefs D.L.","year":"2000"},{"key":"e_1_2_1_3_1","volume-title":"Wellington","author":"Doherty S.","year":"2004"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007945"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 2002 Aerospace Conference (Big Sky, MT, Mar. 9--16)","author":"Gluck P.R.","year":"2002"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.940728"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2003.1203056"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-010-0136-x"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.212"},{"key":"e_1_2_1_10_1","volume-title":"Addison-Wesley","author":"Holzmann G.J.","year":"2004"},{"key":"e_1_2_1_11_1","first-page":"91","volume":"76","author":"Holzmann G.J.","year":"2004","journal-title":"Berlin"},{"key":"e_1_2_1_12_1","first-page":"2","volume":"5","author":"Holzmann G.J.","year":"2000","journal-title":"Bell Labs Technical Journal"},{"key":"e_1_2_1_13_1","unstructured":"Jet Propulsion Laboratory. JPL Coding Standard for Flight Software; http:\/\/lars-lab.jpl.nasa.gov\/JPL_Coding_Standard_C.pdf  Jet Propulsion Laboratory. JPL Coding Standard for Flight Software ; http:\/\/lars-lab.jpl.nasa.gov\/JPL_Coding_Standard_C.pdf"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2006.14"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_11"},{"key":"e_1_2_1_16_1","unstructured":"Motor Industry Software Reliability Association. MISRA-C Guidelines for the Use of the C Language in Critical Systems. MIRA Ltd. Warwickshire U.K. 2012; http:\/\/www.misra-c.com\/  Motor Industry Software Reliability Association. MISRA-C Guidelines for the Use of the C Language in Critical Systems . MIRA Ltd. Warwickshire U.K. 2012; http:\/\/www.misra-c.com\/"},{"key":"e_1_2_1_17_1","unstructured":"NASA. NASA Engineering and Safety Center Technical Assessment Report. National Highway Traffic Safety Administration (NHTSA) Toyota Unintended Acceleration Investigation Appendix A: Software Washington D.C. Jan. 18 2011; http:\/\/www.nhtsa.gov\/staticfiles\/nvs\/pdf\/NASA_FR_Appendix_A_Software.pdf  NASA. NASA Engineering and Safety Center Technical Assessment Report . National Highway Traffic Safety Administration (NHTSA) Toyota Unintended Acceleration Investigation Appendix A: Software Washington D.C. Jan. 18 2011; http:\/\/www.nhtsa.gov\/staticfiles\/nvs\/pdf\/NASA_FR_Appendix_A_Software.pdf"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the International Conference on Space Mission Challenges for Information Technology","author":"Ong E.C.","year":"2003"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_20_1","author":"Redberg R.","year":"2013","journal-title":"Review. LaRS Report, Jet Propulsion Laboratory, Pasadena, CA"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645536.657319"},{"key":"e_1_2_1_22_1","unstructured":"SRI International Computer Science Laboratory. The PVS Specification and Verification System; http:\/\/pvs.csl.sri.com\/  SRI International Computer Science Laboratory. The PVS Specification and Verification System ; http:\/\/pvs.csl.sri.com\/"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the First IEEE Symposium on Logic in Computer Science","author":"Vardi M.","year":"1986"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2560217.2560218","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2560217.2560218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:21Z","timestamp":1750234221000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2560217.2560218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2560217.2560218"],"URL":"https:\/\/doi.org\/10.1145\/2560217.2560218","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2014-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}