{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:50Z","timestamp":1725484130090},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_15","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T00:45:28Z","timestamp":1179362728000},"page":"252-271","source":"Crossref","is-referenced-by-count":4,"title":["Verification Using Test Generation Techniques"],"prefix":"10.1007","author":[{"given":"Vlad","family":"Rusu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"P. Ammann and P. Black. Abstracting formal specifications to generate software tests via model checking. In Digital Avionics Systems Conference, DASC\u201999. Also a National Institute of Research and Technology research report, NIST-IR 6405.","DOI":"10.6028\/NIST.IR.6405"},{"issue":"2","key":"15_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein, and S.K. Ramajani. Automatic predicate abstraction of C programs. ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI\u201901, pages 203\u2013213.","DOI":"10.1145\/378795.378846"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"A. Belinfante, J. Feenstra, R. de Vries, J. Tretmans, N. Goga, L. Feijs, and S. Mauw. Formal test automation: a simple experiment. Int. Workshop on the Testing of Communicating Systems, IWTCS\u201999, pages 179\u2013196.","DOI":"10.1007\/978-0-387-35567-2_12"},{"key":"15_CR5","unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, C. Munoz, S. Owre, H. Rue\u00df, J. Rushby, V. Rusu, H. Sa\u00efdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. LFM 2000: NASA Langley Formal Methods Workshop, LFM\u201900, pages 187\u2013196."},{"issue":"1","key":"15_CR6","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Formal Methods in System Design, 15(1):75\u201392, 1999.","journal-title":"Formal Methods in System Design"},{"key":"15_CR7","unstructured":"CEPS: Common Electronic Purse System. http:\/\/www.cepsco.org ."},{"key":"15_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/3-540-45418-7_6","volume-title":"Conference on Research in Smart Cards, eSmart\u201901","author":"D. Clarke","year":"2001","unstructured":"D. Clarke, T. J\u00e9ron, V. Rusu, and E. Zinovieva. Automated test and oracle generation for smart-card applications. Conference on Research in Smart Cards, eSmart\u201901, pages 58\u201370. LNCS 2140."},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","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 (TACAS\u201902)","author":"D. Clarke","year":"2002","unstructured":"D. Clarke, T. J\u00e9ron, V. Rusu, and E. Zinovieva. stg: a Symbolic Test Generation tool. Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), pages 470\u2013475. LNCS 2280."},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u201996","author":"J.-C. Fernandez","year":"1996","unstructured":"J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A protocol validation and verification toolbox. Computer-Aided Verification, CAV\u201996. LNCS 1102."},{"key":"15_CR11","unstructured":"C. Flanagan and S. Qadeer. Predicate Abstraction for Software Verification. To appear in Principles of Program Design, POPL\u2019 02."},{"key":"15_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification, CAV\u201997","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. Computer Aided Verification, CAV\u201997, pages 72\u201383. LNCS 1254."},{"issue":"2","key":"15_CR13","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","first-page":"39","volume-title":"Concurrency Theory, CONCUR\u201901","author":"J. Hatcliff","year":"1997","unstructured":"J. Hatcliff and M. Dwyer, Using the Bandera tool set to model-check properties of concurrent Java software. Concurrency Theory, CONCUR\u201901, pages 39\u201359. LNCS 2154."},{"key":"15_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"Formal Methods Europe, FME\u201996","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. Formal Methods Europe, FME\u201996, pages 662\u2013681. LNCS 1051."},{"key":"15_CR16","unstructured":"T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. To appear in Principles of Program Design, POPL\u2019 02."},{"key":"15_CR17","unstructured":"G.J. Holzmann. Design and validation of communication protocols. Prentice Hall, 1991."},{"key":"15_CR18","unstructured":"ISO\/IEC. International Standard 9646, OSI-Open Systems Interconnection, Information Technology-Conformance Testing Methodology and Framework, 1992."},{"key":"15_CR19","unstructured":"R.S Lazi\u0107, T.C. Newcomb, and A.W. Roscoe. On model checking data-independent systems with arrays without reset. Oxford University Computing Laboratory, Research Report RR-02-02."},{"key":"15_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-48683-6_12","volume-title":"Computer-Aided Verification, CAV\u201999","author":"T. J\u00e9ron","year":"1999","unstructured":"T. J\u00e9ron and P. Morel. Test generation derived from model-checking. Computer-Aided Verification, CAV\u201999, pages 108\u2013122. LNCS 1633."},{"issue":"2","key":"15_CR21","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rusby, N. Shankar, and F. von Henke. Formal verification of fault-tolerant architectures: Prolegomena to the design of pvs. IEEE Transactions on Software Engineering, 21(2): 107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"V. Rusu. Verifying a sliding-window protocol using PVS. In Formal Techniques for Networked and Distributed Systems, FORTE\u201901, pages 251\u2013266. Kluwer Academic Publishers, 2001.","DOI":"10.1007\/0-306-47003-9_16"},{"key":"15_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-40911-4_20","volume-title":"Conference on Integrating Formal Methods (IFM\u201900)","author":"V. Rusu","year":"2000","unstructured":"V. Rusu, L. du Bousquet, and T. J\u00e9ron. An approach to symbolic test generation. Conference on Integrating Formal Methods (IFM\u201900), pages 338\u2013357. LNCS 1945."},{"key":"15_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer-Aided Verification, CAV\u201999","author":"H. Sa\u00efdi","year":"1999","unstructured":"H. Sa\u00efdi and N. Shankar. Abstract and model check while you prove. Computer-Aided Verification, CAV\u201999, pages 443\u2013454. LNCS 1633."},{"key":"15_CR25","unstructured":"F. Tip. A survey of program slicing techniques. Technical Report CS-R9438, Centrum voor Wiskunde en InformatIca, 1994."},{"key":"15_CR26","series-title":"Lect Notes Comput Sci","first-page":"46","volume-title":"Concurrency Theory, CONCUR\u201999","author":"J. Tretmans","year":"1664","unstructured":"J. Tretmans. Testing concurrent systems: A formal approach. Concurrency Theory, CONCUR\u201999, pages 46\u201365. LNCS 1664."},{"key":"15_CR27","unstructured":"L. Van Aertryck, M. Benveniste, and D. Le Metayer. casting: a formally based software test generation method. In IEEE International Conference on Formal Engineering Methods (ICFEM\u201997), 1997."},{"issue":"4","key":"15_CR28","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M. Weiser","year":"1984","unstructured":"M. Weiser. Program slicing. IEEE Transactions on Software Engineering, 10(4):352\u2013357, 1984.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T00:05:26Z","timestamp":1556409926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}