{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:52Z","timestamp":1746115852695,"version":"3.40.4"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031908965"},{"type":"electronic","value":"9783031908972"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware- and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order theories such as linear rational arithmetic. What about their applicability in the quantitative setting where formulae evaluate to numbers and quantitative supremum\/infimum quantifiers are the natural pendant to traditional Boolean quantifiers? Applications include establishing quantitative properties of programs such as bounds on expected outcomes of probabilistic programs featuring unbounded non-determinism and analyzing the flow of information through programs.<\/jats:p>\n          <jats:p>In this paper, we present the - to the best of our knowledge - first QE algorithm for possibly unbounded, <jats:inline-formula>\n              <jats:tex-math>$$\\infty $$<\/jats:tex-math>\n            <\/jats:inline-formula>- or <jats:inline-formula>\n              <jats:tex-math>$$(-\\infty )$$<\/jats:tex-math>\n            <\/jats:inline-formula>-valued, or discontinuous <jats:italic>piecewise linear quantities<\/jats:italic>. They are the quantitative counterpart to linear rational arithmetic, and are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper space complexity bounds. Moreover, our algorithm yields a quantitative CI theorem: Given arbitrary piecewise linear quantities <jats:inline-formula>\n              <jats:tex-math>$$f,g$$<\/jats:tex-math>\n            <\/jats:inline-formula> with <jats:inline-formula>\n              <jats:tex-math>$$f\\models g$$<\/jats:tex-math>\n            <\/jats:inline-formula>, both the strongest and the weakest Craig interpolant of <jats:inline-formula>\n              <jats:tex-math>$$f$$<\/jats:tex-math>\n            <\/jats:inline-formula> and <jats:inline-formula>\n              <jats:tex-math>$$g$$<\/jats:tex-math>\n            <\/jats:inline-formula> are quantifier-free and effectively constructible.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_9","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:02Z","timestamp":1746001082000},"page":"176-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantifier Elimination and Craig Interpolation: The Quantitative Way"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nora","family":"Orhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 313\u2013329. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: LPAR. Lecture Notes in Computer Science, vol.\u00a07180, pp. 46\u201361. Springer (2012)","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"9_CR3","unstructured":"Aliprantis, C., Burkinshaw, O.: Principles of Real Analysis. North Holland (1981)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Baaz, M., Veith, H.: Quantifier elimination in fuzzy logic. In: CSL. Lecture Notes in Computer Science, vol.\u00a01584, pp. 399\u2013414. Springer (1998)","DOI":"10.1007\/10703163_27"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: TACAS (2). Lecture Notes in Computer Science, vol. 13994, pp. 410\u2013429. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, J., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 524\u2013549. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Batz, K., Gallus, A., Kaminski, B.L., Katoen, J.P., Winkler, T.: Weighted programming: a programming paradigm for specifying mathematical models. Proc. ACM Program. Lang. 6(OOPSLA1) (2022)","DOI":"10.1145\/3527310"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021)","DOI":"10.1145\/3434320"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C., Noll, T.: Quantitative separation logic: A logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang. 3(POPL), 34:1\u201334:29 (2019)","DOI":"10.1145\/3290347"},{"key":"9_CR10","unstructured":"Batz, K., Katoen, J.P., Orhan, N.: Quantifier elimination and craig interpolation: The quantitative way (technical report) (2025), https:\/\/arxiv.org\/abs\/2501.15156"},{"key":"9_CR11","unstructured":"Beyer, D., Lee, N., Wendler, P.: Interpolation and sat-based model checking revisited: Adoption to software verification. CoRR abs\/2208.05046 (2022)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Britikov, K., Blicha, M., Sharygina, N., Fedyukovich, G.: Reachability analysis for multiloop programs using transition power abstraction. In: FM (1). Lecture Notes in Computer Science, vol. 14933, pp. 558\u2013576. Springer (2024)","DOI":"10.1007\/978-3-031-71162-6_29"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"ten Cate, B., Comer, J.: Craig interpolation for decidable first-order fragments. In: FoSSaCS (2). Lecture Notes in Computer Science, vol. 14575, pp. 137\u2013159. Springer (2024)","DOI":"10.1007\/978-3-031-57231-9_7"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 511\u2013526. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N.: NIL: learning nonlinear interpolants. In: CADE. Lecture Notes in Computer Science, vol. 11716, pp. 178\u2013196. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_11"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol.\u00a033, pp. 134\u2013183. Springer (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: CAV. Lecture Notes in Computer Science, vol.\u00a02725, pp. 420\u2013432. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"9_CR18","unstructured":"Cooper, D.: Theorem proving in arithmetic without multiplication. Machine Intelligence (1972)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic 22(3), 269\u2013285 (1957)","DOI":"10.2307\/2963594"},{"key":"9_CR20","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science, Springer (1990)","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: OOPSLA. pp. 443\u2013456. ACM (2013)","DOI":"10.1145\/2509136.2509511"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: TACAS. Lecture Notes in Computer Science, vol.\u00a03920, pp. 489\u2013503. Springer (2006)","DOI":"10.1007\/11691372_35"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. J. Satisf. Boolean Model. Comput. 5(1-4), 27\u201356 (2008)","DOI":"10.3233\/SAT190051"},{"key":"9_CR25","unstructured":"Fourier, J.: Analyse des travaux de l\u2019Acad\u00e9mie royale des sciences pendant l\u2019ann\u00e9e 1824: rapport lu dans la s\u00e9ance publique de l\u2019Institut le 24 avril 1825. Partie math\u00e9matique. Institut (Paris), Institut royal de France (1825)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In: IJCAR. Lecture Notes in Computer Science, vol.\u00a09706, pp. 195\u2013212. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_14"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Gretz, F., Katoen, J., McIver, A.: Prinsys - on a quest for probabilistic loop invariants. In: QEST. Lecture Notes in Computer Science, vol.\u00a08054, pp. 193\u2013208. Springer (2013)","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL. pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: TACAS. Lecture Notes in Computer Science, vol.\u00a03920, pp. 459\u2013473. Springer (2006)","DOI":"10.1007\/11691372_33"},{"key":"9_CR30","unstructured":"Kaminski, B.L.: Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph.D. thesis, RWTH Aachen University, Germany (2019)"},{"key":"9_CR31","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications (2005)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. p. 105-116. SIGSOFT \u201906\/FSE-14, ACM (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: - automated support for proof-based methods. In: SAS. Lecture Notes in Computer Science, vol.\u00a06337, pp. 390\u2013406. Springer (2010)","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Knuth, D.E.: Two notes on notation. The American Mathematical Monthly 99(5), 403\u2013422 (1992)","DOI":"10.1080\/00029890.1992.11995869"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 17\u201334. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","DOI":"10.1007\/s10703-016-0249-4"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. In: STOC. pp. 291\u2013297. ACM (1983)","DOI":"10.1145\/800061.808758"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985)","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Krishnan, H.G.V., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: CAV (2). Lecture Notes in Computer Science, vol. 11562, pp. 367\u2013385. Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_21"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993)","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Mahdi, A., Fr\u00e4nzle, M.: Generalized Craig interpolation for stochastic satisfiability modulo theory problems. In: RP. Lecture Notes in Computer Science, vol.\u00a08762, pp. 203\u2013215. Springer (2014)","DOI":"10.1007\/978-3-319-11439-2_16"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: CAV. Lecture Notes in Computer Science, vol.\u00a02725, pp. 1\u201313. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV. Lecture Notes in Computer Science, vol.\u00a04144, pp. 123\u2013136. Springer (2006)","DOI":"10.1007\/11817963_14"},{"key":"9_CR45","unstructured":"Motzkin, T.: Beitraege zur Theorie der linearen Ungleichungen. Universitaet Basel (1936)"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR47","unstructured":"M\u00fcller, P.: Building Deductive Program Verifiers - Lecture Notes. Engineering Secure and Dependable Software Systems (2019)"},{"key":"9_CR48","doi-asserted-by":"crossref","unstructured":"Nalbach, J., Promies, V., \u00c1brah\u00e1m, E., Kobialka, P.: Fmplex: A novel method for solving linear real arithmetic problems. In: GandALF. EPTCS, vol.\u00a0390, pp. 16\u201332 (2023)","DOI":"10.4204\/EPTCS.390.2"},{"key":"9_CR49","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: PLDI. pp. 496\u2013512. ACM (2018)","DOI":"10.1145\/3192366.3192394"},{"key":"9_CR50","unstructured":"Sanner, S., Delgado, K.V., de\u00a0Barros, L.N.: Symbolic dynamic programming for discrete and continuous state MDPs. In: UAI. pp. 643\u2013652. AUAI Press (2011)"},{"key":"9_CR51","doi-asserted-by":"crossref","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052\u20132082 (2023)","DOI":"10.1145\/3622870"},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Haifa Verification Conference. Lecture Notes in Computer Science, vol.\u00a07261, pp. 160\u2013175. Springer (2011)","DOI":"10.1007\/978-3-642-34188-5_15"},{"key":"9_CR53","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: FMCAD. pp. 114\u2013121. IEEE (2012)"},{"key":"9_CR54","unstructured":"Still, G.: Lectures on parametric optimization: An introduction (2018)"},{"key":"9_CR55","doi-asserted-by":"crossref","unstructured":"Tavana, N., Pourmahdian, M., Khatami, S.A.: The Craig interpolation property in first-order G\u00f6del logic. Fuzzy Sets Syst. 485, 108958 (2024)","DOI":"10.1016\/j.fss.2024.108958"},{"key":"9_CR56","doi-asserted-by":"crossref","unstructured":"Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 260\u2013276. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"9_CR57","doi-asserted-by":"crossref","unstructured":"Wu, H., Wang, J., Xia, B., Li, X., Zhan, N., Gan, T.: Nonlinear Craig interpolant generation over unbounded domains by separating semialgebraic sets. In: FM (1). Lecture Notes in Computer Science, vol. 14933, pp. 92\u2013110. Springer (2024)","DOI":"10.1007\/978-3-031-71162-6_5"},{"key":"9_CR58","unstructured":"Yang, T., Fu, H., Ke, J., Zhan, N., Wu, S.: Piecewise linear expectation analysis via k-induction for probabilistic programs. CoRR abs\/2403.17567 (2024)"},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Zhang, L., Kaminski, B.L.: Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. Proc. ACM Program. Lang. 6(OOPSLA1) (2022)","DOI":"10.1145\/3527331"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:36Z","timestamp":1746001116000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}