{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,29]],"date-time":"2023-04-29T21:10:29Z","timestamp":1682802629200},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1996,11,1]],"date-time":"1996-11-01T00:00:00Z","timestamp":846806400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1996,11]]},"DOI":"10.1007\/bf00122083","type":"journal-article","created":{"date-parts":[[2004,10,31]],"date-time":"2004-10-31T07:48:16Z","timestamp":1099208896000},"page":"235-261","source":"Crossref","is-referenced-by-count":0,"title":["The incorporation of testing into formal verification: Direct, modular, and hierarchical correctness degrees"],"prefix":"10.1007","volume":"9","author":[{"given":"Leo","family":"Marcus","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"no. 1","key":"CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport, ?Composing specifications.? ACM Transactions on Programming Languages and Systems, vol. 15, no. 1, pp. 73?132, January 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"E. W. Adams, Probability and the logic of conditionals. In Hintikka and Suppes, editors, Aspects of Inductive Logic, pp. 265?316. North-Holland, 1966.","DOI":"10.1016\/S0049-237X(08)71673-2"},{"issue":"no. 2","key":"CR3","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1145\/356876.356879","volume":"14","author":"W. R. Adrion","year":"1982","unstructured":"W. R. Adrion, M.A. Branstad, and J. C. Cherniavsky, ?Validation, verification and testing of computer software.? Computing Surveys, ACM, vol. 14, no. 2, pp. 159?192, June 1982.","journal-title":"Computing Surveys, ACM"},{"key":"CR4","unstructured":"J. Alilovic-Curgus and S. T. Vuong, A metric based theory of test selection and coverage. In Proceedings of the IFIP WG 6.I Twelfth International Symposium on Protocol Specification, Testing, and Verification, 1993. North-Holland, 1993."},{"issue":"no. 9","key":"CR5","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1109\/TSE.1985.232545","volume":"11","author":"F. B. Bastani","year":"1985","unstructured":"F. B. Bastani, ?On the uncertainty in the correctness of computer programs.? IEEE Transactions on Software Engineering, vol. SE-11, no. 9, pp. 857?864, September 1985.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"G. Bernot, Testing against formal specifications: a theoretical view. In TAPSOFT 91, pages 99?119. Springer-Verlag, 1991. Lecture Notes in Computer Science, Volume 494.","DOI":"10.1007\/3540539816_63"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"G. Bernot, M. Claude Gaudel, and B. Marre, ?Software testing based on formal specifications: a theory and a tool.? Software Engineering Journal, pp. 387?405, November 1991.","DOI":"10.1049\/sej.1991.0040"},{"key":"CR8","unstructured":"M. Blum and P. Raghavan, ?Program correctness: Can one test for it?? In G. X. Ritter, editor, Information Processing 89, pp. 127?134. Elsevier Science Publishers, 1989."},{"key":"CR9","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0304-3975(85)90090-8","volume":"37","author":"L. Bouge","year":"1985","unstructured":"L. Bouge, ?A contribution to the theory of program testing.? Theoretical Computer Science, vol. 37, pp. 151?181, 1985.","journal-title":"Theoretical Computer Science"},{"key":"CR10","unstructured":"E. Brinksma, ?A theory for the derivation of tests.? In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing, and Verification VIII, pp. 63?74. Elsevier Science Publishers, 1988."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/52.143100","volume":"9","author":"S. Brocklehurst","year":"1992","unstructured":"S. Brocklehurst and B. Littlewood, ?New ways to get accurate reliability measures.? IEEE Software, vol. 9, pp. 34?42, July 1992.","journal-title":"IEEE Software"},{"key":"CR12","unstructured":"T.A. Budd and D. Angluin, ?Two notions of correctness and their relation to testing.? Technical Report TR-80-19, Department of Computer Science, The University of Arizona, June 1980."},{"issue":"no. 2","key":"CR13","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1109\/TSE.1980.234477","volume":"6","author":"R.C. Cheung","year":"1980","unstructured":"R.C. Cheung, ?A user-oriented software reliability model.? IEEE Transactions on Software Engineering, vol. SE-6, no. 2, pp. 118?125, March 1980.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR14","first-page":"77","volume-title":"Proceedings of the AIAA Computing in Aerospace Conference","author":"J. V. Cook","year":"1991","unstructured":"J. V. Cook, I. V. Filippenko, B. H. Levy, L. G. Marcus, and T. K. Menas, ?Formal Computer Verification in the State Delta Verification System (SDVS).? In Proceedings of the AIAA Computing in Aerospace Conference, pp. 77?87, Baltimore, Maryland, October 1991. American Institute of Aeronautics and Astronautics."},{"key":"CR15","volume-title":"Structured Programming","author":"C. J. Dahl","year":"1972","unstructured":"C. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, Structured Programming. Academic Press, London, 1972."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1145\/359488.359495","volume":"21","author":"M. Geller","year":"1978","unstructured":"M. Geller, ?Test data as an aid in proving program correctness.? Communications of the ACM, vol. 21, pp. 368?375, May 1978.","journal-title":"Communications of the ACM"},{"key":"CR17","series-title":"Technical Report UCB\/CSD 93\/737","volume-title":"Tight bounds on expected time to add correctly and add mostly correctly","author":"P. Gemmell","year":"1993","unstructured":"P., Gemmell and M., Harchol, ?Tight bounds on expected time to add correctly and add mostly correctly.? Technical Report UCB\/CSD 93\/737, Computer Science Division, UC Berkeley, April 1993."},{"key":"CR18","unstructured":"S. Gerhart, ?Program validation.? In T. Anderson and B. Randell, editors, Computing Systems Reliability, pp. 66?108. Cambridge University Press, 1979."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"S.L. Gerhart, ?A broad spectrum toolset for upstream testing, verification, and analysis.? In Workshop on Software Testing, Verification, and Analysis, pp. 4?12. IEEE, 1988.","DOI":"10.1109\/WST.1988.5349"},{"issue":"no. 2","key":"CR20","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1109\/TSE.1975.6312836","volume":"1","author":"J.B. Goodenough","year":"1975","unstructured":"J.B. Goodenough and S. L. Gerhart, ?Toward a theory of test data selection.? IEEE Transactions on Software Engineering, vol. SE-1, no. 2, pp. 156?173, June 1975.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"no. 6","key":"CR21","doi-asserted-by":"crossref","first-page":"686","DOI":"10.1109\/TSE.1983.235433","volume":"9","author":"J.S. Gourlay","year":"1983","unstructured":"J.S. Gourlay, ?A mathematical framework for the investigation of testing. IEEE Transactions on Software Engineering, vol. SE-9, no. 6, pp. 686?709, November 1983.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR22","unstructured":"G. Corporation, The Annotated Ada Reference Manual (ANSI\/MIL-STD-1815A-1983), June 1989."},{"key":"CR23","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0004-3702(90)90019-V","volume":"46","author":"J. Y. Halpern","year":"1990","unstructured":"J. Y. Halpern, ?An analysis of first-order logics of probability.? Artificial Intelligence, vol. 46, pp. 311?350, 1990.","journal-title":"Artificial Intelligence"},{"key":"CR24","unstructured":"D. Hamlet, ?Testing for probable correctness.? In Proceedings of the '86 Workshop on Software Testing, pp. 92?97. IEEE, 1986."},{"issue":"no. 12","key":"CR25","doi-asserted-by":"crossref","first-page":"1402","DOI":"10.1109\/32.62448","volume":"16","author":"D. Hamlet","year":"1990","unstructured":"D. Hamlet and R. Taylor. ?Partition testing does not inspire confidence.? IEEE Transactions on Software Engineering, vol. SE-16, no. 12, pp. 1402?1411, December 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"R. Hamlet, ?A patent problem for abstract programming languages: Machine-independent computations.? in Proceedings of the 4th Annual Symposium on Theory of Computing, pp. 193?197. ACM, 1972.","DOI":"10.1145\/800152.804914"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1093\/comjnl\/20.3.232","volume":"20","author":"R. Hamlet","year":"1977","unstructured":"R. Hamlet, ?Testing programs with finite sets of data.? The Computer Journal, vol. 20, pp. 232?237, 1977.","journal-title":"The Computer Journal"},{"key":"CR28","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00289588","volume":"16","author":"R. Hamlet","year":"1981","unstructured":"R. Hamlet, ?Reliability theory of program testing.? Acta Informatica, vol. 16, pp. 31?43, 1981.","journal-title":"Acta Informatica"},{"key":"CR29","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1145\/62959.62962","volume":"31","author":"R. Hamlet","year":"1988","unstructured":"R. Hamlet, ?Guest editor's introduction to special section on software testing.? Communications of the ACM, vol. 31, pp. 662?667, June 1988","journal-title":"Communications of the ACM"},{"issue":"no. 1","key":"CR30","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"332","author":"M. Hennessey","year":"1985","unstructured":"M. Hennessey and R. Milner, ?Algebraic laws for nondeterminism and concurrency.? Journal of the ACM, vol. 332, no. 1, pp. 137?162, 1985.","journal-title":"Journal of the ACM"},{"issue":"no. 3","key":"CR31","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1109\/TSE.1976.233816","volume":"2","author":"W. E. Howden","year":"1976","unstructured":"W. E. Howden, ?Reliability of the path analysis testing strategy.? IEEE Transactions on Software Engineering, vol. SE-2, no. 3, pp. 208?215, September 1976.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF00260923","volume":"10","author":"W. E. Howden","year":"1978","unstructured":"W. E. Howden, ?Algebraic program testing.? Acta Informatica, vol. 10, pp. 53?66, 1978.","journal-title":"Acta Informatica"},{"issue":"no. 1","key":"CR33","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1002\/stvr.4370010103","volume":"1","author":"W. E. Howden","year":"1993","unstructured":"W. E. Howden, ?Program testing versus proofs of correctness.? Journal of Software Testing, Verification, and Reliability, vol. 1, no. 1, pp. 5?15, 1993.","journal-title":"Journal of Software Testing, Verification, and Reliability"},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"H. Hungar, ?Combining model checking and theorem proving to verify parallel processes.? In Proceedings of the 1993 Workshop on Computer-Aided Verification, June 1993.","DOI":"10.1007\/3-540-56922-7_13"},{"key":"CR35","unstructured":"IEEE, Standard VHDL Language Reference Manual, 1988. IEEE Std. 1076-1987."},{"key":"CR36","unstructured":"D. Ince, ?The validation, verification, and testing of software.? In Oxford Surveys in Information Technology, vol. 2, pp. 1?40. Oxford University Press, 1985."},{"key":"CR37","doi-asserted-by":"crossref","unstructured":"A. M. Leone, ?Selecting an appropriate model for software reliability.? In Proceedings 1988 Annual Reliability and Maintainability Symposium, pp. 208?213. IEEE, 1988.","DOI":"10.1109\/ARMS.1988.196447"},{"key":"CR38","unstructured":"R. J. Lipton, ?New directions in testing.? In Distributed Computing and Cryptography; Proceedings of a DIMACS Workshop, October 4?6, 1989, pp. 191?202. AMS, ACM, 1991."},{"key":"CR39","unstructured":"L. G. Marcus, ?The incorporation of formal testing into verification: An introduction to a paradigm and summary of preliminary results.? Technical Report ATR-93(8354)-1, The Aerospace Corporation, September 1993."},{"issue":"no. 1","key":"CR40","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/32.120314","volume":"18","author":"K. W. Miller","year":"1992","unstructured":"K. W. Miller, L. J. Morell, tE. Noonan, S. K. Park, D. M. Nicol, B. W. Murrill, and J. M. Voas, ?Estimating the probability of failure when testing reveals no failures.? IEEE Transactions on Software Engineering, vol. SE-18, no. 1, pp. 33?43, January 1992.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR41","doi-asserted-by":"crossref","unstructured":"H. D. Mills, ?Zero defect software.? In Marshall C. Yovits, editor, Advances in Computers, vol. 36, pp. 1?41. Academic Press, Inc., 1993.","DOI":"10.1016\/S0065-2458(08)60269-7"},{"key":"CR42","unstructured":"T. J. Ostrand, R. Sigal, and E. J. Weyuker, ?Design for a tool to manage specification-based testing.? In Proceedings of the 86 Workshop on Software Testing, pp. 41?50. IEEE, 1986."},{"key":"CR43","doi-asserted-by":"crossref","unstructured":"J. Pearl, ?Reasoning under uncertainty.? In Joseph F. Traub, editor, Annual Review of Computer Science, vol. 4, pp. 37?72. Annual Reviews, Inc., 1989?1990.","DOI":"10.1146\/annurev.cs.04.060190.000345"},{"key":"CR44","unstructured":"M. Phalippou, ?The limited power of testing.? In Proceedings of the 5th Internation Workshop on Protocol Test Systems: Montreal, September 1992."},{"issue":"no. 12","key":"CR45","doi-asserted-by":"crossref","first-page":"1337","DOI":"10.1109\/32.62442","volume":"16","author":"D. H. Pitt","year":"1990","unstructured":"D. H. Pitt and D. Freestone. ?The derivation of conformance tests from LOTOS specifications.? IEEE Transactions on Software Engineering, vo. SE-16, no. 12, pp. 1337?1343, December 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR46","unstructured":"D. J. Richardson and L. A. Clarke, ?Testing techniques based on symbolic evaluation.? In T. Anderson, editor, Software Requirements, Specification, and Testing: Proceedings of CSR Workshop, pp. 93?110. Blackwell Scientific Publications, 1984."},{"issue":"no. 12","key":"CR47","doi-asserted-by":"crossref","first-page":"1477","DOI":"10.1109\/TSE.1985.231892","volume":"11","author":"D. J. Richardson","year":"1985","unstructured":"D. J. Richardson and L. A. Clarke, ?Partition analysis: A method combining testing and verification.? IEEE Transactions on Software Engineering, vol. SE-11, no. 12, pp. 1477?1490, December 1985.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR48","series-title":"Technical Report CS-TR-2988","volume-title":"Approximate testing theory","author":"K.A.R. Romanik","year":"1992","unstructured":"K.A.R. Romanik, ?Approximate testing theory.? Technical Report CS-TR-2988, UMIACS-TR-92?121, University of Maryland, College Park, November 1992."},{"key":"CR49","volume-title":"The Z Notation","author":"J. M. Spivey","year":"1989","unstructured":"J. M. Spivey, The Z Notation. Prentice Hall, Hertfordshire, U. K., 1989."},{"key":"CR50","doi-asserted-by":"crossref","unstructured":"M. Veeraraghavan and K. Trivedi, ?A combinatorial algorithm for performance and reliability analysis using multistate models.? To appear, IEEE-TC, 1993.","DOI":"10.1109\/12.262129"},{"key":"CR51","doi-asserted-by":"crossref","unstructured":"S. N. Weiss, ?Methods of comparing test data adequacy criteria.? In Proceedings of COMPSAC '90-The Fourteenth Annual International Computer Software and Applications Conference, Chicago, IL, October 1990.","DOI":"10.1109\/CMPSAC.1990.139305"},{"issue":"no. 10","key":"CR52","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1109\/32.6196","volume":"14","author":"S. N. Weiss","year":"1988","unstructured":"S. N. Weiss and E. J. Weyuker, ?An extended domain-based model of software reliability.? IEEE Transactions on Software Engineering, vol. SE-14, no. 10, pp. 1512?1524, October 1988.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"no. 1","key":"CR53","first-page":"55","volume":"23","author":"L. J. White","year":"1985","unstructured":"L. J. White, ?Domain testing and several outstanding research problems in program testing.? INFOR, vol. 23, no. 1, pp. 55?68, February 1985.","journal-title":"INFOR"},{"key":"CR54","doi-asserted-by":"crossref","unstructured":"L. J. White, ?Software testing and verification.? In Advances in Computers, vol. 26, pp. 335?391. Academic Press, Inc., 1987.","DOI":"10.1016\/S0065-2458(08)60010-8"},{"key":"CR55","unstructured":"J. A. Whittaker, Markov Chain Techniques for Software Testing and Reliability Analysis. PhD thesis, University of Tennessee, Knoxville, 1992."},{"key":"CR56","doi-asserted-by":"crossref","unstructured":"D. M. Woit, ?Specifying operational profiles for modules.? In Proceedings ISSTA (International Symposium on Software Testing and Analysis). ACM, June 1993.","DOI":"10.1145\/154183.154187"},{"issue":"no. 4","key":"CR57","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1145\/158431.158438","volume":"2","author":"P. Zave","year":"1993","unstructured":"P. Zave and M. Jackson, ?Conjunctions as composition.? ACM Transactions on Software Engineering and Methodology, vol. 2, no. 4, pp. 379?411, October 1993.","journal-title":"ACM Transactions on Software Engineering and Methodology"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00122083.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00122083\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00122083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,29]],"date-time":"2023-04-29T20:31:21Z","timestamp":1682800281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00122083"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,11]]},"references-count":57,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,11]]}},"alternative-id":["BF00122083"],"URL":"https:\/\/doi.org\/10.1007\/bf00122083","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,11]]}}}