{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:34:52Z","timestamp":1762324492381,"version":"3.37.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_9","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:03:25Z","timestamp":1558998205000},"page":"130-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Automated Backend Selection for ProB Using Deep Learning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-5554","authenticated-orcid":false,"given":"Jannik","family":"Dunkelau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-9798","authenticated-orcid":false,"given":"Sebastian","family":"Krings","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8842-2993","authenticated-orcid":false,"given":"Joshua","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR2","unstructured":"Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (2012)"},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"R Back","year":"1981","unstructured":"Back, R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49\u201368 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR4","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroc\u0142aw, pp. 53\u201364, August 2011. https:\/\/hal.inria.fr\/hal-00790310"},{"issue":"1","key":"9_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L.: Random forests. Mach. Learn. 45(1), 5\u201332 (2001)","journal-title":"Mach. Learn."},{"key":"9_CR6","unstructured":"Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and regression trees (1984)"},{"key":"9_CR7","unstructured":"Bridge, J.P.: Machine learning and automated theorem proving. Technical report, University of Cambridge, Computer Laboratory (2010)"},{"issue":"3\u20134","key":"9_CR8","first-page":"221","volume":"22","author":"D Cansell","year":"2012","unstructured":"Cansell, D., M\u00e9ry, D.: Foundations of the B method. Comput. Inform. 22(3\u20134), 221\u2013256 (2012)","journal-title":"Comput. Inform."},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"M Carlsson","year":"1997","unstructured":"Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191\u2013206. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0033845"},{"key":"9_CR10","volume-title":"SICStus Prolog User\u2019s Manual","author":"M Carlsson","year":"1988","unstructured":"Carlsson, M., et al.: SICStus Prolog User\u2019s Manual, vol. 3. Swedish Institute of Computer Science Kista, Sweden (1988)"},{"key":"9_CR11","unstructured":"ClearSy: Atelier B, user and reference manuals. Aix-en-Provence, France (2016). http:\/\/www.atelierb.eu\/"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"9_CR14","volume-title":"Foundations of Set Theory","author":"AA Fraenkel","year":"1973","unstructured":"Fraenkel, A.A., Bar-Hillel, Y., Levy, A.: Foundations of Set Theory, vol. 67. Elsevier, Burlington (1973)"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/BF01457986","volume":"86","author":"A Fraenkel","year":"1922","unstructured":"Fraenkel, A.: Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre. Mathematische Annalen 86(3), 230\u2013237 (1922)","journal-title":"Mathematische Annalen"},{"key":"9_CR16","unstructured":"Goller, C.: Learning search-control heuristics for automated deduction systems with folding architecture networks. In: ESANN, pp. 45\u201350 (1999)"},{"key":"9_CR17","unstructured":"Goller, C., Kuchler, A.: Learning task-dependent distributed representations by backpropagation through structure. In: Proceedings of International Conference on Neural Networks (ICNN 1996), vol. 1, pp. 347\u2013352. IEEE (1996)"},{"key":"9_CR18","volume-title":"Deep Learning","author":"I Goodfellow","year":"2016","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016). http:\/\/www.deeplearningbook.org"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-540-31865-1_25","volume-title":"Advances in Information Retrieval","author":"C Goutte","year":"2005","unstructured":"Goutte, C., Gaussier, E.: A probabilistic interpretation of precision, recall and F-score, with implication for evaluation. In: Losada, D.E., Fern\u00e1ndez-Luna, J.M. (eds.) ECIR 2005. LNCS, vol. 3408, pp. 345\u2013359. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31865-1_25"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Healy, A.: Predicting SMT solver performance for software verification. Master\u2019s thesis, National University of Ireland Maynooth (2016)","DOI":"10.4204\/EPTCS.240.2"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Healy, A., Monahan, R., Power, J.F.: Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, SAC 2016, pp. 1558\u20131561. ACM, New York (2016)","DOI":"10.1145\/2851613.2851975"},{"key":"9_CR22","unstructured":"Japkowicz, N.: The class imbalance problem: Significance and strategies. In: Proceedings of the International Conference on Artificial Intelligence (2000)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-22969-0_15","volume-title":"Software Engineering and Formal Methods","author":"S Krings","year":"2015","unstructured":"Krings, S., Bendisposto, J., Leuschel, M.: From failure to proof: the ProB disprover for B and Event-B. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 199\u2013214. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_15"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-33693-0_23","volume-title":"Integrated Formal Methods","author":"S Krings","year":"2016","unstructured":"Krings, S., Leuschel, M.: SMT solvers for validation of B and Event-B models. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361\u2013375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_23"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-91271-4_6","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"S Krings","year":"2018","unstructured":"Krings, S., Schmidt, J., Brings, C., Frappier, M., Leuschel, M.: A translation from alloy to B. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 71\u201386. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_6"},{"key":"9_CR26","unstructured":"Kubat, M., Matwin, S., et al.: Addressing the curse of imbalanced training sets: one-sided selection. In: ICML, Nashville, USA, vol. 97, pp. 179\u2013186 (1997)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"LeCun, Y., Kavukcuoglu, K., Farabet, C.: Convolutional networks and applications in vision. In: Proceedings of 2010 IEEE International Symposium on Circuits and Systems (ISCAS), pp. 253\u2013256. IEEE (2010)","DOI":"10.1109\/ISCAS.2010.5537907"},{"issue":"2","key":"9_CR28","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: Setheo: a high-performance theorem prover. J. Autom. Reasoning 8(2), 183\u2013212 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"9_CR29","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1002\/9781119002727.ch14","volume-title":"Formal Methods Applied to Complex Systems: Implementation of the B Method","author":"M Leuschel","year":"2014","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the ProB constraint solver 10 years on. In: Boulanger, J.L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 427\u2013446. Wiley ISTE, Hoboken (2014). Chapter 14"},{"issue":"2","key":"9_CR30","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/B978-1-55860-335-6.50026-X","volume-title":"Machine Learning Proceedings 1994","author":"David D. Lewis","year":"1994","unstructured":"Lewis, D.D., Catlett, J.: Heterogeneous uncertainty sampling for supervised learning. In: Proceedings of the Eleventh International Conference on Machine Learning, pp. 148\u2013156 (1994)"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Loreggia, A., Malitsky, Y., Samulowitz, H., Saraswat, V.A.: Deep Learning for Algorithm Portfolios. In: AAAI, pp. 1280\u20131286 (2016)","DOI":"10.1609\/aaai.v30i1.10170"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-32759-9_31","volume-title":"FM 2012: Formal Methods","author":"D Plagge","year":"2012","unstructured":"Plagge, D., Leuschel, M.: Validating B,Z and TLA $$^{+}$$ Using ProB\u00a0and Kodkod. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372\u2013386. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_31"},{"issue":"1","key":"9_CR35","first-page":"81","volume":"1","author":"JR Quinlan","year":"1986","unstructured":"Quinlan, J.R.: Induction of decision trees. Mach. Learn. 1(1), 81\u2013106 (1986)","journal-title":"Mach. Learn."},{"issue":"6","key":"9_CR36","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1037\/h0042519","volume":"65","author":"F Rosenblatt","year":"1958","unstructured":"Rosenblatt, F.: The perceptron: a probabilistic model for information storage and organization in the brain. Psychol. Rev. 65(6), 386 (1958)","journal-title":"Psychol. Rev."},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Rosenblatt, F.: Principles of neurodynamics. perceptrons and the theory of brain mechanisms. Technical report, Cornell Aeronautical Lab, Inc., Buffalo, NY (1961)","DOI":"10.21236\/AD0256582"},{"issue":"6088","key":"9_CR38","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1038\/323533a0","volume":"323","author":"D Rumelhart","year":"1986","unstructured":"Rumelhart, D., Hinton, G., Williams, R.: Learning representations by back-propagating errors. Nature 323(6088), 533\u2013538 (1986)","journal-title":"Nature"},{"issue":"2, 3","key":"9_CR39","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E-A Brainiac theorem prover. AI Commun. 15(2, 3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1015","DOI":"10.1007\/11941439_114","volume-title":"AI 2006: Advances in Artificial Intelligence","author":"M Sokolova","year":"2006","unstructured":"Sokolova, M., Japkowicz, N., Szpakowicz, S.: Beyond accuracy, F-score and ROC: a family of discriminant measures for performance evaluation. In: Sattar, A., Kang, B. (eds.) AI 2006. LNCS (LNAI), vol. 4304, pp. 1015\u20131021. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11941439_114"},{"key":"9_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"},{"issue":"1","key":"9_CR42","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1109\/4235.585893","volume":"1","author":"DH Wolpert","year":"1997","unstructured":"Wolpert, D.H., Macready, W.G.: No free lunch theorems for optimization. IEEE Trans. Evol. Comput. 1(1), 67\u201382 (1997)","journal-title":"IEEE Trans. Evol. Comput."},{"key":"9_CR43","unstructured":"Wolpert, D.H., Macready, W.G., et al.: No free lunch theorems for search. Technical Report SFI-TR-95-02-010, Santa Fe Institute (1995)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T23:06:41Z","timestamp":1694905601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}