{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:00Z","timestamp":1750309080314,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1981,7,1]],"date-time":"1981-07-01T00:00:00Z","timestamp":362793600000},"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":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[1981,7]]},"DOI":"10.1145\/1010832.1010839","type":"journal-article","created":{"date-parts":[[2004,7,21]],"date-time":"2004-07-21T23:30:10Z","timestamp":1090452610000},"page":"16-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["AFFIRM summary"],"prefix":"10.1145","volume":"6","author":[{"given":"Susan L.","family":"Gerhart","sequence":"first","affiliation":[{"name":"ISI"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[1981,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Bates R. editor Affirm Annotated Transcripts 1981.  Bates R. editor Affirm Annotated Transcripts 1981."},{"key":"e_1_2_1_2_1","unstructured":"Berthomieu B. Proving Progress Properties of Communication Protocols in Affirm USC\/Information Sciences Institute Program Verification Project Affirm Memo 35 September 1980.  Berthomieu B. Proving Progress Properties of Communication Protocols in Affirm USC\/Information Sciences Institute Program Verification Project Affirm Memo 35 September 1980."},{"volume-title":"Affirm Memo","year":"1980","author":"Berthomieu B.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233535"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(74)90009-5"},{"volume-title":"SRI International","year":"1979","author":"Boyer R. S.","key":"e_1_2_1_6_1"},{"volume-title":"Fifth Conference on Automated Deduction","year":"1980","author":"Erickson R. W","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics","author":"Floyd R. W.","year":"1967"},{"key":"e_1_2_1_11_1","unstructured":"Gerhart S. L. and D. S. Wile \"Preliminary report on the Delta experiment: specification and verification of a multiple-user file updating module \" in Proceedings of the Conference on Specification of Reliable Software pp. 198--211 IEEE Computer Society April 1979.  Gerhart S. L. and D. S. Wile \"Preliminary report on the Delta experiment: specification and verification of a multiple-user file updating module \" in Proceedings of the Conference on Specification of Reliable Software pp. 198--211 IEEE Computer Society April 1979."},{"key":"e_1_2_1_12_1","first-page":"343","article-title":"An overview of Affirm: a specification and verification system","volume":"80","author":"Gerhart S. L.","year":"1980","journal-title":"Proceedings IFIP"},{"key":"e_1_2_1_13_1","unstructured":"Gerhart S. L. Experience with the MITRE Toy Security Kernel USC\/Information Sciences Institute Program Verification Project Affirm Memo 2 January 1980.  Gerhart S. L. Experience with the MITRE Toy Security Kernel USC\/Information Sciences Institute Program Verification Project Affirm Memo 2 January 1980."},{"key":"e_1_2_1_14_1","unstructured":"Gerhart S. L. A Short Blurb on Program Specification Featuring a New Example USC\/Information Sciences Institute Program Verification Project Affirm Memo 34 September 1980.  Gerhart S. L. A Short Blurb on Program Specification Featuring a New Example USC\/Information Sciences Institute Program Verification Project Affirm Memo 34 September 1980."},{"key":"e_1_2_1_15_1","unstructured":"Gerhart S. L. Fundamental Concepts of Program Verification USC\/Information Sciences Institute Program Verification Project Affirm Memo 15 February 1980.  Gerhart S. L. Fundamental Concepts of Program Verification USC\/Information Sciences Institute Program Verification Project Affirm Memo 15 February 1980."},{"key":"e_1_2_1_16_1","unstructured":"Gerhart S. L. and S. Lee eds. Affirm User's Guide 1981.  Gerhart S. L. and S. Lee eds. Affirm User's Guide 1981."},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Gerhart S. L. editor Affirm Type Library 1981.  Gerhart S. L. editor Affirm Type Library 1981.","DOI":"10.2307\/1372254"},{"volume-title":"Affirm Memo","year":"1981","author":"Gerhart S. L.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312820"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567757"},{"key":"e_1_2_1_21_1","unstructured":"Good D. \"The Problem with Program Verification is Computing Science \" Software Engineering Notes 5 (3) July 1980.  Good D. \"The Problem with Program Verification is Computing Science \" Software Engineering Notes 5 (3) July 1980."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808473"},{"key":"e_1_2_1_23_1","unstructured":"Guttag J. V. The Specification and Application to Programming of Abstract Data Types Ph.D. thesis University of Toronto Department of Computer Science October 1975.   Guttag J. V. The Specification and Application to Programming of Abstract Data Types Ph.D. thesis University of Toronto Department of Computer Science October 1975."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/359605.359618"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359666"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260922"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"volume-title":"Prentice-Hall","year":"1980","author":"Jones C. L.","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","unstructured":"Lee S. A Numerical Analysis Program Proof in Affirm USC\/Information Sciences Institute Program Verification Project Affirm Memo 31 August 1980.  Lee S. A Numerical Analysis Program Proof in Affirm USC\/Information Sciences Institute Program Verification Project Affirm Memo 31 August 1980."},{"key":"e_1_2_1_30_1","first-page":"40","article-title":"Finding a Design Error in a Distributed System: A Case Study, USC\/Information Sciences Institute, Program Verification Project","author":"Lee S.","year":"1981","journal-title":"Affirm Memo"},{"key":"e_1_2_1_31_1","unstructured":"Levitt K. B. Silverberg and L. Robinson The HDM Handbook 1980. 3 volumes  Levitt K. B. Silverberg and L. Robinson The HDM Handbook 1980. 3 volumes"},{"key":"e_1_2_1_33_1","unstructured":"Loeckx J. Proving Properties of Algorithmic Specifications of Abstract Data Types in Affirm USC\/Information Sciences Institute Program Verification Project Affirm Memo 29 July 1980.  Loeckx J. Proving Properties of Algorithmic Specifications of Abstract Data Types in Affirm USC\/Information Sciences Institute Program Verification Project Affirm Memo 29 July 1980."},{"key":"e_1_2_1_34_1","unstructured":"Lomet D. et al IBM Task Force on Provably Secure Operating Systems 1980.  Lomet D. et al IBM Task Force on Provably Secure Operating Systems 1980."},{"key":"e_1_2_1_35_1","unstructured":"London R. L. \"Program verification \" in P. Wegner (ed.) Research Directions In Software Technology MIT Press 1979.  London R. L. \"Program verification \" in P. Wegner (ed.) Research Directions In Software Technology MIT Press 1979."},{"volume-title":"IFIP","year":"1977","author":"Luckham D. C.","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_40_1","unstructured":"Musser D. R. \"A data type verification system based on rewrite rules \" in Proceedings of the Sixth Texas Conference on Computing Systems pp. 1A22-A1A31 Austin Texas November 1977.  Musser D. R. \"A data type verification system based on rewrite rules \" in Proceedings of the Sixth Texas Conference on Computing Systems pp. 1A22-1A31 Austin Texas November 1977."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567461"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_43_1","unstructured":"Popek G. B. Walker J. Chow G. Thiel and C. Kline LOCUS: A Distributed System Architecture University of California Los Angeles Technical Report 1980.   Popek G. B. Walker J. Chow G. Thiel and C. Kline LOCUS: A Distributed System Architecture University of California Los Angeles Technical Report 1980."},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Schwabe D. Formal Specification and Verification of a Connection Establishment Protocol USC\/Information Sciences Institute ISI\/RR-81-91 March 1981.  Schwabe D. Formal Specification and Verification of a Connection Establishment Protocol USC\/Information Sciences Institute ISI\/RR-81-91 March 1981.","DOI":"10.1145\/800081.802654"},{"key":"e_1_2_1_45_1","unstructured":"Schwabe D. Formal Techniques for Specification and Verification of Protocols Ph.D. thesis University of California Los Angeles Computer Science Department March 1981. (Also UCLA Technical Report ENG 8209)   Schwabe D. Formal Techniques for Specification and Verification of Protocols Ph.D. thesis University of California Los Angeles Computer Science Department March 1981. (Also UCLA Technical Report ENG 8209)"},{"volume-title":"USC\/Information Sciences Institute","year":"1979","author":"Thompson D. H.","key":"e_1_2_1_46_1"},{"volume-title":"USC\/Information Sciences Institute","year":"1981","author":"Thompson D. H.","key":"e_1_2_1_47_1"},{"key":"e_1_2_1_48_1","unstructured":"Thompson D. H. C. A. Sunshine R. W. Erickson S. L. Gerhart and D. Schwabe Specification and Verification of Communication Protocols in Affirm using State Transition Models USC\/Information Sciences Institute ISI\/RR-81-88 February 1981. (Also submitted for publication)  Thompson D. H. C. A. Sunshine R. W. Erickson S. L. Gerhart and D. Schwabe Specification and Verification of Communication Protocols in Affirm using State Transition Models USC\/Information Sciences Institute ISI\/RR-81-88 February 1981. (Also submitted for publication)"},{"volume-title":"USC\/Information Sciences Institute","year":"1981","author":"Thompson D. H.","key":"e_1_2_1_49_1"},{"key":"e_1_2_1_51_1","unstructured":"Wile D. S. POPART: Producer of Parsers and Related Tools 1979. (USC\/Information Sciences Institute Technical Report in preparation.)  Wile D. S. POPART: Producer of Parsers and Related Tools 1979. (USC\/Information Sciences Institute Technical Report in preparation.)"},{"volume-title":"Affirm Memo","year":"1980","author":"Wing J. M.","key":"e_1_2_1_52_1"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233830"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1010832.1010839","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1010832.1010839","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:43:25Z","timestamp":1750286605000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1010832.1010839"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981,7]]},"references-count":46,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1981,7]]}},"alternative-id":["10.1145\/1010832.1010839"],"URL":"https:\/\/doi.org\/10.1145\/1010832.1010839","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[1981,7]]},"assertion":[{"value":"1981-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}