{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:59:47Z","timestamp":1740099587439,"version":"3.37.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030349677"},{"type":"electronic","value":"9783030349684"}],"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-34968-4_15","type":"book-chapter","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:14:54Z","timestamp":1574363694000},"page":"265-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Embedding SMT-LIB into B for Interactive Proof and Constraint Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-9798","authenticated-orcid":false,"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"15_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J-R Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588\u2013605. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11901433_32"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45648-1_13","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J-R Abrial","year":"2002","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 242\u2013269. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45648-1_13"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20\u201323. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11513988_4"},{"key":"15_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Tech. rep., Department of Computer Science, The University of Iowa (2015). \nwww.SMT-LIB.org"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116\u2013130. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22438-6_11"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"issue":"2","key":"15_CR10","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/128861.128862","volume":"14","author":"RT Boute","year":"1992","unstructured":"Boute, R.T.: The Euclidean definition of the functions div and mod. ACM Trans. Program. Lang. Syst. 14(2), 127\u2013144 (1992)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-46508-1_8","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D Cantone","year":"2000","unstructured":"Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 126\u2013136. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/3-540-46508-1_8"},{"key":"15_CR14","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). \nhttps:\/\/doi.org\/10.1007\/BFb0033845"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"15_CR16","unstructured":"ClearSy: Atelier B 4.1 Release Notes. Aix-en-Provence, France (2009). \nhttp:\/\/www.atelierb.eu\/"},{"issue":"3","key":"15_CR17","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"15_CR18","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-30885-7_14"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-662-43652-3_26","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Delahaye","year":"2014","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The BWare project: building a proof platform for the automated verification of B proof obligations. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 290\u2013293. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_26"},{"issue":"4-5","key":"15_CR21","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1017\/S1471068412000208","volume":"12","author":"GREGORY J. DUCK","year":"2012","unstructured":"Duck, G.J.: SMCHR: satisfiability modulo constraint handling rules. CoRR, abs\/1210.5307 (2012)","journal-title":"Theory and Practice of Logic Programming"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"issue":"2","key":"15_CR23","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D D\u00e9harbe","year":"2014","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94(2), 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"key":"15_CR24","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: Proceedings SMT Workshop, pp. 6\u201315 (2013)"},{"issue":"1\u20133","key":"15_CR25","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0743-1066(98)10005-5","volume":"37","author":"T Fr\u00fchwirth","year":"1998","unstructured":"Fr\u00fchwirth, T.: Theory and practice of constraint handling rules. J. Logic Program. 37(1\u20133), 95\u2013138 (1998)","journal-title":"J. Logic Program."},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27813-9_14"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-30729-4_3","volume-title":"Integrated Formal Methods","author":"D Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA$$^+$$ to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-30729-4_3"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10705424","volume-title":"Functional and Logic Programming","year":"1999","unstructured":"Middeldorp, A., Sato, T. (eds.): FLOPS 1999. LNCS, vol. 1722. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/10705424"},{"key":"15_CR29","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tcs.2012.02.024","volume":"435","author":"JM Howe","year":"2012","unstructured":"Howe, J.M., King, A.: A pearl on SAT and SMT solving in prolog. Theor. Comput. Sci. 435, 43\u201355 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR30","volume-title":"The art of computer programming, volume 1: Fundamental Algorithms","author":"DE Knuth","year":"1997","unstructured":"Knuth, D.E.: The art of computer programming, volume 1: Fundamental Algorithms, vol. 1. Addison Wesley Longman Publishing Co., Inc., Redwood City (1997)"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Reger, G., Voronkov, A.: The vampire and the FOOL. In: Proceedings CPP, CPP 2016, pp. 37\u201348. ACM (2016)","DOI":"10.1145\/2854065.2854071"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-20615-8_5","volume-title":"Intelligent Computer Mathematics","author":"E Kotelnikov","year":"2015","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Voronkov, A.: A first class boolean sort in first-order theorem proving and TPTP. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 71\u201386. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-20615-8_5"},{"key":"15_CR33","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33693-0_23"},{"key":"15_CR34","doi-asserted-by":"crossref","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 (2014)","DOI":"10.1002\/9781119002727.ch14"},{"issue":"5","key":"15_CR35","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-10373-5_25","volume-title":"Formal Methods and Software Engineering","author":"PJ Matos","year":"2009","unstructured":"Matos, P.J., Fischer, B., Marques-Silva, J.: A lazy unbounded model checker for Event-B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 485\u2013503. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-10373-5_25"},{"key":"15_CR37","unstructured":"Reger, G., Suda, M., Voronkov, A.: Instantiation and pretending to be an SMT solver with vampire. In: Proceedings SMT Workshop (2012)"},{"key":"15_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-19249-9_30","volume-title":"FM 2015: Formal Methods","author":"D Schneider","year":"2015","unstructured":"Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487\u2013495. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_30"},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"15_CR40","unstructured":"Weissenbacher, G., Kr\u00f6ning, D., R\u00fcmmer, P.: A proposal for a theory of finite sets, lists, and maps for the SMT-Lib standard. In: Proceedings SMT Workshop (2009)"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Witulski, J., Leuschel, M.: Checking computations of formal method tools - a secondary toolchain for ProB. In: Proceedings F-IDE, vol. 149, EPTCS. Electronic Proceedings in Theoretical Computer Science (2014)","DOI":"10.4204\/EPTCS.149.9"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:18:30Z","timestamp":1574363910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_15","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":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","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":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}