{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:01:04Z","timestamp":1725858064172},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319411347"},{"type":"electronic","value":"9783319411354"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41135-4_7","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T12:23:38Z","timestamp":1466425418000},"page":"112-129","source":"Crossref","is-referenced-by-count":13,"title":["Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification"],"prefix":"10.1007","author":[{"given":"Shaoying","family":"Liu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Dillinger, P.C., Manolios, P., Vroon, D., Moore, J.S.: The ACL2 Sedan. In: Proceedings of 7th Workshop on User Interfaces for Theorem Provers (UITP 2006). Electronic Notes in Theoretical Computer Science, pp. 3\u201318. Elsevier, 15 May 2007","DOI":"10.1016\/j.entcs.2006.09.018"},{"issue":"2","key":"7_CR2","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., Henke, F.V.: Formal verification for fault-tolerant architetures: prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21(2), 107\u2013125 (1995)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"T Leavens","year":"2007","unstructured":"Leavens, T., Rustand, K., Leino, M., Muller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19, 159\u2013189 (2007)","journal-title":"Formal Aspects Comput."},{"key":"7_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07287-5","volume-title":"Formal Engineering for Industrial Software Development Using the SOFL Method","author":"S Liu","year":"2004","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development Using the SOFL Method. Springer, Heidelberg (2004). ISBN: 3-540-20602-7"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Liu, S., Nakajima, S.: A decompositional approach to automatic test case generation based on formal specifications. In: 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010), Singapore, 9\u201311 June 2010, pp. 147\u2013155 (2010)","DOI":"10.1109\/SSIRI.2010.11"},{"key":"7_CR6","unstructured":"Manthey, N.: Solver Description of RISS 2.0 and PRISS 2.0, KRR Teport 12\u201302, Knowledge Representation and Reasoning, Technical University Dresden (2012)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"7_CR9","volume-title":"Black-Box Testing","author":"B Beizer","year":"1995","unstructured":"Beizer, B.: Black-Box Testing. Wiley, New York (1995)"},{"issue":"4","key":"7_CR10","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1109\/TR.2010.2085571","volume":"59","author":"S Liu","year":"2010","unstructured":"Liu, S., McDermid, J.A., Chen, Y.: A rigorous method for inspection of model-based formal specifications. IEEE Trans. Reliab. 59(4), 667\u2013684 (2010)","journal-title":"IEEE Trans. Reliab."},{"issue":"4","key":"7_CR11","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1145\/322993.322996","volume":"8","author":"DR Kuhn","year":"1999","unstructured":"Kuhn, D.R.: Fault classes and error detection capability of specification-based testing. ACM Trans. Softw. Eng. Methodol. 8(4), 411\u2013424 (1999)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"7_CR12","unstructured":"Chamarthi, H.R., Manolios, P.: Automated specification analysis using an interactive theorem prover. In: Formal Methods in Computer-Aided Design (FMCAD 2011), 30 October\u20132 November 2011, pp. 46\u201353. IEEE Press (2011)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Theorem Proving in Higher Order Logics","author":"P Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"key":"7_CR14","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Castern, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-319-22102-1_22","volume-title":"Interactive Theorem Proving","author":"Z Paraskevopoulou","year":"2015","unstructured":"Paraskevopoulou, Z., Hirtcu, C., Denes, M., Lamproulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) ITP. LNCS, vol. 9236, pp. 325\u2013343. Springer, Heidelberg (2015)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"Certified Programs and Proofs","author":"L Bulwahn","year":"2012","unstructured":"Bulwahn, L.: The new quickcheck for isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92\u2013108. Springer, Heidelberg (2012)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/978-3-540-24617-6_3","volume-title":"Formal Approaches to Software Testing","author":"R H\u00e4hnle","year":"2004","unstructured":"H\u00e4hnle, R., Wallenburg, A.: Using a software testing technique to improve theorem proving. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 30\u201341. Springer, Heidelberg (2004)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Chamarthi, H.R., Dillinger, P.C., Kaufmann, M.: Integrating testing and interactive theorem proving. In: Proceedings of 10th International Workshop on the ACL2 Theorem Prover and Its Applications (EPTCS 70), 3\u20134 November 2011, pp. 4\u201319 (2011)","DOI":"10.4204\/EPTCS.70.1"},{"key":"7_CR19","unstructured":"Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0024651","volume-title":"FME 1993: Industrial-Strength Formal Methods","author":"J Dick","year":"1993","unstructured":"Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Larsen, P.G., Wing, J.M. (eds.) FME 1993. LNCS, vol. 670, pp. 268\u2013284. Springer, Heidelberg (1993)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-45614-7_2","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"B Legeard","year":"2002","unstructured":"Legeard, B., Peureux, F., Utting, M.: Automated boundary testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 21\u201340. Springer, Heidelberg (2002)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0027283","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"S Helke","year":"1997","unstructured":"Helke, S., Neustupny, T., Santen, T.: Automating test case generation from Z specifications with Isabelle. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 52\u201371. Springer, Heidelberg (1997)"},{"issue":"4","key":"7_CR23","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: TestEra: specification-based testing of Java programs using SAT. Autom. Softw. Eng. 11(4), 403\u2013434 (2004)","journal-title":"Autom. Softw. Eng."},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-3-540-24605-3_21","volume-title":"Theory and Applications of Satisfiability Testing","author":"S Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A case for efficient solution enumeration. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 272\u2013286. Springer, Heidelberg (2004)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Salas, P.A.P.: Test case generation by OCL mutation and constraint solving. In: Cai, K.-Y., Ohnishi, A. (eds.) Proceedings of Fifth International Conference on Quality Software (QSIC 2005), Melbourne, Australia, 19\u201321 September 2005, pp. 64\u201371. IEEE CS Press (2005)","DOI":"10.1109\/QSIC.2005.63"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-39698-4_2","volume-title":"Theories of Programming and Formal Methods","author":"BK Aichernig","year":"2013","unstructured":"Aichernig, B.K.: Model-based mutation testing of reactive systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 23\u201336. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41135-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T20:12:56Z","timestamp":1568059976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}