{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:50:44Z","timestamp":1762458644858},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_18","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"161-172","source":"Crossref","is-referenced-by-count":20,"title":["Automated Test Generation and Verified Software"],"prefix":"10.1007","author":[{"given":"John","family":"Rushby","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Hayhurst, K.J., Veerhusen, D.S., Chilenski, J.J., Rierson, L.K.: A practical tutorial on modified condition\/decision coverage. NASA Technical Memorandum TM-2001-210876, NASA Langley Research Center, Hampton, VA (2001), http:\/\/www.faa.gov\/certification\/aircraft\/av-info\/software\/Research\/MCDC%20Tutorial.pdf"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48166-4_10","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"A. Gargantini","year":"1999","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 146\u2013162. Springer, Heidelberg (1999)"},{"key":"18_CR3","first-page":"261","volume-title":"2nd International Conference on Software Engineering and Formal Methods (SEFM)","author":"G. Hamon","year":"2004","unstructured":"Hamon, G., de Moura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM), pp. 261\u2013270. IEEE Computer Society, Beijing (2004)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_42","volume-title":"Computer Aided Verification","author":"H. Sa\u00efdi","year":"1997","unstructured":"Sa\u00efdi, H., Graf, S.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: [48], pp. 67\u201381","DOI":"10.1007\/11513988_8"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11901914_27","volume-title":"Automated Technology for Verification and Analysis","author":"S. Xia","year":"2006","unstructured":"Xia, S., Di Vito, B., Mu\u00f1oz, C.: Predicate abstraction of programs with non-linear computation. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 352\u2013368. Springer, Heidelberg (2006)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Boppana, V., Rajan, S.P., Takayama, K., Fujita, M.: Model checking based on sequential ATPG. In: [49], pp. 418\u2013430","DOI":"10.1007\/3-540-48683-6_36"},{"key":"18_CR9","unstructured":"Ho, P.H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal simulation engines. In: International Conference on Computer Aided Design (ICCAD), Jan Jose, CA, Association for Computing Machinery, pp. 120\u2013126 (2000)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Conference on Programming Language Design and Implementation: PLDI, Chicago, IL. Association for Computing Machinery, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability modulo theories competition. In: [48], pp. 20\u201323.","DOI":"10.1007\/11513988_4"},{"key":"18_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1049\/sej.1991.0040","volume":"6","author":"G. Bernot","year":"1991","unstructured":"Bernot, G., Gaudel, M.C., Marre, B.: Software testing based on formal specifications: A theory and a tool. IEE\/BCS Software Engineering Journal\u00a06, 387\u2013405 (1991)","journal-title":"IEE\/BCS Software Engineering Journal"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45136-6_3","volume-title":"Reliable Software Technologies \u2013 Ada Europe 2001","author":"M.C. Gaudel","year":"2001","unstructured":"Gaudel, M.C.: Testing from formal specifications, a generic approach. In: Strohmeier, A., Craeynest, D. (eds.) Ada-Europe 2001. LNCS, vol.\u00a02043, pp. 35\u201348. Springer, Heidelberg (2001)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy. Association for Computing Machinery, pp. 123\u2013122 (2002)","DOI":"10.1145\/566172.566191"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"J\u00e9ron, T., Morel, P.: Test generation derived from model-checking. In: [49], pp. 108\u2013121","DOI":"10.1007\/3-540-48683-6_12"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: Proceedings of the 13th Annual Symposium on Foundations of Software Engineering (FSE), Lisbon, Portugal. Association for Computing Machinery, pp. 273\u2013282 (2005)","DOI":"10.1145\/1081706.1081751"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Tiwari, A.: Abstractions for hybrid systems. In: Formal Methods in Systems Design (to appear, 2007), http:\/\/www.csl.sri.com\/~tiwari\/new.pdf","DOI":"10.1007\/s10703-007-0044-3"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/3-540-45657-0_42","volume-title":"Computer Aided Verification","author":"S. Ben-David","year":"2002","unstructured":"Ben-David, S., Gringauze, A., Sterin, B., Wolfsthal, Y.: PathFinder: A tool for design exploration. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 510\u2013514. Springer, Heidelberg (2002)"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: International Conference on Functional Programming, Montreal, Canada. Association for Computing Machinery, pp. 268\u2013279 (2000)","DOI":"10.1145\/351240.351266"},{"key":"18_CR21","first-page":"230","volume-title":"2nd International Conference on Software Engineering and Formal Methods","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: 2nd International Conference on Software Engineering and Formal Methods, Beijing, China, pp. 230\u2013239. IEEE Computer Society, Los Alamitos (2004)"},{"key":"18_CR22","unstructured":"Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM), Seattle, WA (2006), http:\/\/fm.csl.sri.com\/AFM06\/papers\/5-Owre.pdf"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Sullivan, K., Yang, J., Coppit, D., Khurshid, S., Jackson, D.: Software assurance by bounded exhaustive testing. In: International Symposium on Software Testing and Analysis (ISSTA), Boston, MA. Association for Computing Machinery, pp. 133\u2013142 (2004)","DOI":"10.1145\/1007512.1007531"},{"key":"18_CR24","volume-title":"Test Driven Development: By Example","author":"K. Beck","year":"2002","unstructured":"Beck, K.: Test Driven Development: By Example. Addison-Wesley, Reading (2002)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-39910-0_16","volume-title":"Verification: Theory and Practice","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 332\u2013358. Springer, Heidelberg (2004)"},{"key":"18_CR26","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/ISSRE.2004.12","volume-title":"15th International Symposium on Software Reliability Engineering (ISSRE 2004)","author":"N. Kosmatov","year":"2004","unstructured":"Kosmatov, N., Legeard, B., Peureux, F., Utting, M.: Boundary coverage criteria for test generation from formal models. In: 15th International Symposium on Software Reliability Engineering (ISSRE 2004), Saint-Malo, France, pp. 139\u2013150. IEEE Computer Society, Los Alamitos (2004)"},{"key":"18_CR27","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1109\/32.286420","volume":"20","author":"E. Weyuker","year":"1994","unstructured":"Weyuker, E., Goradia, T., Singh, A.: Automatically generating test data from a Boolean specification. IEEE Transactions on Software Engineering\u00a020, 353\u2013363 (1994)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"18_CR28","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/322993.322996","volume":"8","author":"D.R. Kuhn","year":"1999","unstructured":"Kuhn, D.R.: Fault classes and error detection capability of specification-based testing. ACM Transactions on Software Engineering and Methodology\u00a08, 411\u2013424 (1999)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"18_CR29","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/504087.504089","volume":"11","author":"T. Tsuchiya","year":"2002","unstructured":"Tsuchiya, T., Kikuno, T.: On fault classes and error detection capability of specification-based testing. ACM Transactions on Software Engineering and Methodology\u00a011, 58\u201362 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"18_CR30","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1016\/j.infsof.2003.10.003","volume":"46","author":"V. Okun","year":"2004","unstructured":"Okun, V., Black, P.E., Yesha, Y.: Comparison of fault classes in specification-based testing. Information and Software Technology\u00a046, 525\u2013533 (2004)","journal-title":"Information and Software Technology"},{"key":"18_CR31","volume-title":"Practical Model-Based Testing","author":"M. Utting","year":"2006","unstructured":"Utting, M., Legeard, B.: Practical Model-Based Testing. Morgan Kaufmann, San Francisco (2006)"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-46002-0_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Clarke","year":"2002","unstructured":"Clarke, D., J\u00e9ron, T., Rusu, V., Zinovieva, E.: STG: a symbolic test generation tool. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 470\u2013475. Springer, Heidelberg (2002)"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy. Association for Computing Machinery, pp. 112\u2013122 (2002)","DOI":"10.1145\/566172.566190"},{"key":"18_CR34","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1145\/302405.302634","volume-title":"21st International Conference on Software Engineering","author":"L. Bosquet du","year":"1999","unstructured":"du Bosquet, L., Ouabdesselam, F., Richier, J.L., Zuanon, N.: Lutess: A specification-driven testing environment for synchronous software. In: 21st International Conference on Software Engineering, pp. 267\u2013276. IEEE Computer Society, Los Alamitos (1999)"},{"key":"18_CR35","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D. Lee","year":"1996","unstructured":"Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines. Proceedings of the IEEE\u00a084, 1090\u20131123 (1996)","journal-title":"Proceedings of the IEEE"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Whalen, M.W., Rajan, A., Heimdahl, M.P.E., Miller, S.P.: Coverage metrics for requirements-based testing. In: International Symposium on Software Testing and Analysis (ISSTA), Portland, ME. Association for Computing Machinery, pp. 25\u201336 (2006)","DOI":"10.1145\/1146238.1146242"},{"key":"18_CR37","first-page":"178","volume-title":"High-Assurance Systems Engineering Symposium","author":"M.P. Heimdahl","year":"2004","unstructured":"Heimdahl, M.P., George, D., Weber, R.: Specification test coverage adequacy criteria = specification test generation Inadequacy criteria? In: High-Assurance Systems Engineering Symposium, Tampa, FL, pp. 178\u2013186. IEEE Computer Society, Los Alamitos (2004)"},{"key":"18_CR38","unstructured":"Tretmans, J., Belinfante, A.: Automatic testing with formal methods. In: EuroSTAR 1999: 7 th European Int. Conference on Software Testing, Analysis & Review. EuroStar Conferences, Barcelona, Spain, Galway, Ireland (1999)"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-46419-0_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2000","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L.: Using static analysis to improve automatic test generatin. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 235\u2013250. Springer, Heidelberg (2000)"},{"key":"18_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-45614-7_15","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"V. Rusu","year":"2002","unstructured":"Rusu, V.: Verification using test generation techniques. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 252\u2013271. Springer, Heidelberg (2002)"},{"key":"18_CR41","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A new algorithm for property checking. In: Proceedings of the 14th Annual Symposium on Foundations of Software Engineering (FSE), Portland, OR. Association for Computing Machinery, pp. 117\u2013127 (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"18_CR42","unstructured":"Duprat, S., Souyris, J., Favre-Felix, D.: Formal verification workbench for Airbus avionics software. In: ERTS 2006: Embedded Real Time Software, Societe des Ingenieurs de l\u2019Automobile (2006)"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"Hamon, G., de Moura, L., Rushby, J.: Automated test generation with SAL. Technical note, Computer Science Laboratory, SRI International, Menlo Park, CA (2005), http:\/\/www.csl.sri.com\/users\/rushby\/abstracts\/sal-atg","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"18_CR44","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N.: Integrating verification components. In: These proceedings (2007)"},{"key":"18_CR45","first-page":"25","volume-title":"The International Conference on Dependable Systems and Networks","author":"R. Bloomfield","year":"2003","unstructured":"Bloomfield, R., Littlewood, B.: Multi-legged arguments: The impact of diversity upon confidence in dependability arguments. In: The International Conference on Dependable Systems and Networks, pp. 25\u201334. IEEE Computer Society, San Francisco (2003)"},{"key":"18_CR46","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1109\/TSE.2007.1002","volume":"33","author":"B. Littlewood","year":"2007","unstructured":"Littlewood, B., Wright, D.: The use of multi-legged arguments to increase confidence in safety claims for software-based systems: a study based on a BBN analysis of an idealised example. IEEE Transactions on Software Engineering\u00a033, 347\u2013365 (2007)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"18_CR47","volume-title":"12th IEEE International Conference on the Engineering of Complex Computer Systems (ICECCS)","author":"J. Rushby","year":"2007","unstructured":"Rushby, J.: What use is verified software? In: 12th IEEE International Conference on the Engineering of Complex Computer Systems (ICECCS), Auckland, New Zealand, IEEE Computer Society, Los Alamitos (2007), http:\/\/www.csl.sri.com\/~rushby\/abstracts\/iceccs07-vsi"},{"key":"18_CR48","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"2005","unstructured":"Etessami, K., Rajamani, S.K. (eds.): CAV 2005. LNCS, vol.\u00a03576. Springer, Heidelberg (2005)"},{"key":"18_CR49","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1999","unstructured":"Halbwachs, N., Peled, D.A. (eds.): CAV 1999. LNCS, vol.\u00a01633. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T17:50:36Z","timestamp":1631641836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}