{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:57:42Z","timestamp":1742961462163,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_39","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"561-579","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Empirical Software Metrics for Benchmarking of Verification Tools"],"prefix":"10.1007","author":[{"given":"Yulia","family":"Demyanova","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Pani","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"39_CR1","unstructured":"Collective benchmark (cBench). \n                      http:\/\/ctuning.org\/wiki\/index.php\/CTools:CBench\n                      \n                    . Accessed 6 Feb 2015"},{"key":"39_CR2","unstructured":"Competition on Software Verification 2014. \n                      http:\/\/sv-comp.sosy-lab.org\/2014\/\n                      \n                    . Accessed 6 Feb 2015"},{"key":"39_CR3","unstructured":"Competition on Software Verification 2015. \n                      http:\/\/sv-comp.sosy-lab.org\/2015\/\n                      \n                    . Accessed 6 Feb 2015"},{"key":"39_CR4","unstructured":"SV-COMP 2014 - Minutes. \n                      http:\/\/sv-comp.sosy-lab.org\/2015\/Minutes-2014.txt\n                      \n                    . Accessed 6 Feb 2015"},{"key":"39_CR5","unstructured":"Verifolio. \n                      http:\/\/forsyte.at\/software\/verifolio\/\n                      \n                    . Accessed 11 May 2015"},{"key":"39_CR6","volume-title":"Compilers: Princiles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Princiles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"39_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2015","unstructured":"Baier, C., Tinelli, C. (eds.): TACAS 2015. LNCS, vol. 9035. Springer, Heidelberg (2015)"},{"key":"39_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-54862-8_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2014","unstructured":"Beyer, D.: Status report on software verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 373\u2013388. Springer, Heidelberg (2014)"},{"key":"39_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015)"},{"key":"39_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504\u2013518. Springer, Heidelberg (2007)"},{"key":"39_CR11","volume-title":"Pattern Recognition and Machine Learning","author":"CM Bishop","year":"2006","unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning. Springer, New York (2006)"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Boser, B.E., Guyon, I., Vapnik, V.: A training algorithm for optimal margin classifiers. In: Conference on Computational Learning Theory (COLT 1992), pp. 144\u2013152 (1992)","DOI":"10.1145\/130385.130401"},{"issue":"3","key":"39_CR13","first-page":"27","volume":"2","author":"C Chang","year":"2011","unstructured":"Chang, C., Lin, C.: LIBSVM: a library for support vector machines. ACM TIST 2(3), 27 (2011)","journal-title":"ACM TIST"},{"key":"39_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"3","key":"39_CR15","first-page":"273","volume":"20","author":"C Cortes","year":"1995","unstructured":"Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273\u2013297 (1995)","journal-title":"Mach. Learn."},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Demyanova, Y., Veith, H., Zuleger, F.: On the concept of variable roles and its use in software analysis. In: Formal Methods in Computer-Aided Design (FMCAD 2013), pp. 226\u2013230 (2013)","DOI":"10.1109\/FMCAD.2013.6679414"},{"key":"39_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-38856-9_13","volume-title":"Static Analysis","author":"K Dudka","year":"2013","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 215\u2013237. Springer, Heidelberg (2013)"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-20895-9_40","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2011","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T., Schneider, M.T., Ziller, S.: A portfolio solver for answer set programming: preliminary report. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol. 6645, pp. 352\u2013357. Springer, Heidelberg (2011)"},{"issue":"1\u20132","key":"39_CR19","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0004-3702(00)00081-3","volume":"126","author":"CP Gomes","year":"2001","unstructured":"Gomes, C.P., Selman, B.: Algorithm portfolios. Artif. Intell. 126(1\u20132), 43\u201362 (2001)","journal-title":"Artif. Intell."},{"key":"39_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-642-54862-8_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2014","unstructured":"Gurfinkel, A., Belov, A.: FrankenBit: bit-precise verification with many bits. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 408\u2013411. Springer, Heidelberg (2014)"},{"issue":"9","key":"39_CR21","doi-asserted-by":"publisher","first-page":"1263","DOI":"10.1109\/TKDE.2008.239","volume":"21","author":"H He","year":"2009","unstructured":"He, H., Garcia, E.A.: Learning from imbalanced data. Knowl. Data Eng. 21(9), 1263\u20131284 (2009)","journal-title":"Knowl. Data Eng."},{"key":"39_CR22","unstructured":"Hsu, C.W., Chang, C.C., Lin, C.J., et al.: A practical guide to support vector classification (2003)"},{"key":"39_CR23","first-page":"4365","volume":"7","author":"YM Huang","year":"2005","unstructured":"Huang, Y.M., Du, S.X.: Weighted support vector machine for classification with uneven training class sizes. Mach. Learn. Cybern. 7, 4365\u20134369 (2005)","journal-title":"Mach. Learn. Cybern."},{"issue":"5296","key":"39_CR24","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"BA Huberman","year":"1997","unstructured":"Huberman, B.A., Lukose, R.M., Hogg, T.: An economics approach to hard computational problems. Science 275(5296), 51\u201354 (1997)","journal-title":"Science"},{"key":"39_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-23786-7_35","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"S Kadioglu","year":"2011","unstructured":"Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 454\u2013469. Springer, Heidelberg (2011)"},{"key":"39_CR26","unstructured":"Lobjois, L., Lema\u00eetre, M.: Branch and bound algorithm selection by performance prediction. In: Mostow, J., Rich, C. (eds.) National Conference on Artificial Intelligence and Innovative Applications of Artificial Intelligence Conference, pp. 353\u2013358 (1998)"},{"key":"39_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-33353-8_39","volume-title":"Logics in Artificial Intelligence","author":"M Maratea","year":"2012","unstructured":"Maratea, M., Pulina, L., Ricca, F.: The multi-engine ASP solver me-asp. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS, vol. 7519, pp. 484\u2013487. Springer, Heidelberg (2012)"},{"key":"39_CR28","unstructured":"O\u2019Mahony, E., Hebrard, E., Holland, A., Nugent, C., OSullivan, B.: Using case-based reasoning in an algorithm portfolio for constraint solving. In: Irish Conference on Artificial Intelligence and Cognitive Science (2008)"},{"key":"39_CR29","unstructured":"Pani, T.: Loop patterns in C programs. Diploma Thesis (2014). \n                      http:\/\/forsyte.at\/static\/people\/pani\/sloopy\/thesis.pdf"},{"key":"39_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-540-74970-7_41","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"L Pulina","year":"2007","unstructured":"Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 574\u2013589. Springer, Heidelberg (2007)"},{"issue":"1","key":"39_CR31","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","volume":"14","author":"L Pulina","year":"2009","unstructured":"Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1), 80\u2013116 (2009)","journal-title":"Constraints"},{"key":"39_CR32","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0065-2458(08)60520-3","volume":"15","author":"JR Rice","year":"1976","unstructured":"Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65\u2013118 (1976)","journal-title":"Adv. Comput."},{"key":"39_CR33","unstructured":"Roussel, O.: Description of ppfolio. \n                      http:\/\/www.cril.univ-artois.fr\/~roussel\/ppfolio\/solver1.pdf"},{"key":"39_CR34","unstructured":"Samulowitz, H., Memisevic, R.: Learning to solve QBF. In: Proceedings of the Conference on Artificial Intelligence (AAAI), pp. 255\u2013260 (2007)"},{"key":"39_CR35","doi-asserted-by":"crossref","unstructured":"Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V.: MUX: algorithm selection for software model checkers. In: Working Conference on Mining Software Repositories, pp. 132\u2013141 (2014)","DOI":"10.1145\/2597073.2597080"},{"key":"39_CR36","first-page":"975","volume":"5","author":"TF Wu","year":"2004","unstructured":"Wu, T.F., Lin, C.J., Weng, R.C.: Probability estimates for multi-class classification by pairwise coupling. J. Mach. Learn. Res. 5, 975\u20131005 (2004)","journal-title":"J. Mach. Learn. Res."},{"key":"39_CR37","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. (JAIR) 32, 565\u2013606 (2008)","journal-title":"J. Artif. Intell. Res. (JAIR)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:11:05Z","timestamp":1563826265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}