{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:47:03Z","timestamp":1782877623414,"version":"3.54.5"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T00:00:00Z","timestamp":1484006400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11403-N23"],"award-info":[{"award-number":["S11403-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["PROSEED"],"award-info":[{"award-number":["PROSEED"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT12-059"],"award-info":[{"award-number":["ICT12-059"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10703-016-0264-5","type":"journal-article","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T15:25:14Z","timestamp":1484061914000},"page":"289-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Empirical software metrics for benchmarking of verification tools"],"prefix":"10.1007","volume":"50","author":[{"given":"Yulia","family":"Demyanova","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Pani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,1,10]]},"reference":[{"key":"264_CR1","volume-title":"Compilers: princiles, techniques, and tools","author":"AV Aho","year":"1986","unstructured":"Aho AV, Sethi R, Ullman JD (1986) Compilers: princiles, techniques, and tools. Addison-Wesley, Boston"},{"key":"264_CR2","doi-asserted-by":"crossref","unstructured":"Baier C, Tinelli C (eds) (2015) Tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11\u201318, 2015. In: Proceedings, Lecture Notes in Computer Science, vol. 9035. Springer","DOI":"10.1007\/978-3-662-46681-0"},{"key":"264_CR3","unstructured":"Beyer D (2014) Status report on software verification (competition summary SV-COMP 2014). In: Tools and algorithms for the construction and analysis of systems, pp 373\u2013388"},{"key":"264_CR4","unstructured":"Beyer D (2015) Software verification and verifiable witnesses\u2014(report on SV-COMP 2015). In: Proceedings of the tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11\u201318, 2015, pp 401\u2013416"},{"key":"264_CR5","doi-asserted-by":"publisher","unstructured":"Beyer D (2016) Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016). In: TACAS, Lecture Notes in computer science, vol 9636. Springer, pp 887\u2013904","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"264_CR6","doi-asserted-by":"publisher","unstructured":"Beyer D, Henzinger TA, Th\u00e9oduloz G (2007) Configurable software verification: concretizing the convergence of model checking and program analysis. In: Computer aided verification (CAV\u201907), pp 504\u2013518","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"264_CR7","volume-title":"Pattern recognition and machine learning","author":"CM Bishop","year":"2006","unstructured":"Bishop CM (2006) Pattern recognition and machine learning. Springer, New York"},{"key":"264_CR8","doi-asserted-by":"publisher","unstructured":"Boser BE, Guyon I, Vapnik V (1992) A training algorithm for optimal margin classifiers. In: Conference on computational learning theory (COLT\u201992), pp 144\u2013152","DOI":"10.1145\/130385.130401"},{"issue":"3","key":"264_CR9","first-page":"27","volume":"2","author":"C Chang","year":"2011","unstructured":"Chang C, Lin C (2011) LIBSVM: a library for support vector machines. ACM TIST 2(3):27","journal-title":"ACM TIST"},{"key":"264_CR10","doi-asserted-by":"publisher","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ansi-c programs. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"264_CR11","unstructured":"Collective benchmark (cBench). http:\/\/ctuning.org\/wiki\/index.php\/CTools:CBench . Accessed 11 Mar 2016"},{"key":"264_CR12","unstructured":"Competition on Software Verification (2014). http:\/\/sv-comp.sosy-lab.org\/2014\/ . Accessed 11 Mar 2016"},{"key":"264_CR13","unstructured":"Competition on Software Verification (2015). http:\/\/sv-comp.sosy-lab.org\/2015\/ . Accessed 11 Mar 2016"},{"key":"264_CR14","unstructured":"Competition on Software Verification (2016). http:\/\/sv-comp.sosy-lab.org\/2016\/ . Accessed 11 Mar 2016"},{"key":"264_CR15","unstructured":"Competition on Software Verification. http:\/\/sv-comp.sosy-lab.org\/ . Accessed 11 Mar 2016"},{"issue":"3","key":"264_CR16","first-page":"273","volume":"20","author":"C Cortes","year":"1995","unstructured":"Cortes C, Vapnik V (1995) Support-vector networks. Mach Learn 20(3):273\u2013297","journal-title":"Mach Learn"},{"key":"264_CR17","doi-asserted-by":"publisher","unstructured":"Demyanova Y, Pani T, Veith H, Zuleger F (2015) Empirical software metrics for benchmarking of verification tools. In: Proceedings of the computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Part I, pp 561\u2013579","DOI":"10.1007\/978-3-319-21690-4_39"},{"key":"264_CR18","doi-asserted-by":"publisher","unstructured":"Demyanova Y, Veith H, Zuleger F (2013) On the concept of variable roles and its use in software analysis. In: Formal methods in computer-aided design, FMCAD 2013, Portland, OR, USA, October 20\u201323, 2013, pp 226\u2013230","DOI":"10.1109\/FMCAD.2013.6679414"},{"key":"264_CR19","doi-asserted-by":"publisher","unstructured":"Dudka K, Peringer P, Vojnar T (2013) Byte-precise verification of low-level list manipulation. In: Static analysis. Springer, pp. 215\u2013237","DOI":"10.1007\/978-3-642-38856-9_13"},{"key":"264_CR20","doi-asserted-by":"publisher","unstructured":"Gebser M, Kaminski R, Kaufmann B, Schaub T, Schneider MT, Ziller S (2011) A portfolio solver for answer set programming: preliminary report. In: Logic programming and nonmonotonic reasoning (LPNMR\u201911), pp 352\u2013357","DOI":"10.1007\/978-3-642-20895-9_40"},{"issue":"1\u20132","key":"264_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0004-3702(00)00081-3","volume":"126","author":"CP Gomes","year":"2001","unstructured":"Gomes CP, Selman B (2001) Algorithm portfolios. Artif Intell 126(1\u20132):43\u201362","journal-title":"Artif Intell"},{"key":"264_CR22","unstructured":"Gurfinkel A, Belov A (2014) Frankenbit: Bit-precise verification with many bits\u2014(competition contribution). In: Tools and algorithms for the construction and analysis of systems (TACAS\u201914), pp 408\u2013411"},{"issue":"9","key":"264_CR23","doi-asserted-by":"publisher","first-page":"1263","DOI":"10.1109\/TKDE.2008.239","volume":"21","author":"H He","year":"2009","unstructured":"He H, Garcia EA (2009) Learning from imbalanced data. Knowl Data Eng 21(9):1263\u20131284","journal-title":"Knowl Data Eng"},{"key":"264_CR24","unstructured":"Hsu CW, Chang CC, Lin CJ, et\u00a0al (2003) A practical guide to support vector classification"},{"key":"264_CR25","first-page":"4365","volume":"7","author":"YM Huang","year":"2005","unstructured":"Huang YM, Du SX (2005) Weighted support vector machine for classification with uneven training class sizes. Mach Learn Cybern 7:4365\u20134369","journal-title":"Mach Learn Cybern"},{"issue":"5296","key":"264_CR26","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"BA Huberman","year":"1997","unstructured":"Huberman BA, Lukose RM, Hogg T (1997) An economics approach to hard computational problems. Science 275(5296):51\u201354","journal-title":"Science"},{"key":"264_CR27","doi-asserted-by":"publisher","unstructured":"Kadioglu S, Malitsky Y, Sabharwal A, Samulowitz H, Sellmann M (2011) Algorithm selection and scheduling. In: Principles and practice of constraint programming (CP\u201911), pp 454\u2013469","DOI":"10.1007\/978-3-642-23786-7_35"},{"key":"264_CR28","unstructured":"Lobjois L, Lematre M (1998) 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"},{"key":"264_CR29","doi-asserted-by":"publisher","unstructured":"Maratea M, Pulina L, Ricca F (2012) The multi-engine ASP solver me-asp. In: Logics in artificial intelligence (JELIA), pp 484\u2013487","DOI":"10.1007\/978-3-642-33353-8_39"},{"key":"264_CR30","unstructured":"O\u2019Mahony E, Hebrard E, Holland A, Nugent C, OSullivan B (2008) Using case-based reasoning in an algorithm portfolio for constraint solving. In: Irish conference on artificial intelligence and cognitive science"},{"key":"264_CR31","unstructured":"Pani T, Veith H, Zuleger F (2015) Loop patterns in C programs. ECEASST 72"},{"key":"264_CR32","doi-asserted-by":"publisher","unstructured":"Pulina L, Tacchella A (2007) A multi-engine solver for quantified boolean formulas. In: Bessiere C (ed) Principles and practice of constraint programming (CP\u201907), pp 574\u2013589","DOI":"10.1007\/978-3-540-74970-7_41"},{"issue":"1","key":"264_CR33","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 (2009) A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1):80\u2013116","journal-title":"Constraints"},{"key":"264_CR34","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0065-2458(08)60520-3","volume":"15","author":"JR Rice","year":"1976","unstructured":"Rice JR (1976) The algorithm selection problem. Adv Comput 15:65\u2013118","journal-title":"Adv Comput"},{"key":"264_CR35","unstructured":"Roussel O. Description of ppfolio. \u00a0 http:\/\/www.cril.univ-artois.fr\/~roussel\/ppfolio\/solver1.pdf"},{"key":"264_CR36","unstructured":"Samulowitz H, Memisevic R (2007) Learning to solve QBF. In: Proceedings of the conference on artificial intelligence (AAAI), pp 255\u2013260"},{"issue":"6","key":"264_CR37","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/32.391377","volume":"21","author":"AM Stavely","year":"1995","unstructured":"Stavely AM (1995) Verifying definite iteration over data structures. IEEE Trans Softw Eng 21(6):506\u2013514","journal-title":"IEEE Trans Softw Eng"},{"key":"264_CR38","unstructured":"SV-COMP 2014\u2014Minutes. http:\/\/sv-comp.sosy-lab.org\/2015\/Minutes-2014.txt . Accessed 6 Feb 2015. No longer available, archived version: https:\/\/web.archive.org\/web\/20150413080431\/ and http:\/\/sv-comp.sosy-lab.org\/2015\/Minutes-2014.txt"},{"key":"264_CR39","doi-asserted-by":"publisher","unstructured":"Tulsian V, Kanade A, Kumar R, Lal A, Nori AV (2014) Mux: algorithm selection for software model checkers. In: Working conference on mining software repositories, pp 132\u2013141","DOI":"10.1145\/2597073.2597080"},{"key":"264_CR40","unstructured":"Verifolio. http:\/\/forsyte.at\/software\/verifolio\/ . Accessed 11 Mar 2016"},{"key":"264_CR41","first-page":"975","volume":"5","author":"TF Wu","year":"2004","unstructured":"Wu TF, Lin CJ, Weng RC (2004) Probability estimates for multi-class classification by pairwise coupling. J Mach Learn Res 5:975\u20131005","journal-title":"J Mach Learn Res"},{"key":"264_CR42","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 HH, Leyton-Brown K (2008) Satzilla: portfolio-based algorithm selection for SAT. J Artif Intell Res (JAIR) 32:565\u2013606","journal-title":"J Artif Intell Res (JAIR)"},{"key":"264_CR43","doi-asserted-by":"publisher","unstructured":"Xu L, Hutter F, Hoos H, Leyton-Brown K (2012) Evaluating component solver contributions to portfolio-based algorithm selectors. In: Cimatti A, Sebastiani R(eds) Proceedings of the theory and applications of satisfiability testing\u2014SAT 2012\u201415th international conference, Trento, Italy, June 17\u201320, 2012, Springer, pp 228\u2013241","DOI":"10.1007\/978-3-642-31612-8_18"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0264-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0264-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0264-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T04:36:23Z","timestamp":1658378183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0264-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,10]]},"references-count":43,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["264"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0264-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1,10]]}}}