{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:53Z","timestamp":1750308233402,"version":"3.41.0"},"reference-count":11,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1985,8,1]],"date-time":"1985-08-01T00:00:00Z","timestamp":491702400000},"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":[[1985,8]]},"abstract":"<jats:p>This paper describes methods for decomposing large conjectures into smaller ones in order to make their proof easier and for limiting the amount of reproving that occurs when a specification is modified. It proposes a tool, based on these methods, for managing the proofs of conjectures about an evolving specification.<\/jats:p>","DOI":"10.1145\/1012497.1012505","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:39:09Z","timestamp":1097170749000},"page":"19-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["An Ina Jo\u00ae proof manager for the formal development method"],"prefix":"10.1145","volume":"10","author":[{"given":"Daniel M.","family":"Berry","sequence":"first","affiliation":[{"name":"University of California Los Angeles, CA"}]}],"member":"320","published-online":{"date-parts":[[1985,8]]},"reference":[{"key":"e_1_2_1_2_1","volume-title":"Department of Defense","author":"Ada Language Reference Manual A, U.S.","year":"1983","unstructured":"{ADA83} \" Ada Language Reference Manual ,\" MIL-STD-1815 A, U.S. Department of Defense ( 1983 ).]] {ADA83} \"Ada Language Reference Manual,\" MIL-STD-1815A, U.S. Department of Defense (1983).]]"},{"key":"e_1_2_1_3_1","volume-title":"]]","author":"Berry D. M.","year":"1982","unstructured":"{Bry82} Berry , D. M. , \" The Application of the Formal Development Methodology to Data Base Design and Integrity Verification ,\" Proceedings of Fourth Israel Conference on Software Quality Assurance ( 1982 ). ]] {Bry82} Berry, D. M., \"The Application of the Formal Development Methodology to Data Base Design and Integrity Verification,\" Proceedings of Fourth Israel Conference on Software Quality Assurance (1982).]]"},{"key":"e_1_2_1_4_1","volume-title":"]]","author":"Feldman S. I.","year":"1978","unstructured":"{Fel78} Feldman , S. I. , \"Make --- A Program for Maintaining Computer Programs ,\" Technical Report , Bell Laboratories , Murray Hill , NJ ( 1978 ). ]] {Fel78} Feldman, S. I., \"Make --- A Program for Maintaining Computer Programs,\" Technical Report, Bell Laboratories, Murray Hill, NJ (1978).]]"},{"key":"e_1_2_1_5_1","volume-title":"Problems, Perspectives, and Opportunities,\" ISI\/RR-78-71","author":"Gerhart S. L.","year":"1978","unstructured":"{Ger78} Gerhart , S. L. , \" Program Verification in the 1980s : Problems, Perspectives, and Opportunities,\" ISI\/RR-78-71 , USC Information Sciences Institute , Marina Del Rey, CA ( August , 1978 ).]] {Ger78} Gerhart, S. L., \"Program Verification in the 1980s: Problems, Perspectives, and Opportunities,\" ISI\/RR-78-71, USC Information Sciences Institute, Marina Del Rey, CA (August, 1978).]]"},{"key":"e_1_2_1_7_1","volume-title":"The Ina Jo Reference Manual,\" TM-(L)-6021\/001\/000","author":"Locasso R.","year":"1980","unstructured":"{LSSE80} Locasso , R. , Scheid , J., Schorre , D. V. , and Eggert , P. R. , \" The Ina Jo Reference Manual,\" TM-(L)-6021\/001\/000 , System Development Corporation , Santa Monica, CA ( June 27, 1980 ).]] {LSSE80} Locasso, R., Scheid, J., Schorre, D. V., and Eggert, P. R., \"The Ina Jo Reference Manual,\" TM-(L)-6021\/001\/000, System Development Corporation, Santa Monica, CA (June 27, 1980).]]"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"{Mor79} Moriconi M. S. \"A Designer\/Verifier's Assistant \" IEEE Transactions on Software EngineeringSE-5(4) pp. 387--401 (July 1979).]]  {Mor79} Moriconi M. S. \"A Designer\/Verifier's Assistant \" IEEE Transactions on Software EngineeringSE-5(4) pp. 387--401 (July 1979).]]","DOI":"10.1109\/TSE.1979.234206"},{"key":"e_1_2_1_11_1","volume-title":"Petrocelli\/Charter","author":"Myers G. J.","year":"1975","unstructured":"{Mye75} Myers , G. J. , Reliable Software through Composite Design , Petrocelli\/Charter , New York , NY ( 1975 ).]] {Mye75} Myers, G. J., Reliable Software through Composite Design, Petrocelli\/Charter, New York, NY (1975).]]"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_2_1_14_1","volume-title":"Private Communication,\" USC ISI","author":"Smallberg D. A.","year":"1980","unstructured":"{PC80} Smallberg , D. A. and London , R , \" Private Communication,\" USC ISI ( 1980 ).]] {PC80} Smallberg, D. A. and London, R, \"Private Communication,\" USC ISI (1980).]]"},{"key":"e_1_2_1_15_1","volume-title":"Revision Control System","author":"Tichy W.","year":"1981","unstructured":"{Tic81} Tichy , W. , Revision Control System , Purdue University , Lafayette, IN ( 1981 ).]] {Tic81} Tichy, W., Revision Control System, Purdue University, Lafayette, IN (1981).]]"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1012497.1012505","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1012497.1012505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:42Z","timestamp":1750264302000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1012497.1012505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,8]]},"references-count":11,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1985,8]]}},"alternative-id":["10.1145\/1012497.1012505"],"URL":"https:\/\/doi.org\/10.1145\/1012497.1012505","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[1985,8]]},"assertion":[{"value":"1985-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}