{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T10:14:56Z","timestamp":1760955296388},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642246890"},{"type":"electronic","value":"9783642246906"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_26","type":"book-chapter","created":{"date-parts":[[2011,10,25]],"date-time":"2011-10-25T01:35:37Z","timestamp":1319506537000},"page":"382-398","source":"Crossref","is-referenced-by-count":23,"title":["Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques"],"prefix":"10.1007","author":[{"given":"Julian","family":"Tschannen","sequence":"first","affiliation":[]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Nordio","sequence":"additional","affiliation":[]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: POPL, pp. 4\u201316 (2002)","DOI":"10.1145\/503272.503275"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"issue":"5-6","key":"26_CR3","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur.\u00a012 (2008)","DOI":"10.1145\/1455518.1455522"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/11916246_5","volume-title":"Rigorous Development of Complex Fault-Tolerant Systems","author":"P. Chalin","year":"2006","unstructured":"Chalin, P.: Are practitioners writing contracts? In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.) Fault-Tolerant Systems. LNCS, vol.\u00a04157, pp. 100\u2013113. Springer, Heidelberg (2006)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: ISSTA (July 2010)","DOI":"10.1145\/1831708.1831719"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: Towards practical verification for Java. In: Proceedings of OOPSLA, pp. 213\u2013226 (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Ernst, M.: Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington, US (2000)","DOI":"10.1145\/302405.302467"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-13977-2_1","volume-title":"Tests and Proofs","author":"M.D. Ernst","year":"2010","unstructured":"Ernst, M.D.: How tests and proofs impede one another: The need for always-on static and dynamic feedback. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 1\u20132. Springer, Heidelberg (2010)"},{"key":"26_CR11","unstructured":"Eve: Eiffel verification environment, http:\/\/se.inf.ethz.ch\/research\/eve\/"},{"key":"26_CR12","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234\u2013245. ACM, New York (2002)"},{"key":"26_CR13","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1065010.1065036","volume-title":"Proceedings of PLDI","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI, pp. 213\u2013223. ACM, New York (2005)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., Misra, J.: Preface to special issue on software verification. ACM Comput. Surv.\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592435"},{"key":"26_CR15","unstructured":"Hunt, J.: Blackboard architectures, JayDee Technology Ltd. 27 (2002)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B. Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 304\u2013311. Springer, Heidelberg (2010)"},{"key":"26_CR17","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/229000.226319","volume-title":"Proceedings of ISSTA","author":"B. Korel","year":"1996","unstructured":"Korel, B.: Automated test data generation for programs with procedures. In: Proceedings of ISSTA, pp. 209\u2013215. ACM, New York (1996)"},{"key":"26_CR18","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/MC.2008.306","volume":"41","author":"B. Meyer","year":"2008","unstructured":"Meyer, B.: Seven principles of software testing. Computer\u00a041, 99\u2013101 (2008)","journal-title":"Computer"},{"key":"26_CR19","first-page":"46","volume":"42","author":"B. Meyer","year":"2009","unstructured":"Meyer, B., Fiva, A., Ciupa, I., Leitner, A., Wei, Y., Stapf, E.: Programs that test themselves. IEEE Software\u00a042, 46\u201355 (2009)","journal-title":"IEEE Software"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-13953-6_5","volume-title":"Objects, Models, Components, Patterns","author":"M. Nordio","year":"2010","unstructured":"Nordio, M., Calcagno, C., Meyer, B., M\u00fcller, P., Tschannen, J.: Reasoning about Function Objects. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol.\u00a06141, pp. 79\u201396. Springer, Heidelberg (2010)"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Ciupa, I., Meyer, B.: A comparative study of programmer-written and automatically inferred contracts. In: ISSTA, pp. 93\u2013104 (2009)","DOI":"10.1145\/1572272.1572284"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-05089-3_4","volume-title":"FM 2009: Formal Methods","author":"S.K. Rajamani","year":"2009","unstructured":"Rajamani, S.K.: Verification, testing and statistics. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 33\u201340. Springer, Heidelberg (2009)"},{"key":"26_CR23","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/1081706.1081750","volume-title":"Proceedings of ESEC\/FSE","author":"K. Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC\/FSE, pp. 263\u2013272. ACM, New York (2005)"},{"key":"26_CR24","unstructured":"International conference on tests and proofs. LNCS. Springer, Heidelberg (2007-2010)"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013white box test generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"26_CR26","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/1081706.1081749","volume-title":"Proceedings of ESEC\/FSE","author":"N. Tillmann","year":"2005","unstructured":"Tillmann, N., Schulte, W.: Parameterized unit tests. In: Proceedings of ESEC\/FSE, pp. 253\u2013262. ACM, New York (2005)"},{"key":"26_CR27","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: BOOGIE workshop (2011), http:\/\/arxiv.org\/abs\/1106.4700"},{"key":"26_CR28","unstructured":"Usable verification workshop (November 2010), http:\/\/fm.csl.sri.com\/UV10\/ ,"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: Proceedings of ICSE 2011, pp. 191\u2013200 (2011)","DOI":"10.1145\/1985793.1985820"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"Wei, Y., Gebhardt, S., Oriol, M., Meyer, B.: Satisfying test preconditions through guided object selection. In: Proceedings of ICST 2010, pp. 303\u2013312 (2010)","DOI":"10.1109\/ICST.2010.34"},{"key":"26_CR31","unstructured":"Wei, Y., Oriol, M., Meyer, B.: Is coverage a good measure of testing effectiveness? Technical Report 674, ETH Zurich (2010)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T03:00:18Z","timestamp":1713063618000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}