{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:43:30Z","timestamp":1725497010026},"edition-number":"1","reference-count":24,"publisher":"Wiley","isbn-type":[{"type":"print","value":"9780471383932"},{"type":"electronic","value":"9780470050118"}],"license":[{"start":{"date-parts":[[2008,4,15]],"date-time":"2008-04-15T00:00:00Z","timestamp":1208217600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/doi.wiley.com\/10.1002\/tdm_license_1.1"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Using formal program verification, it is possible to prove mathematically and mechanically that software behaves correctly as specified. For verification to scale up to software built from components, components must have formal specifications and the verification process must be modular. Unlike testing that can only reveal the presence of errors, formal varification can guarantee correctness.<\/jats:p>","DOI":"10.1002\/9780470050118.ecse331","type":"other","created":{"date-parts":[[2008,4,10]],"date-time":"2008-04-10T16:47:05Z","timestamp":1207846025000},"page":"1-10","source":"Crossref","is-referenced-by-count":1,"title":["Formal Program Verification"],"prefix":"10.1002","author":[{"given":"Heather K.","family":"Harton","sequence":"first","affiliation":[]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[]},{"given":"Joan","family":"Krone","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2008,4,15]]},"reference":[{"key":"e_1_2_9_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_9_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_9_4_1","unstructured":"J.Bloch http:\/\/googleresearch.blogspot.com\/2006\/06\/extra\u2010extra\u2010readall\u2010about\u2010it\u2010nearly.html 2006."},{"key":"e_1_2_9_5_1","article-title":"Technical Note 2000\u2013002, Compaq Systems Research Center","author":"Leino K. R .M.","year":"2000","journal-title":"ESC\/Java User's Manual"},{"key":"e_1_2_9_6_1","doi-asserted-by":"crossref","unstructured":"B.Hackett R.Rugina Region\u2010based shape analysis with tracked locations Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'05) Long Beach CA 2005.","DOI":"10.1145\/1040305.1040331"},{"key":"e_1_2_9_7_1","unstructured":"G.Kulczycki M.Sitaraman W. F.Ogden B. W.Weide Clean Semantics for Calls with Repeated Arguments Technical ReportRSRG\u201005\u201001 Department of Computer Science Clemson University Clemson SC2005."},{"key":"e_1_2_9_8_1","unstructured":"The Isabelle Theorem Proving Environment Developed by Larry Paulson at Cambridge University and Tobias Nipkow at TU Mumich. Available:http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabell."},{"key":"e_1_2_9_9_1","doi-asserted-by":"crossref","unstructured":"G. T.Leavens J.Abrial D.Batory M.Butler A.Coglio K.Fisler E.Hehner C.Jones D.Miller S.Peyton\u2010Jgnes M.Sitaraman D. R.Smith A.Stump Roadmap for enhanced lnguages and methods to aid verification Proceedings of the 5th international Conference on Generative Programming and Component Engineer 2006. GPCE \u203206.New York:ACM Press 2006 PP.221\u2013236.","DOI":"10.1145\/1173706.1173740"},{"key":"e_1_2_9_10_1","unstructured":"J.Krone. The role of verification in software reusability Ph.D. Thesis Columbus OH: The Ohio State University 1988."},{"key":"e_1_2_9_11_1","unstructured":"W.Heym Computer program verification: improvements for human reasoning Ph.D. Thesis Columbus OH: The Ohio State University 1995."},{"key":"e_1_2_9_12_1","doi-asserted-by":"crossref","unstructured":"M.Sitaraman S.Atkinson G.Kulczycki B.Weide T. J.Long P.Bucci W.Heym S.Pike J. E.Hollingsworth Reasoning about software\u2010component behavior Proceedings of the 6th International Conf. on Software Reuse.Berlin:Springer\u2010Verlag 2000 pp.266\u2013283.","DOI":"10.1007\/978-3-540-44995-9_16"},{"volume-title":"Systematic Software Development using VDM","year":"1990","author":"Jones C. B.","key":"e_1_2_9_13_1"},{"key":"e_1_2_9_14_1","unstructured":"A.A.Koptelov A.K.Petrenko VDM vs. programming language extensions or their integration Proceedings of the First International Overture Workshop Newcastle 2005."},{"key":"e_1_2_9_15_1","doi-asserted-by":"crossref","unstructured":"S.Owre J. M.Rushby N.Shankar PVS: A prototype verification system Proceedings of the 11th International Conference on Automated Deduction 1992 pp.748\u2013752.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_2_9_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_2_9_17_1","unstructured":"J.Filli\u00e2tre C.March\u00e9 The Why\/Krakatoa\/Caduceus platform for deductive program verification inW.DammandH.Hermanns(eds.) 19th International Conference on Computer Aided Verification Lecture Notes in Computer science Berlin Germany 2007."},{"volume-title":"Model Checking","year":"2000","author":"Clarke W. M.","key":"e_1_2_9_18_1"},{"key":"e_1_2_9_19_1","doi-asserted-by":"crossref","unstructured":"W.Visser K.Havelund G.Brat S.Park Model checking programs IEEE International Conference on Automated Software Engineering 2000.","DOI":"10.1109\/ASE.2000.873645"},{"key":"e_1_2_9_20_1","doi-asserted-by":"crossref","unstructured":"T.Ball R.Majumdar T.Millstein S. K.Rajamani Automatic predicate abstraction of C programs Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation(Snowbird Utah United States). PLDI '01.New York:ACM Press 2001 pp.203\u2013213.","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_9_21_1","doi-asserted-by":"crossref","unstructured":"D.Leinenbach W.Paul E.Petrova Towards the formal verification of a C0 compiler: code generation and implementation correctness Software Engineering and Formal Methods 2005. SEFM 2005. Third IEEE International Conference on 2005.","DOI":"10.1109\/SEFM.2005.51"},{"volume-title":"Foundation of component\u2010Based Systems","year":"2000","author":"Muller P.","key":"e_1_2_9_22_1"},{"key":"e_1_2_9_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_9_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_9_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"}],"container-title":["Wiley Encyclopedia of Computer Science and Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/9780470050118.ecse331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,24]],"date-time":"2024-02-24T19:54:50Z","timestamp":1708804490000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/9780470050118.ecse331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,4,15]]},"ISBN":["9780471383932","9780470050118"],"references-count":24,"alternative-id":["10.1002\/9780470050118.ecse331","10.1002\/9780470050118"],"URL":"https:\/\/doi.org\/10.1002\/9780470050118.ecse331","archive":["Portico"],"relation":{},"subject":[],"published":{"date-parts":[[2008,4,15]]}}}