{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,25]],"date-time":"2023-10-25T09:11:34Z","timestamp":1698225094132},"reference-count":20,"publisher":"Wiley","issue":"4","license":[{"start":{"date-parts":[[2006,10,30]],"date-time":"2006-10-30T00:00:00Z","timestamp":1162166400000},"content-version":"vor","delay-in-days":5081,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Softw. Maint: Res. Pract."],"published-print":{"date-parts":[[1992,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The application of formal verification in software engineering is limited because programs continue to evolve during the maintenance phase, thus rendering the original verification obsolete. Program decomposition schemes can be used to identify the parts of the modified program that need verification. The original program verification can be reused and combined with the verification of the parts of the modified program. Automatic decomposition of programs into independent computational threads called projections can be performed by utilizing program\u2010dependence relations. These relations represent dependence information among the variables and statements of a program. The individual proofs of each projection can be combined to produce the verification of the entire program. After a modification, many of the original projections may still be present in the new program and they are not re\u2010verified. Only new projections need verification which is usually easier than re\u2010verifying the entire program.<\/jats:p>","DOI":"10.1002\/smr.4360040403","type":"journal-article","created":{"date-parts":[[2006,11,17]],"date-time":"2006-11-17T15:43:54Z","timestamp":1163778234000},"page":"183-198","source":"Crossref","is-referenced-by-count":1,"title":["Application of automatic decomposition schemes in proof maintenance for evolving programs"],"prefix":"10.1002","volume":"4","author":[{"given":"R.","family":"Gopal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. R.","family":"Schach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2006,10,30]]},"reference":[{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2363.2366"},{"key":"e_1_2_1_4_1","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","year":"1976"},{"key":"e_1_2_1_5_1","first-page":"19","volume-title":"Proceedings of Symposium on Applied Mathematics","author":"Floyd R. W.","year":"1967"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_7_1","unstructured":"Gopal R.(1989) \u2018On supporting software evolution\u2014automatic decomposition schemes based on static and dynamic analysis of programs\u2019 Ph.D. dissertation Department of Computer Science Vanderbilt University Nashville TN."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.1989.65204"},{"key":"e_1_2_1_9_1","first-page":"35","volume-title":"Proceedings of the SIGPLAN '88 Conference on Programming Languages Design and Implementation","author":"Horwitz S.","year":"1988"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/65979.65980"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.232210"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1986.233414"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1109\/ICSM.1988.10172","volume-title":"\u2018Using program decomposition to guide modifications\u2019, in Proceedings of Conference on Software Maintenance\u20141988","author":"Lyle J. R.","year":"1988"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/360569.360659"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.234206"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Ottenstein K. J.andOttenstein L. M.(1984) \u2018The program dependence graph in a software development environment\u2019 inProceedings of the ACM SIGPLANISIGSOFT Symposium on Practical Programming Development Environments May 1984 Pittsburgh PA;","DOI":"10.1145\/800020.808263"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1145\/390011.808263","volume":"19","journal-title":"ACM SIGPLAN Notices"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48021"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.86782"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/358557.358577"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"}],"container-title":["Journal of Software Maintenance: Research and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fsmr.4360040403","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/smr.4360040403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T07:55:35Z","timestamp":1698134135000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/smr.4360040403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,12]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1992,12]]}},"alternative-id":["10.1002\/smr.4360040403"],"URL":"https:\/\/doi.org\/10.1002\/smr.4360040403","archive":["Portico"],"relation":{},"ISSN":["1040-550X","1096-908X"],"issn-type":[{"value":"1040-550X","type":"print"},{"value":"1096-908X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,12]]}}}