{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:30:42Z","timestamp":1742952642036,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031433689"},{"type":"electronic","value":"9783031433696"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Clause sets saturated by hierarchic ordered resolution do not offer a model representation that can be effectively queried, in general. They only offer the guarantee of the existence of a model. We present an effective symbolic model construction for saturated constrained Horn clauses. Constraints are in linear arithmetic, the first-order part is restricted to a function-free language. The model is constructed in finite time, and non-ground clauses can be effectively evaluated with respect to the model. Furthermore, we prove that our model construction produces the least model.<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_8","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"137-155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Model Construction for\u00a0Saturated Constrained Horn Clauses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-2190","authenticated-orcid":false,"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0391-3430","authenticated-orcid":false,"given":"Lorenz","family":"Leutgeb","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84\u201399. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1993. LNCS, vol. 713, pp. 83\u201396. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0022557"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. AAECC 5, 193\u2013212 (1994). https:\/\/doi.org\/10.1007\/BF01190829","journal-title":"AAECC"},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"DA Basin","year":"2001","unstructured":"Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. JACM 48(1), 70\u2013109 (2001). https:\/\/doi.org\/10.1145\/363647.363681","journal-title":"JACM"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: (LIA) - model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 258\u2013273. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_19"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-22102-7_2","volume-title":"Description Logic, Theory Combination, and All That","author":"P Baumgartner","year":"2019","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.-Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 15\u201356. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22102-7_2"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-030-99524-9_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bromberger","year":"2022","unstructured":"Bromberger, M., et al.: A sorted datalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: TACAS 2022. LNCS, vol. 13243, pp. 480\u2013501. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_27"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-86205-3_1","volume-title":"Frontiers of Combining Systems","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Kr\u00f6tzsch, M., Weidenbach, C.: A datalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 3\u201324. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_1"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-030-67067-2_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 511\u2013533. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_23"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Leutgeb, L., Weidenbach, C.: An efficient subsumption test pipeline for BS(LRA) clauses. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 147\u2013168. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_10","DOI":"10.1007\/978-3-031-10769-6_10"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Leutgeb, L., Weidenbach, C.: Symbolic model construction for saturated constrained horn clauses. arXiv (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.05064","DOI":"10.48550\/arXiv.2305.05064"},{"key":"8_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-2653-9","volume-title":"Automated Model Building, APLS","author":"R Caferra","year":"2004","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building, APLS, vol. 31. Springer, Dordrecht (2004). https:\/\/doi.org\/10.1007\/978-1-4020-2653-9"},{"key":"8_CR14","first-page":"91","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91\u201399 (1972)","journal-title":"Mach. Intell."},{"issue":"6","key":"8_CR15","doi-asserted-by":"publisher","first-page":"974","DOI":"10.1017\/S1471068421000211","volume":"22","author":"E De Angelis","year":"2022","unstructured":"De Angelis, E., Fioravanti, F., Gallagher, J.P., Hermenegildo, M.V., Pettorossi, A., Proietti, M.: Analysis and transformation of constrained horn clauses for program verification. TPLP 22(6), 974\u20131042 (2022). https:\/\/doi.org\/10.1017\/S1471068421000211","journal-title":"TPLP"},{"key":"8_CR16","unstructured":"Downey, P.J.: Undecidability of presburger arithmetic with a single monadic predicate letter. Center for Research in Computer Technology, Harvard University, Technical report (1972)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-96145-3_7","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2018","unstructured":"Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 124\u2013143. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_7"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Feferman, S.: Some applications of the notions of forcing and generic sets. Fundamenta Mathematicae. 56(3), 325\u2013345 (1964). http:\/\/eudml.org\/doc\/213821","DOI":"10.4064\/fm-56-3-325-345"},{"issue":"2","key":"8_CR19","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"CG Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Hyperresolution and automated model building. LOGCOM 6(2), 173\u2013203 (1996). https:\/\/doi.org\/10.1093\/logcom\/6.2.173","journal-title":"LOGCOM"},{"issue":"1","key":"8_CR20","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1093\/jigpal\/6.1.17","volume":"6","author":"CG Ferm\u00fcller","year":"1998","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Decision procedures and model building in equational clause logic. IGPL 6(1), 17\u201341 (1998). https:\/\/doi.org\/10.1093\/jigpal\/6.1.17","journal-title":"IGPL"},{"key":"8_CR21","unstructured":"Fiori, A., Weidenbach, C.: SCL with theory constraints. arXiv (2020). http:\/\/arxiv.org\/abs\/2003.04627"},{"issue":"4\u20135","key":"8_CR22","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1017\/S1471068415000204","volume":"15","author":"G Gange","year":"2015","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Horn clauses as an intermediate representation for program analysis and transformation. TPLP 15(4\u20135), 526\u2013542 (2015). https:\/\/doi.org\/10.1017\/S1471068415000204","journal-title":"TPLP"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th LICS, 1999, pp. 295\u2013303. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782624","DOI":"10.1109\/LICS.1999.782624"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416. ACM (2012). https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"8_CR26","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable. arXiv (2017). http:\/\/arxiv.org\/abs\/1703.01212"},{"issue":"20","key":"8_CR27","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. JLP 19(20), 503\u2013581 (1994). https:\/\/doi.org\/10.1016\/0743-1066(94)90033-7","journal-title":"JLP"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223\u2013237. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19"},{"key":"8_CR30","unstructured":"Kruglov, E.: Superposition modulo theory. Ph.D. thesis, Saarland University (2013). http:\/\/scidok.sulb.uni-saarland.de\/volltexte\/2013\/5559\/"},{"key":"8_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"JW Lloyd","year":"1987","unstructured":"Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Cham (1987). https:\/\/doi.org\/10.1007\/978-3-642-83189-8","edition":"2"},{"issue":"5","key":"8_CR32","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993). https:\/\/doi.org\/10.1093\/comjnl\/36.5.450","journal-title":"Comput. J."},{"issue":"2","key":"8_CR33","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1017\/S1471068418000042","volume":"18","author":"P L\u00f3pez-Garc\u00eda","year":"2018","unstructured":"L\u00f3pez-Garc\u00eda, P., Darmawan, L., Klemen, M., Liqat, U., Bueno, F., Hermenegildo, M.V.: Interval-based resource usage verification by translation into horn clauses and an application to energy consumption. TPLP 18(2), 167\u2013223 (2018). https:\/\/doi.org\/10.1017\/S1471068418000042","journal-title":"TPLP"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-08867-9_16","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2014","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 243\u2013259. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_16"},{"issue":"5","key":"8_CR35","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1017\/S1471068420000216","volume":"20","author":"F Mesnard","year":"2020","unstructured":"Mesnard, F., Payet, \u00c9., Vidal, G.: Concolic testing in CLP. TPLP 20(5), 671\u2013686 (2020). https:\/\/doi.org\/10.1017\/S1471068420000216","journal-title":"TPLP"},{"issue":"3","key":"8_CR36","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"DC Oppen","year":"1978","unstructured":"Oppen, D.C.: A 2 $$\\hat{}$$ 2 $$\\hat{}$$ 2 $$\\hat{}$$PN upper bound on the complexity of Presburger arithmetic. JCSS 16(3), 323\u2013332 (1978). https:\/\/doi.org\/10.1016\/0022-0000(78)90021-1","journal-title":"JCSS"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"issue":"3","key":"8_CR38","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1709093.1709095","volume":"32","author":"F Spoto","year":"2010","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyzer for java bytecode based on path-length. TOPLAS 32(3), 8:1-8:70 (2010). https:\/\/doi.org\/10.1145\/1709093.1709095","journal-title":"TOPLAS"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955). https:\/\/doi.org\/10.2140\/pjm.1955.5.285","DOI":"10.2140\/pjm.1955.5.285"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-23506-6_12","volume-title":"Correct System Design","author":"C Weidenbach","year":"2015","unstructured":"Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 172\u2013188. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23506-6_12"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43369-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:34:24Z","timestamp":1694702064000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}