{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:44:57Z","timestamp":1772163897444,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T00:00:00Z","timestamp":1131840000000},"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":[[2005,11,13]]},"DOI":"10.1145\/1103846.1103855","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T10:52:40Z","timestamp":1139223160000},"page":"57-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The affordable application of formal methods to software engineering"],"prefix":"10.1145","author":[{"given":"James F.","family":"Davis","sequence":"first","affiliation":[{"name":"University of Maryland University College, Adelphia, MD"}]}],"member":"320","published-online":{"date-parts":[[2005,11,13]]},"reference":[{"key":"e_1_3_2_1_1_1","volume":"20","author":"Amey P.","unstructured":"Amey , P. (2002, March ). Correctness by Construction: Better can also be cheaper. Crosstalk Magazine. Retrieved 20 April 2005, from http:\/\/www.praxis-his.com\/pdfs\/c_by_c_better_cheaper.pdf.]] Amey, P. (2002, March). Correctness by Construction: Better can also be cheaper. Crosstalk Magazine. Retrieved 20 April 2005, from http:\/\/www.praxis-his.com\/pdfs\/c_by_c_better_cheaper.pdf.]]","journal-title":"Crosstalk Magazine. Retrieved"},{"key":"e_1_3_2_1_2_1","volume-title":"Correctness by Construction: A TSP-Friendly Approach to Ultra-Low Defect Software. Retrieved","author":"Chapman R.","year":"2004","unstructured":"Chapman , R. ( 2004 ). Correctness by Construction: A TSP-Friendly Approach to Ultra-Low Defect Software. Retrieved 20 April 2005, from http:\/\/www.sei.cmu.edu\/tsp\/tug-2004-presentations\/chapman.pdf.]] Chapman, R. (2004). Correctness by Construction: A TSP-Friendly Approach to Ultra-Low Defect Software. Retrieved 20 April 2005, from http:\/\/www.sei.cmu.edu\/tsp\/tug-2004-presentations\/chapman.pdf.]]"},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the SIGADA Conference, 14-18 November.]]","author":"Chapman R.","year":"2004","unstructured":"Chapman , R. ( 2004 , November). SPARK, an Intensive Overview . Proceedings of the SIGADA Conference, 14-18 November.]] Chapman, R. (2004, November). SPARK, an Intensive Overview. Proceedings of the SIGADA Conference, 14-18 November.]]"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.976937"},{"key":"e_1_3_2_1_5_1","volume-title":"2nd National Software Summit","author":"Chen J.","year":"2005","unstructured":"Chen , J. (2004, May ). The Enterprise: Unwired . 2nd National Software Summit , Reston, VA . Retrieved 20 April 2005 , from http:\/\/www.cnsoftware.org\/nss2report\/Chen-NSS2v.3.pdf.]] Chen, J. (2004, May). The Enterprise: Unwired. 2nd National Software Summit, Reston, VA. Retrieved 20 April 2005, from http:\/\/www.cnsoftware.org\/nss2report\/Chen-NSS2v.3.pdf.]]"},{"key":"e_1_3_2_1_6_1","unstructured":"\"Formal Methods.\" (n.d.). Retrieved 20 April 2005 from http:\/\/en.wikipedia.org\/wiki\/Formal_methods.]]  \"Formal Methods.\" (n.d.). Retrieved 20 April 2005 from http:\/\/en.wikipedia.org\/wiki\/Formal_methods.]]"},{"key":"e_1_3_2_1_7_1","volume-title":"High Confidence Software & Systems Conference, March. Retrieved","author":"Hoare T.","year":"2004","unstructured":"Hoare , T. ( 2004 , August). The Verifying Compiler: a Grand Challenge for Computing Research . High Confidence Software & Systems Conference, March. Retrieved 20 April 2005, from http:\/\/research.microsoft.com\/~thoare\/The_Verifying_Compiler.ppt.]] Hoare, T. (2004, August). The Verifying Compiler: a Grand Challenge for Computing Research. High Confidence Software & Systems Conference, March. Retrieved 20 April 2005, from http:\/\/research.microsoft.com\/~thoare\/The_Verifying_Compiler.ppt.]]"},{"key":"e_1_3_2_1_8_1","volume-title":"Correctness by Construction: An Introduction to SPARK Ada. Retrieved","author":"Knight J.C.","year":"2004","unstructured":"Knight , J.C. ( 2004 ). Correctness by Construction: An Introduction to SPARK Ada. Retrieved 20 April 2005, from http:\/\/www.cs.virginia.edu\/~jck\/cs651\/slides\/14.correctness.by.construction.pdf.]] Knight, J.C. (2004). Correctness by Construction: An Introduction to SPARK Ada. Retrieved 20 April 2005, from http:\/\/www.cs.virginia.edu\/~jck\/cs651\/slides\/14.correctness.by.construction.pdf.]]"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the Center for National Software Studies Workshop on Trustworthy Software, 8-9 April. Retrieved","author":"Michael J.B.","year":"2004","unstructured":"Michael , J.B. , Voas , J.M. , & Linger , R.C. ( 2004 , May) . Proceedings of the Center for National Software Studies Workshop on Trustworthy Software, 8-9 April. Retrieved 20 April 2005, from http:\/\/www.cnsoftware.org\/nss2report\/NSS2FinalReport04-29-05PDF.pdf.]] Michael, J.B., Voas, J.M., & Linger, R.C. (2004, May). Proceedings of the Center for National Software Studies Workshop on Trustworthy Software, 8-9 April. Retrieved 20 April 2005, from http:\/\/www.cnsoftware.org\/nss2report\/NSS2FinalReport04-29-05PDF.pdf.]]"},{"key":"e_1_3_2_1_10_1","volume-title":"et. al. (2003). The Spread of the Sapphire\/Slammer Worm. Retrieved","author":"Moore D.","year":"2005","unstructured":"Moore , D. , Paxson , V. , Savage , S. , et. al. (2003). The Spread of the Sapphire\/Slammer Worm. Retrieved 20 April 2005 , from http:\/\/www.cs.berkeley.edu\/~nweaver\/sapphire\/.]] Moore, D., Paxson, V., Savage, S., et. al. (2003). The Spread of the Sapphire\/Slammer Worm. Retrieved 20 April 2005, from http:\/\/www.cs.berkeley.edu\/~nweaver\/sapphire\/.]]"},{"key":"e_1_3_2_1_11_1","volume-title":"An Analysis of the Patriot Missile System. Retrieved","author":"Morgan T.","year":"2002","unstructured":"Morgan , T. & Roberts , J. ( 2002 ). An Analysis of the Patriot Missile System. Retrieved 20 April 2005, from http:\/\/seeri.etsu.edu\/SECodeCases\/ethicsC\/PatriotMissile.htm.]] Morgan, T. & Roberts, J. (2002). An Analysis of the Patriot Missile System. Retrieved 20 April 2005, from http:\/\/seeri.etsu.edu\/SECodeCases\/ethicsC\/PatriotMissile.htm.]]"},{"key":"e_1_3_2_1_12_1","volume-title":"Case Study: MULTOS Certification Authority. Retrieved","author":"Praxis High Integrity Systems","year":"2005","unstructured":"Praxis High Integrity Systems . (n.d.). Case Study: MULTOS Certification Authority. Retrieved 20 April 2005 , from http:\/\/www.praxis his.com\/services\/software\/casestudy.asp.]] Praxis High Integrity Systems. (n.d.). Case Study: MULTOS Certification Authority. Retrieved 20 April 2005, from http:\/\/www.praxis his.com\/services\/software\/casestudy.asp.]]"},{"key":"e_1_3_2_1_13_1","volume-title":"Correctness by Construction Approach. Retrieved","author":"Praxis High Integrity Systems","year":"2005","unstructured":"Praxis High Integrity Systems . (n.d.). Correctness by Construction Approach. Retrieved 20 April 2005 , from http:\/\/www.praxis-his.com\/services\/software\/approach.asp.]] Praxis High Integrity Systems. (n.d.). Correctness by Construction Approach. Retrieved 20 April 2005, from http:\/\/www.praxis-his.com\/services\/software\/approach.asp.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"Correctness by Construction Principles. Retrieved","author":"Praxis High Integrity Systems","year":"2005","unstructured":"Praxis High Integrity Systems . (n.d.). Correctness by Construction Principles. Retrieved 20 April 2005 , from http:\/\/www.praxis-his.com\/services\/software\/principles.asp.]] Praxis High Integrity Systems. (n.d.). Correctness by Construction Principles. Retrieved 20 April 2005, from http:\/\/www.praxis-his.com\/services\/software\/principles.asp.]]"},{"key":"e_1_3_2_1_15_1","volume-title":"Do we have a creeping crisis and are we losing our edge? 2nd National Software Summit","author":"Wulf W.A.","year":"2005","unstructured":"Wulf , W.A. (2004, May ). Do we have a creeping crisis and are we losing our edge? 2nd National Software Summit , Reston, VA . Retrieved 20 April 2005 , from http:\/\/www.cnsoftware.org\/nss2report\/Wulf%20Luncheon%20Presentation.pdf.]] Wulf, W.A. (2004, May). Do we have a creeping crisis and are we losing our edge? 2nd National Software Summit, Reston, VA. Retrieved 20 April 2005, from http:\/\/www.cnsoftware.org\/nss2report\/Wulf%20Luncheon%20Presentation.pdf.]]"},{"key":"e_1_3_2_1_16_1","volume-title":"Software failure cited in August blackout investigation. ComputerWorld. Retrieved","author":"Verton D.","year":"2004","unstructured":"Verton , D. (2003, November ). Software failure cited in August blackout investigation. ComputerWorld. Retrieved 20 April 2004 , from http:\/\/www.computerworld.com\/securitytopics\/security\/recovery\/story\/0,10801,87400,00.html.]] Verton, D. (2003, November). Software failure cited in August blackout investigation. ComputerWorld. Retrieved 20 April 2004, from http:\/\/www.computerworld.com\/securitytopics\/security\/recovery\/story\/0,10801,87400,00.html.]]"},{"key":"e_1_3_2_1_17_1","volume-title":"A Review of Formal Methods. Retrieved","author":"Vienneau R.","year":"2005","unstructured":"Vienneau , R. (1993, May ). A Review of Formal Methods. Retrieved 20 April 2005 , from http:\/\/www.dacs.dtic.mil\/techs\/fmreview\/definition.html]] Vienneau, R. (1993, May). A Review of Formal Methods. Retrieved 20 April 2005, from http:\/\/www.dacs.dtic.mil\/techs\/fmreview\/definition.html]]"}],"event":{"name":"SIGAda '05: ACM SIGAda Annual International Conference","location":"Atlanta GA USA","acronym":"SIGAda '05","sponsor":["ACM Association for Computing Machinery","SIGAda ACM Special Interest Group on Ada Programming Language","SIGAPP ACM Special Interest Group on Applied Computing","SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering","SIGCAS ACM Special Interest Group on Computers and Society","SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2005 annual ACM SIGAda international conference on Ada: The Engineering of Correct and Reliable Software for Real-Time & Distributed Systems using Ada and Related Technologies"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1103846.1103855","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1103846.1103855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:48:54Z","timestamp":1750272534000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1103846.1103855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11,13]]},"references-count":17,"alternative-id":["10.1145\/1103846.1103855","10.1145\/1103846"],"URL":"https:\/\/doi.org\/10.1145\/1103846.1103855","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1104011.1103855","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,11,13]]},"assertion":[{"value":"2005-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}