{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T05:57:42Z","timestamp":1725688662377},"reference-count":141,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2009,10]]},"abstract":"Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.<\/jats:p>","DOI":"10.1145\/1592434.1592436","type":"journal-article","created":{"date-parts":[[2009,10,8]],"date-time":"2009-10-08T17:31:08Z","timestamp":1255023068000},"page":"1-36","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":426,"title":["Formal methods"],"prefix":"10.1145","volume":"41","author":[{"given":"Jim","family":"Woodcock","sequence":"first","affiliation":[{"name":"University of York, Heslington, York, UK"}]},{"given":"Peter Gorm","family":"Larsen","sequence":"additional","affiliation":[{"name":"Engineering College of Aarhus, Aarhus, Denmark"}]},{"given":"Juan","family":"Bicarregui","sequence":"additional","affiliation":[{"name":"STFC Rutherford Appleton Laboratory, Oxfordshire, UK"}]},{"given":"John","family":"Fitzgerald","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle, UK"}]}],"member":"320","published-online":{"date-parts":[[2009,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_2_1_2_1","first-page":"619","article-title":"Formal methods: Theory becoming practice","volume":"13","author":"Abrial J.-R.","year":"2007","unstructured":"Abrial , J.-R. 2007 . Formal methods: Theory becoming practice . JUCS 13 , 5, 619 -- 628 . Abrial, J.-R. 2007. Formal methods: Theory becoming practice. JUCS 13, 5, 619--628.","journal-title":"JUCS"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the IFIP 12th World Computer Congress","author":"Allen R. B.","year":"1992","unstructured":"Allen , R. B. and Garlan , D . 1992. A formal approach to software architectures. In Algorithms, Software, Architecture\u2014Information Processing '92, Volume 1 , Proceedings of the IFIP 12th World Computer Congress , Madrid, Spain, 7- -11 Sep. 1992 , J. van Leeuwen, Ed. IFIP Transactions, vol. A-12. North-Holland, Amsterdam, 134--141. Allen, R. B. and Garlan, D. 1992. A formal approach to software architectures. In Algorithms, Software, Architecture\u2014Information Processing '92, Volume 1, Proceedings of the IFIP 12th World Computer Congress, Madrid, Spain, 7--11 Sep. 1992, J. van Leeuwen, Ed. IFIP Transactions, vol. A-12. North-Holland, Amsterdam, 134--141."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_2"},{"key":"e_1_2_1_6_1","unstructured":"Austin S. and Parkin G. 1993. Formal methods: A survey. Tech. rep. National Physical Laboratory Teddington Middlesex UK. Mar. Austin S. and Parkin G. 1993. Formal methods: A survey. Tech. rep. National Physical Laboratory Teddington Middlesex UK. Mar."},{"key":"e_1_2_1_7_1","volume-title":"Course: Practical decision procedures. www.andrew.cmu.edu\/user\/avigad\/practical\/. Cited","author":"Avigad J.","year":"2007","unstructured":"Avigad , J. 2007 . Course: Practical decision procedures. www.andrew.cmu.edu\/user\/avigad\/practical\/. Cited 9 Mar. 2009. Avigad, J. 2007. Course: Practical decision procedures. www.andrew.cmu.edu\/user\/avigad\/practical\/. Cited 9 Mar. 2009."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69073-3_21"},{"key":"e_1_2_1_9_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop","author":"Back R.-J.","unstructured":"Back , R.-J. and von Wright , J. 1990. Refinement calculus, Part I: Sequential nondeterministic programs . In Proceedings of the Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop . Lecture Notes in Computer Science , vol. 430 . Springer-Verlag , Berlin, Heidelberg , Germany, 42--66. Back, R.-J. and von Wright, J. 1990. Refinement calculus, Part I: Sequential nondeterministic programs. In Proceedings of the Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop. Lecture Notes in Computer Science, vol. 430. Springer-Verlag, Berlin, Heidelberg, Germany, 42--66."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_20"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Balser M. Reif W. Schellhorn G. Stenzel K. and Thums A. 2000. Formal system development with KIV. In Proceedings of the 3rd International Conference on Fundamental Approaches to Software Engineering FASE 2000 (Held as Part of the European Joint Conferences on the Theory and Practice of Software ETAPS 2000). Lecture Notes in Computer Science vol. 1783. Springer-Verlag Berlin Heidelberg Germany 363--366. Balser M. Reif W. Schellhorn G. Stenzel K. and Thums A. 2000. Formal system development with KIV. In Proceedings of the 3rd International Conference on Fundamental Approaches to Software Engineering FASE 2000 (Held as Part of the European Joint Conferences on the Theory and Practice of Software ETAPS 2000). Lecture Notes in Computer Science vol. 1783. Springer-Verlag Berlin Heidelberg Germany 363--366.","DOI":"10.1007\/3-540-46428-X_25"},{"key":"e_1_2_1_13_1","volume-title":"High Integrity Ada: The SPARK Approach to Safety and Security","author":"Barnes J.","unstructured":"Barnes , J. 2003. High Integrity Ada: The SPARK Approach to Safety and Security . Addison-Wesley , Reading, MA . Barnes, J. 2003. High Integrity Ada: The SPARK Approach to Safety and Security. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 1st International Symposium on Secure Software Engineering. IEEE Computer Society Press","author":"Barnes J.","unstructured":"Barnes , J. , Chapman , R. , Johnson , R. , Widmaier , J. , Cooper , D. , and Everett , B . 2006. Engineering the Tokeneer enclave protection system . In Proceedings of the 1st International Symposium on Secure Software Engineering. IEEE Computer Society Press , Los Alamitos, CA. Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., and Everett, B. 2006. Engineering the Tokeneer enclave protection system. In Proceedings of the 1st International Symposium on Secure Software Engineering. IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_15_1","first-page":"737","article-title":"Satisfiability modulo theories. In Handbook of Satisfiability, IOS Press, Amsterdam, The Netherlands","volume":"12","author":"Barrett C.","year":"2008","unstructured":"Barrett , C. , Sebastiani , R. , Seshia , S. A. , and Tinelli , C. 2008 . Satisfiability modulo theories. In Handbook of Satisfiability, IOS Press, Amsterdam, The Netherlands , Chapter 12 , 737 -- 797 . Barrett, C., Sebastiani, R., Seshia, S. A., and Tinelli, C. 2008. Satisfiability modulo theories. In Handbook of Satisfiability, IOS Press, Amsterdam, The Netherlands, Chapter 12, 737--797.","journal-title":"Chapter"},{"key":"e_1_2_1_16_1","volume-title":"Formal methods applied to a floating-point number system. Technical Monograph PRG-58","author":"Barrett G.","unstructured":"Barrett , G. 1987. Formal methods applied to a floating-point number system. Technical Monograph PRG-58 , Oxford University Computing Laboratory , Oxford Univ . Barrett, G. 1987. Formal methods applied to a floating-point number system. Technical Monograph PRG-58, Oxford University Computing Laboratory, Oxford Univ."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.24710"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 1st Conference of the North American Transputer Users Group, IOS","author":"Barrett G.","year":"1990","unstructured":"Barrett , G. 1990 . Verifying the Transputer. In Transputer Research and Applications , Proceedings of the 1st Conference of the North American Transputer Users Group, IOS , Amsterdam, The Netherlands, 17--24. Barrett, G. 1990. Verifying the Transputer. In Transputer Research and Applications, Proceedings of the 1st Conference of the North American Transputer Users Group, IOS, Amsterdam, The Netherlands, 17--24."},{"key":"e_1_2_1_19_1","volume-title":"-M","author":"Behm P.","year":"1999","unstructured":"Behm , P. , Benoit , P. , Faivre , A. , and Meynadier , J . -M . 1999 . M\u00e9t\u00e9or : A successful application of B in a large project. In World Congress on Formal Methods. Lecture Notes in Computer Science, vol. 1708 . Springer-Verlag , Berlin, Heidelberg, Germany, 369--387. Behm, P., Benoit, P., Faivre, A., and Meynadier, J.-M. 1999. M\u00e9t\u00e9or: A successful application of B in a large project. In World Congress on Formal Methods. Lecture Notes in Computer Science, vol. 1708. Springer-Verlag, Berlin, Heidelberg, Germany, 369--387."},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Formal Methods for Industrial Critical Systems","author":"Berry G.","unstructured":"Berry , G. 2008. Synchronous design and verification of critical embedded systems using SCADE and Esterel . In Proceedings of the Formal Methods for Industrial Critical Systems . Lecture Notes in Computer Science , vol. 4916 . Springer-Verlag , Berlin, Heidelberg Germany. Berry, G. 2008. Synchronous design and verification of critical embedded systems using SCADE and Esterel. In Proceedings of the Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, vol. 4916. Springer-Verlag, Berlin, Heidelberg Germany."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0079-4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_23_1","volume-title":"Tech. Rep. D\/167\/6101, Adelard","author":"Bloomfield R.","year":"1999","unstructured":"Bloomfield , R. and Craigen , D . 1999 . Formal methods diffusion: Past lessons and future prospects. Tech. Rep. D\/167\/6101, Adelard , Coborn House, 3 Coborn Road, London, UK. Dec . Bloomfield, R. and Craigen, D. 1999. Formal methods diffusion: Past lessons and future prospects. Tech. Rep. D\/167\/6101, Adelard, Coborn House, 3 Coborn Road, London, UK. Dec."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. and St\u00e4rk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag Berlin Heidelberg Germany. B\u00f6rger E. and St\u00e4rk R. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag Berlin Heidelberg Germany.","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1993.0025"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.35"},{"key":"e_1_2_1_28_1","first-page":"212","article-title":"An overview of JML tools and applications. Softw. Tools. tech","volume":"7","author":"Burdy L.","year":"2005","unstructured":"Burdy , L. , Cheon , Y. , Cok , D. R. , Ernst , M. D. , Kiniry , J. R. , Leavens , G. T. , Leino , K. R. M. , and Poll , E. 2005 . An overview of JML tools and applications. Softw. Tools. tech . Trans. 7 , 3, 212 -- 232 . Burdy, L., Cheon, Y., Cok, D. R., Ernst, M. D., Kiniry, J. R., Leavens, G. T., Leino, K. R. M., and Poll, E. 2005. An overview of JML tools and applications. Softw. Tools. tech. Trans. 7, 3, 212--232.","journal-title":"Trans."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/3065491.3065651"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1049\/ic:19970929"},{"key":"e_1_2_1_32_1","volume-title":"The CADE ATP system competition: The world championship for 1st order automated theorem proving. www.cs.miami.edu\/~tptp\/CASC\/. Cited","year":"2009","unstructured":"CADE. 2009. The CADE ATP system competition: The world championship for 1st order automated theorem proving. www.cs.miami.edu\/~tptp\/CASC\/. Cited 9 Mar. 2009 . CADE. 2009. The CADE ATP system competition: The world championship for 1st order automated theorem proving. www.cs.miami.edu\/~tptp\/CASC\/. Cited 9 Mar. 2009."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_18"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_16"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_27"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127900"},{"key":"e_1_2_1_40_1","unstructured":"Craigen D. Gerhart S. and Ralston T. 1993a. An International Survey of Industrial Applications of Formal Methods. Vol. 1 Purpose Approach Analysis and Conclusions. U.S. Department of Commerce Technology Administration National Institute of Standards and Technology Computer Systems Laboratory Gaithersburg MD. Craigen D. Gerhart S. and Ralston T. 1993a. An International Survey of Industrial Applications of Formal Methods. Vol. 1 Purpose Approach Analysis and Conclusions. U.S. Department of Commerce Technology Administration National Institute of Standards and Technology Computer Systems Laboratory Gaithersburg MD."},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Craigen D. Gerhart S. and Ralston T. 1993b. An International Survey of Industrial Applications of Formal Methods. Vol. 2 Case Studies. U.S. Department of Commerce Technology Administration National Institute of Standards and Technology Computer Systems Laboratory Gaithersburg MD. Craigen D. Gerhart S. and Ralston T. 1993b. An International Survey of Industrial Applications of Formal Methods. Vol. 2 Case Studies. U.S. Department of Commerce Technology Administration National Institute of Standards and Technology Computer Systems Laboratory Gaithersburg MD.","DOI":"10.1016\/B978-0-8155-1362-9.50005-6"},{"key":"e_1_2_1_42_1","first-page":"12","article-title":"Teach formal methods","volume":"19","author":"Cuadrado J.","year":"1994","unstructured":"Cuadrado , J. 1994 . Teach formal methods . Byte 19 , 12 (Dec.), 292. Cuadrado, J. 1994. Teach formal methods. Byte 19, 12 (Dec.), 292.","journal-title":"Byte"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_44_1","volume-title":"Computer Science bibliography. www.informatik.uni-trier.de\/~ley\/db\/. Cited","year":"2009","unstructured":"DBLP. 2009. Computer Science bibliography. www.informatik.uni-trier.de\/~ley\/db\/. Cited 9 Mar. 2009 . DBLP. 2009. Computer Science bibliography. www.informatik.uni-trier.de\/~ley\/db\/. Cited 9 Mar. 2009."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090200076"},{"key":"e_1_2_1_46_1","volume-title":"www.deploy-project.eu. Cited","author":"Deploy","year":"2009","unstructured":"Deploy . 2009. www.deploy-project.eu. Cited 9 Mar. 2009 . Deploy. 2009. www.deploy-project.eu. Cited 9 Mar. 2009."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_48_1","volume-title":"Engineering and Physical Sciences Research Council. www.epsrc.ac.uk. Cited","year":"2009","unstructured":"EPSRC. 2009. Engineering and Physical Sciences Research Council. www.epsrc.ac.uk. Cited 9 Mar. 2009 . EPSRC. 2009. Engineering and Physical Sciences Research Council. www.epsrc.ac.uk. Cited 9 Mar. 2009."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.976940"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(96)00122-7"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1361213.1361214"},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of Symposia in Applied Mathematics, Rhode Island. American Mathematical Society","author":"Floyd R.","year":"1967","unstructured":"Floyd , R. 1967 . Assigning meanings to programs. In Mathematical Aspects of Computer Science , Proceedings of Symposia in Applied Mathematics, Rhode Island. American Mathematical Society , Providence, RI, 19--32. Floyd, R. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, Rhode Island. American Mathematical Society, Providence, RI, 19--32."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/3065491.3065652"},{"key":"e_1_2_1_54_1","series-title":"Lecture Notes in Computer Science","volume-title":"TAPSOFT'95: Proceedings of the 6th International Joint Conference Theory and Practice of Software Development, CAAP\/FASE","author":"Gaudel M.-C.","unstructured":"Gaudel , M.-C. 1995. Testing can be formal, too . In TAPSOFT'95: Proceedings of the 6th International Joint Conference Theory and Practice of Software Development, CAAP\/FASE . Lecture Notes in Computer Science , vol. 915 . Springer-Verlag, Berlin , Heidelberg , 82--96. Gaudel, M.-C. 1995. Testing can be formal, too. In TAPSOFT'95: Proceedings of the 6th International Joint Conference Theory and Practice of Software Development, CAAP\/FASE. Lecture Notes in Computer Science, vol. 915. Springer-Verlag, Berlin, Heidelberg, 82--96."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0054-3"},{"key":"e_1_2_1_56_1","volume-title":"Crosstalk: The J. Defense Softw. Eng.","author":"George V.","year":"2003","unstructured":"George , V. and Vaughn , R . 2003 . Application of lightweight formal methods in requirement engineering. Crosstalk: The J. Defense Softw. Eng. George, V. and Vaughn, R. 2003. Application of lightweight formal methods in requirement engineering. Crosstalk: The J. Defense Softw. Eng."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/824462.824753"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 13th New Zealand Computer Society Conference, New Zealand Computer Society, Auckland, NZ, 207--217","author":"Gibbons J.","year":"1993","unstructured":"Gibbons , J. 1993 . Formal methods: Why should I care? The development of the T800 Transputer floating-point unit . In Proceedings of the 13th New Zealand Computer Society Conference, New Zealand Computer Society, Auckland, NZ, 207--217 . Gibbons, J. 1993. Formal methods: Why should I care? The development of the T800 Transputer floating-point unit. In Proceedings of the 13th New Zealand Computer Society Conference, New Zealand Computer Society, Auckland, NZ, 207--217."},{"key":"e_1_2_1_59_1","first-page":"3","article-title":"Software's chronic crisis. Sci","volume":"271","author":"Gibbs W. W.","year":"1994","unstructured":"Gibbs , W. W. 1994 . Software's chronic crisis. Sci . Amer. 271 , 3 (Sept.), 72--81. Gibbs, W. W. 1994. Software's chronic crisis. Sci. Amer. 271, 3 (Sept.), 72--81.","journal-title":"Amer."},{"key":"e_1_2_1_60_1","first-page":"4","article-title":"Formal methods are a surrogate for a more serious software concern","volume":"29","author":"Glass R. L.","year":"1996","unstructured":"Glass , R. L. 1996 . Formal methods are a surrogate for a more serious software concern . IEEE Comput. 29 , 4 (Apr.), 19. Glass, R. L. 1996. Formal methods are a surrogate for a more serious software concern. IEEE Comput. 29, 4 (Apr.), 19.","journal-title":"IEEE Comput."},{"key":"e_1_2_1_61_1","volume-title":"STACS. Lecture Notes in Computer Science","volume":"247","author":"Goldsmith M.","unstructured":"Goldsmith , M. , Cox , A. , and Barrett , G . 1987. An algebraic transformation system for Occam programs . In STACS. Lecture Notes in Computer Science , vol. 247 . Springer-Verlag, Berlin, Heidelberg, Germany, 481. Goldsmith, M., Cox, A., and Barrett, G. 1987. An algebraic transformation system for Occam programs. In STACS. Lecture Notes in Computer Science, vol. 247. Springer-Verlag, Berlin, Heidelberg, Germany, 481."},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the NSA High-Confidence Systems and Software Conference (HCSS).","author":"Greve D.","unstructured":"Greve , D. and Wilding , M . 2002. Evaluatable, high-assurance microprocessors . In Proceedings of the NSA High-Confidence Systems and Software Conference (HCSS). Greve, D. and Wilding, M. 2002. Evaluatable, high-assurance microprocessors. In Proceedings of the NSA High-Confidence Systems and Software Conference (HCSS)."},{"key":"e_1_2_1_63_1","volume-title":"ICSE: Proceedings of the 12th International Conference on Software Engineering. IEEE Computer Society Press","author":"Guiho G. D.","unstructured":"Guiho , G. D. and Hennebert , C . 1990. SACEM software validation (experience report) . In ICSE: Proceedings of the 12th International Conference on Software Engineering. IEEE Computer Society Press , Los Alamitos, CA, 186--191. Guiho, G. D. and Hennebert, C. 1990. SACEM software validation (experience report). In ICSE: Proceedings of the 12th International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 186--191."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.976937"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0057-0"},{"key":"e_1_2_1_67_1","volume-title":"SACEM: A fault tolerant system for train speed control. In Proceedings of the Fault Tolerence Computing Systems (FTCS)","author":"Hennebert C.","year":"1993","unstructured":"Hennebert , C. and Guiho , G. D . 1993 . SACEM: A fault tolerant system for train speed control. In Proceedings of the Fault Tolerence Computing Systems (FTCS) . IEEE Computer Society Press , Los Alamitos, CA , 624--628. Hennebert, C. and Guiho, G. D. 1993. SACEM: A fault tolerant system for train speed control. In Proceedings of the Fault Tolerence Computing Systems (FTCS). IEEE Computer Society Press, Los Alamitos, CA, 624--628."},{"key":"e_1_2_1_68_1","volume-title":"Eds","author":"Hierons R. M.","year":"2008","unstructured":"Hierons , R. M. , Bowen , J. P. , and Harman , M. , Eds . 2008 . Formal Methods and Testing An Outcome of the FORTEST Network. Revised Selected Papers. Lecture Notes in Computer Science, vol. 4949 . Springer-Verlag , Berlin, Heidelberg, Germany. Hierons, R. M., Bowen, J. P., and Harman, M., Eds. 2008. Formal Methods and Testing An Outcome of the FORTEST Network. Revised Selected Papers. Lecture Notes in Computer Science, vol. 4949. Springer-Verlag, Berlin, Heidelberg, Germany."},{"key":"e_1_2_1_69_1","unstructured":"Hinchey M. G. and Bowen J. P. 1995. Applications of Formal Methods. Prentice-Hall Englewood Cliffs NJ. Hinchey M. G. and Bowen J. P. 1995. Applications of Formal Methods. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_70_1","unstructured":"Hinchey M. G. and Bowen J. P. 1996. To formalize or not to formalize? IEEE Comput. 29 4 (Apr.) 18--19. Hinchey M. G. and Bowen J. P. 1996. To formalize or not to formalize? IEEE Comput. 29 4 (Apr.) 18--19."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_73_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"Hoare , C. A. R. 1985. Communicating Sequential Processes . Prentice-Hall , Englewood Cliffs, NJ . Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/645984.676027"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_76_1","unstructured":"Hoare T. 2002b. Assert early and assert often: Practical hints on effective asserting. Presentation at Microsoft Techfest. Hoare T. 2002b. Assert early and assert often: Practical hints on effective asserting. Presentation at Microsoft Techfest."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxl078"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_1"},{"key":"e_1_2_1_79_1","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","unstructured":"Holzmann , G. J. 2004. The SPIN Model Checker: Primer and Reference Manual . Addison-Wesley, Reading , MA. Holzmann, G. J. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2007.190611"},{"key":"e_1_2_1_81_1","volume-title":"VDM '91: Formal Software Development Methods. Lecture Notes in Computer Science","volume":"551","author":"Houston I.","unstructured":"Houston , I. and King , S . 1991. Experiences and results from the use of Z in IBM . In VDM '91: Formal Software Development Methods. Lecture Notes in Computer Science , vol. 551 . Springer-Verlag, Berlin, Heidelberg, Germany, 588--595. Houston, I. and King, S. 1991. Experiences and results from the use of Z in IBM. In VDM '91: Formal Software Development Methods. Lecture Notes in Computer Science, vol. 551. Springer-Verlag, Berlin, Heidelberg, Germany, 588--595."},{"key":"e_1_2_1_83_1","volume-title":"Standard 754-1985 ed","unstructured":"IEEE. 1985. Standard for Binary Floating-Point Arithmetic , Standard 754-1985 ed . ANSI\/IEEE , New York . IEEE. 1985. Standard for Binary Floating-Point Arithmetic, Standard 754-1985 ed. ANSI\/IEEE, New York."},{"key":"e_1_2_1_84_1","volume-title":"Occam2 Reference Manual","author":"Inmos Ltd","unstructured":"Inmos Ltd . 1988a. Occam2 Reference Manual . Prentice Hall , Englewood Cliffs, NJ . Inmos Ltd. 1988a. Occam2 Reference Manual. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_85_1","volume-title":"Transputer Reference Manual","author":"Inmos Ltd","unstructured":"Inmos Ltd . 1988b. Transputer Reference Manual . Prentice Hall, Englewood Cliffs , NJ. Inmos Ltd. 1988b. Transputer Reference Manual. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_87_1","first-page":"4","article-title":"Lightweight formal methods","volume":"29","author":"Jackson D.","year":"1996","unstructured":"Jackson , D. and Wing , J. 1996 . Lightweight formal methods . IEEE Comput. 29 , 4 (Apr.), 22--23. Jackson, D. and Wing, J. 1996. Lightweight formal methods. IEEE Comput. 29, 4 (Apr.), 22--23.","journal-title":"IEEE Comput."},{"key":"e_1_2_1_89_1","first-page":"4","article-title":"A rigorous approach to formal methods","volume":"29","author":"Jones C.","year":"1996","unstructured":"Jones , C. 1996 . A rigorous approach to formal methods . IEEE Comput. 29 , 4 (Apr.), 20--21. Jones, C. 1996. A rigorous approach to formal methods. IEEE Comput. 29, 4 (Apr.), 20--21.","journal-title":"IEEE Comput."},{"key":"e_1_2_1_90_1","volume-title":"Systematic Software Development Using VDM","author":"Jones C. B.","unstructured":"Jones , C. B. 1990. Systematic Software Development Using VDM , 2 nd ed. Prentice-Hall International, Englewood Cliffs , NJ. Jones, C. B. 1990. Systematic Software Development Using VDM, 2nd ed. Prentice-Hall International, Englewood Cliffs, NJ.","edition":"2"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.46"},{"key":"e_1_2_1_92_1","unstructured":"Jones G. and Goldsmith M. 1988. Programming in Occam2. Prentice-Hall Englewood Cliffs NJ. Jones G. and Goldsmith M. 1988. Programming in Occam2. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_93_1","volume-title":"The Single Unix Specification Version 3","author":"Josey A.","year":"1931","unstructured":"Josey , A. 2004. The Single Unix Specification Version 3 . Open Group, San Francisco , CA. ISBN : 1931 62447X. Josey, A. 2004. The Single Unix Specification Version 3. Open Group, San Francisco, CA. ISBN: 193162447X."},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_2_1_95_1","volume-title":"Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science","volume":"33","author":"Kars P.","year":"1997","unstructured":"Kars , P. 1997 . The application of PROMELA and SPIN in the BOS project. In The SPIN Verification System: The Second Workshop on the SPIN Verification System . Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science , vol. 33 . Rutgers University, Piscataway, NJ, 51--63. Kars, P. 1997. The application of PROMELA and SPIN in the BOS project. In The SPIN Verification System: The Second Workshop on the SPIN Verification System. Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 33. Rutgers University, Piscataway, NJ, 51--63."},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481874"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.5555\/3065491.3065650"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_31"},{"key":"e_1_2_1_99_1","volume-title":"FACS 2007 Christmas Workshop: Formal Methods in Industry, BCS, eWIC","author":"Larsen P. G.","unstructured":"Larsen , P. G. and Fitzgerald , J . 2007. Recent industrial applications of VDM in Japan . In FACS 2007 Christmas Workshop: Formal Methods in Industry, BCS, eWIC , London, U.K. Larsen, P. G. and Fitzgerald, J. 2007. Recent industrial applications of VDM in Japan. In FACS 2007 Christmas Workshop: Formal Methods in Industry, BCS, eWIC, London, U.K."},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.493020"},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2004.1293079"},{"key":"e_1_2_1_102_1","volume-title":"6th International Andrei Ershov Memorial Conference, PSI","volume":"4378","author":"Leino K. R. M.","year":"2007","unstructured":"Leino , K. R. M. 2007 . Specifying and verifying programs in Spec#. In Perspectives of Systems Informatics , 6th International Andrei Ershov Memorial Conference, PSI 2006, Revised Papers. Lecture Notes in Computer Science , vol. 4378 . Springer-Verlag, Berlin, Heidelberg, Germany, 20. Leino, K. R. M. 2007. Specifying and verifying programs in Spec#. In Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Revised Papers. Lecture Notes in Computer Science, vol. 4378. Springer-Verlag, Berlin, Heidelberg, Germany, 20."},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1992.0022"},{"key":"e_1_2_1_104_1","unstructured":"Meyer B. 1991. In Advances in Object-Oriented Software Engineering Prentice-Hall Englewood Cliffs NJ Chapter Design by Contract 1--50. Meyer B. 1991. In Advances in Object-Oriented Software Engineering Prentice-Hall Englewood Cliffs NJ Chapter Design by Contract 1--50."},{"key":"e_1_2_1_105_1","volume-title":"Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT95)","author":"Miller S.","unstructured":"Miller , S. and Srivas , M . 1995. Formal verification of the AAMP5 microprocessor . In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT95) . IEEE Computer Society Press, Los Alamitos, CA. Miller, S. and Srivas, M. 1995. Formal verification of the AAMP5 microprocessor. In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT95). IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_106_1","volume-title":"The industrial use of formal methods: Was Darwin right&quest","author":"Miller S. P.","unstructured":"Miller , S. P. 1998. The industrial use of formal methods: Was Darwin right&quest ; In Proceedings of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques. IEEE Computer Society Press , Los Alamitos, CA, 74--82. Miller, S. P. 1998. The industrial use of formal methods: Was Darwin right? In Proceedings of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques. IEEE Computer Society Press, Los Alamitos, CA, 74--82."},{"key":"e_1_2_1_107_1","volume-title":"Proceedings of the 3rd AMAST Workshop on Real-Time Systems.","author":"Miller S. P.","unstructured":"Miller , S. P. , Greve , D. A. , and Srivas , M. K . 1996. Formal verification of the AAMP5 and AAMP-FV microcode . In Proceedings of the 3rd AMAST Workshop on Real-Time Systems. Miller, S. P., Greve, D. A., and Srivas, M. K. 1996. Formal verification of the AAMP5 and AAMP-FV microcode. In Proceedings of the 3rd AMAST Workshop on Real-Time Systems."},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_112_1","volume-title":"The Invisible Computer: Why Good Products Can Fail, the Personal Computer Is So Complex, and Information Appliances Are the Solution","author":"Norman D. A.","unstructured":"Norman , D. A. 1999. The Invisible Computer: Why Good Products Can Fail, the Personal Computer Is So Complex, and Information Appliances Are the Solution . MIT Press , Cambridge, MA . Norman, D. A. 1999. The Invisible Computer: Why Good Products Can Fail, the Personal Computer Is So Complex, and Information Appliances Are the Solution. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_113_1","volume-title":"15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL. Lecture Notes in Computer Science","volume":"2142","author":"O'Hearn P. W.","unstructured":"O'Hearn , P. W. , Reynolds , J. C. , and Yang , H . 2001. Local reasoning about programs that alter data structures. In Computer Science Logic , 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL. Lecture Notes in Computer Science , vol. 2142 . Springer-Verlag, Berlin, Heidelberg, Germany, 1--19. O'Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL. Lecture Notes in Computer Science, vol. 2142. Springer-Verlag, Berlin, Heidelberg, Germany, 1--19."},{"key":"e_1_2_1_114_1","volume-title":"Overture web site. www.overturetool.org. Cited","author":"Overture-Core-Team","year":"2009","unstructured":"Overture-Core-Team . 2007. Overture web site. www.overturetool.org. Cited 9 Mar. 2009 . Overture-Core-Team. 2007. Overture web site. www.overturetool.org. Cited 9 Mar. 2009."},{"key":"e_1_2_1_115_1","series-title":"Lecture Notes in Computer Science","volume-title":"PVS: A prototype verification system. In CADE-11, Proceedings of the 11th International Conference on Automated Deduction","author":"Owre S.","year":"1992","unstructured":"Owre , S. , Rushby , J. M. , and Shankar , N . 1992 . PVS: A prototype verification system. In CADE-11, Proceedings of the 11th International Conference on Automated Deduction . Lecture Notes in Computer Science , vol. 607 . Springer-Verlag , Berlin, Heidelberg , Germany, 748--752. Owre, S., Rushby, J. M., and Shankar, N. 1992. PVS: A prototype verification system. In CADE-11, Proceedings of the 11th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 607. Springer-Verlag, Berlin, Heidelberg, Germany, 748--752."},{"key":"e_1_2_1_116_1","series-title":"The BCS Practitioners Series","volume-title":"The RAISE Specification Language","author":"RAISE Language Group","unstructured":"RAISE Language Group . 1992. The RAISE Specification Language . The BCS Practitioners Series . Prentice-Hall, Englewood Cliffs , NJ. RAISE Language Group. 1992. The RAISE Specification Language. The BCS Practitioners Series. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_117_1","series-title":"The BCS Practitioners Series","volume-title":"The RAISE Development Method","author":"RAISE Method Group","unstructured":"RAISE Method Group . 1995. The RAISE Development Method . The BCS Practitioners Series . Prentice-Hall International, Engleward Cliffs , NJ. RAISE Method Group. 1995. The RAISE Development Method. The BCS Practitioners Series. Prentice-Hall International, Engleward Cliffs, NJ."},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0058-z"},{"key":"e_1_2_1_119_1","first-page":"2","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov A.","year":"2002","unstructured":"Riazanov , A. and Voronkov , A. 2002 . The design and implementation of VAMPIRE . AI Commun. 15 , 2 -- 3 , 91--110. Riazanov, A. and Voronkov, A. 2002. The design and implementation of VAMPIRE. AI Commun. 15, 2--3, 91--110.","journal-title":"AI Commun."},{"key":"e_1_2_1_120_1","volume-title":"RODIN web site. rodin.cs.ncl.ac.uk\/. Cited","author":"Project-Members","year":"2009","unstructured":"RODIN- Project-Members . 2007. RODIN web site. rodin.cs.ncl.ac.uk\/. Cited 9 Mar. 2009 . RODIN-Project-Members. 2007. RODIN web site. rodin.cs.ncl.ac.uk\/. Cited 9 Mar. 2009."},{"key":"e_1_2_1_121_1","first-page":"54","article-title":"DEPLOY: Industrial deployment of advanced system engineering methods for high productivity and dependability","volume":"74","author":"Romanovsky A.","year":"2008","unstructured":"Romanovsky , A. 2008 . DEPLOY: Industrial deployment of advanced system engineering methods for high productivity and dependability . ERCIM News 74 , 54 -- 55 . Romanovsky, A. 2008. DEPLOY: Industrial deployment of advanced system engineering methods for high productivity and dependability. ERCIM News 74, 54--55.","journal-title":"ERCIM News"},{"key":"e_1_2_1_122_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90049-7"},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2000.895446"},{"key":"e_1_2_1_125_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1996.488298"},{"key":"e_1_2_1_126_1","volume-title":"Second International Conference, VSTTE","volume":"5295","author":"Shankar N.","year":"2008","unstructured":"Shankar , N. and Woodcock , J. , Eds . 2008. Verified Software: Theories, Tools, Experiments , Second International Conference, VSTTE 2008 . Lecture Notes in Computer Science , vol. 5295 . Springer-Verlag, Berlin, Heidelberg, Germany. Shankar, N. and Woodcock, J., Eds. 2008. Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008. Lecture Notes in Computer Science, vol. 5295. Springer-Verlag, Berlin, Heidelberg, Germany."},{"key":"e_1_2_1_127_1","volume-title":"Communicating Process Architectures","author":"Shepherd D.","unstructured":"Shepherd , D. 1988. The role of Occam in the design of the IMS T800 . In Communicating Process Architectures . Prentice-Hall , Englewood Cliffs, NJ . Shepherd, D. 1988. The role of Occam in the design of the IMS T800. In Communicating Process Architectures. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_128_1","first-page":"39","article-title":"Making chips that work","volume":"1664","author":"Shepherd D.","year":"1989","unstructured":"Shepherd , D. and Wilson , G. 1989 . Making chips that work . New Scientist 1664 , 39 -- 42 . Shepherd, D. and Wilson, G. 1989. Making chips that work. New Scientist 1664, 39--42.","journal-title":"New Scientist"},{"key":"e_1_2_1_129_1","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125811"},{"key":"e_1_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00166-X"},{"key":"e_1_2_1_131_1","volume-title":"A look at zero-defect code. www.spinellis.gr\/blog\/20081018\/. Cited","author":"Spinellis D.","year":"2009","unstructured":"Spinellis , D. 2008. A look at zero-defect code. www.spinellis.gr\/blog\/20081018\/. Cited 9 Mar. 2009 . Spinellis, D. 2008. A look at zero-defect code. www.spinellis.gr\/blog\/20081018\/. Cited 9 Mar. 2009."},{"key":"e_1_2_1_132_1","series-title":"International Series in Computer Science","volume-title":"The Z Notation: a Reference Manual","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1989. The Z Notation: a Reference Manual . International Series in Computer Science . Prentice-Hall , Englewood Cliffs, NJ . Spivey, J. M. 1989. The Z Notation: a Reference Manual. International Series in Computer Science. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_133_1","volume-title":"Proceedings of the IFIP Conference on Hardware Description Languages and their Applications (CHDL'95)","author":"Srivas M.","unstructured":"Srivas , M. and Miller , S . 1995. Applying formal verification to a commercial microprocessor . In Proceedings of the IFIP Conference on Hardware Description Languages and their Applications (CHDL'95) . Srivas, M. and Miller, S. 1995. Applying formal verification to a commercial microprocessor. In Proceedings of the IFIP Conference on Hardware Description Languages and their Applications (CHDL'95)."},{"key":"e_1_2_1_134_1","unstructured":"Stepney S. Cooper D. and Woodcock J. 2000. An electronic purse: Specification refinement and proof. Technical Monograph PRG-126 Oxford University Computing Laboratory. Jul. Stepney S. Cooper D. and Woodcock J. 2000. An electronic purse: Specification refinement and proof. Technical Monograph PRG-126 Oxford University Computing Laboratory. Jul."},{"key":"e_1_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(93)90091-K"},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805818"},{"key":"e_1_2_1_137_1","volume-title":"www.adacore.com\/tokeneer. Cited","author":"Tokeneer","year":"2009","unstructured":"Tokeneer . 2009. www.adacore.com\/tokeneer. Cited 9 Mar. 2009 . Tokeneer. 2009. www.adacore.com\/tokeneer. Cited 9 Mar. 2009."},{"key":"e_1_2_1_138_1","volume-title":"Entrants' system descriptions. www.cs.miami.edu\/~tptp\/CASC\/J2\/SystemDescriptions.html. Cited","year":"2009","unstructured":"TPTP. 2009a. Entrants' system descriptions. www.cs.miami.edu\/~tptp\/CASC\/J2\/SystemDescriptions.html. Cited 9 Mar. 2009 . TPTP. 2009a. Entrants' system descriptions. www.cs.miami.edu\/~tptp\/CASC\/J2\/SystemDescriptions.html. Cited 9 Mar. 2009."},{"key":"e_1_2_1_139_1","volume-title":"The TPTP problem library for automated theorem proving. www.cs.miami.edu\/~tptp\/. Cited","year":"2009","unstructured":"TPTP. 2009b. The TPTP problem library for automated theorem proving. www.cs.miami.edu\/~tptp\/. Cited 9 Mar. 2009 . TPTP. 2009b. The TPTP problem library for automated theorem proving. www.cs.miami.edu\/~tptp\/. Cited 9 Mar. 2009."},{"key":"e_1_2_1_140_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011236117591"},{"key":"e_1_2_1_141_1","volume-title":"Proceedings of the 18th International Conference on Concurrency Theory, CONCUR 2007. Lecture Notes in Computer Science","volume":"4703","author":"Vafeiadis V.","unstructured":"Vafeiadis , V. and Parkinson , M. J . 2007. A marriage of rely\/guarantee and separation logic . In Proceedings of the 18th International Conference on Concurrency Theory, CONCUR 2007. Lecture Notes in Computer Science , vol. 4703 . Springer-Verlag, Berlin, Heidelberg, Germany, 256--271. Vafeiadis, V. and Parkinson, M. J. 2007. A marriage of rely\/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory, CONCUR 2007. Lecture Notes in Computer Science, vol. 4703. Springer-Verlag, Berlin, Heidelberg, Germany, 256--271."},{"key":"e_1_2_1_142_1","doi-asserted-by":"crossref","unstructured":"van Lamsweerde A. 2003. From system goals to software architecture. In SFM. 25--43. van Lamsweerde A. 2003. From system goals to software architecture. In SFM. 25--43.","DOI":"10.1007\/978-3-540-39800-4_2"},{"key":"e_1_2_1_143_1","volume-title":"Verified Software Repository. vsr.sourceforge.net\/fmsurvey.htm. Cited","year":"2009","unstructured":"VSR. 2009. Verified Software Repository. vsr.sourceforge.net\/fmsurvey.htm. Cited 9 Mar. 2009 . VSR. 2009. Verified Software Repository. vsr.sourceforge.net\/fmsurvey.htm. Cited 9 Mar. 2009."},{"key":"e_1_2_1_144_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194095000034"},{"key":"e_1_2_1_145_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_30"},{"key":"e_1_2_1_146_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011217102270"},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_2_1_148_1","unstructured":"Woodcock J. and Davies J. 1996. Using Z: Specification Refinement and Proof. International Series in Computer Science. Prentice-Hall Englewood Cliffs NJ. Woodcock J. and Davies J. 1996. Using Z: Specification Refinement and Proof. International Series in Computer Science. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_149_1","doi-asserted-by":"publisher","DOI":"10.5555\/3065491.3065655"},{"key":"e_1_2_1_150_1","volume-title":"Proceedings of the 1996 International Conference on Software Maintenance (ICSM '96)","author":"Younger E. J.","unstructured":"Younger , E. J. , Luo , Z. , Bennett , K. H. , and Bull , T. M . 1996. Reverse engineering concurrent programs using formal modelling and analysis . In Proceedings of the 1996 International Conference on Software Maintenance (ICSM '96) . IEEE Computer Society Press, Los Alamitos, CA, 255--264. Younger, E. J., Luo, Z., Bennett, K. H., and Bull, T. M. 1996. Reverse engineering concurrent programs using formal modelling and analysis. In Proceedings of the 1996 International Conference on Software Maintenance (ICSM '96). IEEE Computer Society Press, Los Alamitos, CA, 255--264."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1592434.1592436","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T06:20:37Z","timestamp":1672294837000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1592434.1592436"}},"subtitle":["Practice and experience"],"short-title":[],"issued":{"date-parts":[[2009,10]]},"references-count":141,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["10.1145\/1592434.1592436"],"URL":"https:\/\/doi.org\/10.1145\/1592434.1592436","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10]]},"assertion":[{"value":"2008-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}