{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:48:42Z","timestamp":1725749322104},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405600"},{"type":"electronic","value":"9783642405617"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40561-7_14","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T13:10:29Z","timestamp":1379509829000},"page":"197-211","source":"Crossref","is-referenced-by-count":2,"title":["Static Detection of Implementation Errors Using Formal Code Specification"],"prefix":"10.1007","author":[{"given":"Iman","family":"Saleh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregory","family":"Kulczycki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. Brian","family":"Blake","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Marciniak, J.J.: Encyclopedia of Software Engineering, 2nd edn. Wiley Interscience (2001)"},{"issue":"9","key":"14_CR2","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"J.M. Wing","year":"1990","unstructured":"Wing, J.M.: A Specifier\u2019s Introduction to Formal Methods. Computer\u00a023(9), 8\u201322 (1990)","journal-title":"Computer"},{"key":"14_CR3","volume-title":"Wiley Encyclopedia of Computer Science and Engineering, B","author":"H.K. Harton","year":"2008","unstructured":"Harton, H.K., Sitaraman, M., Krone, J.: Formal Program Verification. In: Wah, B.W. (ed.) Wiley Encyclopedia of Computer Science and Engineering. John Wiley & Sons, Inc., Hoboken (2008)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"14_CR5","unstructured":"Voas, J.M., McGraw, G.: Software Fault Injection: Inoculating Programs Against Errors. John Wiley & Sons (1998)"},{"key":"14_CR6","series-title":"IFIP","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-0-387-39388-9_27","volume-title":"Software Engineering Techniques: Design for Quality","author":"A. Derezi\u0144ska","year":"2006","unstructured":"Derezi\u0144ska, A.: Advanced Mutation Operators Applicable in C# Programs. In: Sacha, K. (ed.) Software Engineering Techniques: Design for Quality. IFIP, vol.\u00a0227, pp. 283\u2013288. Springer, Boston (2006)"},{"issue":"5","key":"14_CR7","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y. Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An Analysis and Survey of the Development of Mutation Testing. IEEE Transactions on Software Engineering\u00a037(5), 649\u2013678 (2011)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR8","unstructured":"Saleh, I.: Spec# Mutation Testing DataSet (2013), \n                    \n                      http:\/\/filebox.vt.edu\/users\/imostafa\/DataSets\/FormalSpecification\/"},{"key":"14_CR9","unstructured":"Wah, B.W.: Wiley Encyclopedia of Computer Science and Engineering, 1st edn. Wiley-Interscience (2009)"},{"issue":"10","key":"14_CR10","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"14_CR11","unstructured":"Leino, K.R.M., Monahan, R.: Automatic Verification of Textbook Programs that Use Comprehensions. Presented at the ECOOP Workshop, Berlin, Germany (2007)"},{"key":"14_CR12","unstructured":"Dijkstra, E.W., Feijen, W.H.J., Sterringa, J.: A Method of Programming, 1st English Edn. Addison-Wesley (1988)"},{"key":"14_CR13","unstructured":"Tukey, J.W.: Exploratory Data Analysis, 1st edn. Addison Wesley (1977)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-13010-6_4","volume-title":"Advanced Lectures on Software Engineering","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., M\u00fcller, P.: Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. In: M\u00fcller, P. (ed.) LASER Summer School 2007\/2008. LNCS, vol.\u00a06029, pp. 91\u2013139. Springer, Heidelberg (2010)"},{"key":"14_CR15","unstructured":"DeMillo, R.A., Guindi, D.S., McCracken, W.M., Offutt, A.J., King, K.N.: An extended overview of the Mothra software testing environment. Presented at the Proceedings of the Second Workshop on Software Testing, Verification, and Analysis, pp. 142\u2013151 (1988)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Derezinska, A., Szustek, A.: Tool-Supported Advanced Mutation Approach for Verification of C# Programs, Los Alamitos, CA, USA, pp. 261\u2013268 (2008)","DOI":"10.1109\/DepCoS-RELCOMEX.2008.51"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Derezinska, A.: Quality Assessment of Mutation Operators Dedicated for C# Programs. Presented at the Sixth International Conference on Quality Software, QSIC 2006, pp. 227\u2013234 (2006)","DOI":"10.1109\/QSIC.2006.51"},{"key":"14_CR18","unstructured":"Jones, C.B.: Software Development: A Rigorous Approach, 1st edn. Prentice Hall (1980)"},{"key":"14_CR19","unstructured":"Sufrin, B., Morgan, C., Sorensen, I., Hayes, I.: Notes for a Z handbook: Part 1-The mathematical language, Oxford University, Computing Laboratory, Programming Research Group (1984)"},{"key":"14_CR20","unstructured":"Meyer, B.: Eiffel: The Language. Prentice Hall (1992)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Hackett, B., Das, M., Wang, D., Yang, Z.: Modular checking for buffer overflows in the large, New York, NY, USA, pp. 232\u2013241 (2006)","DOI":"10.1145\/1134285.1134319"},{"issue":"1-3","key":"14_CR22","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the Design of JML Accommodates both Runtime Assertion Checking and Formal Verification. Science of Computer Programming\u00a055(1-3), 185\u2013208 (2005)","journal-title":"Science of Computer Programming"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, 1st edn. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting eSC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., Muller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing\u00a019, 159\u2013189 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24841-5_1","volume-title":"Reliable Software Technologies - Ada-Europe 2004","author":"M. Gogolla","year":"2004","unstructured":"Gogolla, M.: Benefits and Problems of Formal Methods. In: Llamos\u00ed, A., Strohmeier, A. (eds.) Ada-Europe 2004. LNCS, vol.\u00a03063, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Saleh, I., Kulczycki, G., Blake, M.B.: Formal Specification and Verification of Data-Centric Service Composition. In: IEEE International Conference on Web Services, ICWS 2010, pp. 131\u2013138 (2010)","DOI":"10.1109\/ICWS.2010.80"},{"issue":"5","key":"14_CR28","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/MIC.2009.106","volume":"13","author":"I. Saleh","year":"2009","unstructured":"Saleh, I., Kulczycki, G., Blake, M.B.: Demystifying Data-Centric Web Services. IEEE Internet Computing\u00a013(5), 86\u201390 (2009)","journal-title":"IEEE Internet Computing"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Saleh, I., Kulczycki, G., Blake, M.B., Wei, Y.: Formal Methods for Data-Centric Web Services: From Model to Implementation. In: IEEE International Conference on Web Services, ICWS 2013, pp. 332\u2013339 (2013)","DOI":"10.1109\/ICWS.2013.52"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40561-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:55:30Z","timestamp":1558317330000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40561-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405600","9783642405617"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40561-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}