{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:04Z","timestamp":1784675044890,"version":"3.55.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"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><jats:p>Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_5","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"92-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Nonlinear Craig Interpolant Generation Over\u00a0Unbounded Domains by\u00a0Separating Semialgebraic Sets"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9368-4744","authenticated-orcid":false,"given":"Hao","family":"Wu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9681-1451","authenticated-orcid":false,"given":"Jie","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2570-2338","authenticated-orcid":false,"given":"Bican","family":"Xia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1663-1287","authenticated-orcid":false,"given":"Xiakun","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4880-5129","authenticated-orcid":false,"given":"Ting","family":"Gan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"issue":"3","key":"5_CR1","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1090\/S0894-0347-99-00302-1","volume":"12","author":"F Acquistapace","year":"1999","unstructured":"Acquistapace, F., Andradas, C., Broglia, F.: Separation of semialgebraic sets. J. Am. Math. Soc. 12(3), 703\u2013728 (1999). https:\/\/doi.org\/10.1090\/S0894-0347-99-00302-1","journal-title":"J. Am. Math. Soc."},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-1-4757-3216-0_8","volume-title":"High Performance Optimization","author":"ED Andersen","year":"2000","unstructured":"Andersen, E.D., Andersen, K.D.: The Mosek interior point optimizer for linear programming: an implementation of the homogeneous algorithm. In: Frenk, H., Roos, K., Terlaky, T., Zhang, S. (eds.) High Performance Optimization, pp. 197\u2013232. Springer US, Boston, MA (2000). https:\/\/doi.org\/10.1007\/978-1-4757-3216-0_8"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol.\u00a02, pp. 571\u2013603 (2006). https:\/\/doi.org\/10.1016\/S1574-6526(06)80020-9","DOI":"10.1016\/S1574-6526(06)80020-9"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-030-29436-6_11","volume-title":"Automated Deduction \u2013 CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings","author":"M Chen","year":"2019","unstructured":"Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N.: NIL: learning nonlinear interpolants. In: Fontaine, P. (ed.) Automated Deduction \u2013 CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27\u201330, 2019, Proceedings, pp. 178\u2013196. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_11"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolation generation in satisfiability modulo theories. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. Lecture Notes in Computer Science, vol.\u00a04963, pp. 397\u2013412 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_30","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1\u201319:52 (2018). https:\/\/doi.org\/10.1145\/3230639","DOI":"10.1145\/3230639"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013. Lecture Notes in Computer Science, vol.\u00a08044, pp. 364\u2013380. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_25","DOI":"10.1007\/978-3-642-39799-8_25"},{"issue":"1\u20132","key":"5_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\u20132), 29\u201335 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80004-X","journal-title":"J. Symb. Comput."},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"D\u2019Silva, V.V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010. Lecture Notes in Computer Science, vol.\u00a05944, pp. 129\u2013145. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-11319-2_12","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In: Automated Reasoning: 8th International Joint Conference, IJCAR 2016, pp. 195\u2013212. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_14","DOI":"10.1007\/978-3-319-40229-1_14"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Gan, T., Xia, B., Xue, B., Zhan, N., Dai, L.: Nonlinear Craig interpolant generation. In: Computer Aided Verification - 32nd International Conference, CAV 2020. Lecture Notes in Computer Science, vol. 12224, pp. 415\u2013438. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_20","DOI":"10.1007\/978-3-030-53288-8_20"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Proof generation from delta-decisions. In: 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, pp. 156\u2013163. IEEE Computer Society (2014). https:\/\/doi.org\/10.1109\/SYNASC.2014.29","DOI":"10.1109\/SYNASC.2014.29"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Gao, S., Zufferey, D.: Interpolants in nonlinear theories over the reals. In: Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Lecture Notes in Computer Science, vol.\u00a09636, pp. 625\u2013641. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_41","DOI":"10.1007\/978-3-662-49674-9_41"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 232\u2013244. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Hoenicke, J., Schindler, T.: Efficient interpolation for the theory of arrays. In: Automated Reasoning - 9th International Joint Conference, IJCAR 2018. Lecture Notes in Computer Science, vol. 10900, pp. 549\u2013565. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_36","DOI":"10.1007\/978-3-319-94205-6_36"},{"key":"5_CR16","unstructured":"Huang, L., Kang, S., Wang, J., Yang, H.: Sparse polynomial optimization with unbounded sets (2024). https:\/\/arxiv.org\/abs\/2401.15837"},{"issue":"1","key":"5_CR17","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/S10107-022-01878-5","volume":"200","author":"L Huang","year":"2023","unstructured":"Huang, L., Nie, J., Yuan, Y.: Homogenization for polynomial optimization with unbounded sets. Math. Program. 200(1), 105\u2013145 (2023). https:\/\/doi.org\/10.1007\/S10107-022-01878-5","journal-title":"Math. Program."},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Dutertre, B.: Interpolation and model checking for nonlinear arithmetic. In: Computer Aided Verification - 33rd International Conference, CAV 2021. Lecture Notes in Computer Science, vol. 12760, pp. 266\u2013288. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_13","DOI":"10.1007\/978-3-030-81688-9_13"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Jung, Y., Lee, W., Wang, B., Yi, K.: Predicate generation for learning-based quantifier-free loop invariant inference. In: Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011. Lecture Notes in Computer Science, vol.\u00a06605, pp. 205\u2013219. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_17","DOI":"10.1007\/978-3-642-19835-9_17"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, pp. 105\u2013116. ACM (2006). https:\/\/doi.org\/10.1145\/1181775.1181789","DOI":"10.1145\/1181775.1181789"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Computer Aided Verification - 26th International Conference, CAV 2014. Lecture Notes in Computer Science, vol.\u00a08559, pp. 17\u201334. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: 22nd International Conference on Automated Deduction, CADE\u201922. Lecture Notes in Computer Science, vol.\u00a05663, pp. 199\u2013213. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_17","DOI":"10.1007\/978-3-642-02959-2_17"},{"issue":"2","key":"5_CR23","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00edcek","year":"1997","unstructured":"Kraj\u00edcek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457\u2013486 (1997). https:\/\/doi.org\/10.2307\/2275541","journal-title":"J. Symb. Log."},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) Formal Modeling and Analysis of Timed Systems - 9th International Conference, FORMATS 2011. Lecture Notes in Computer Science, vol.\u00a06919, pp. 240\u2013255. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_17","DOI":"10.1007\/978-3-642-24310-3_17"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Lasserre, J.B.: Moments, positive polynomials and their applications, vol.\u00a01. World Scientific (2009). https:\/\/doi.org\/10.1142\/p665","DOI":"10.1142\/p665"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Lin, S., Sun, J., Xiao, H., San\u00e1n, D., Hansen, H.: Fib: Squeezing loop invariants by interpolation between forward\/backward predicate transformers. In: Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, pp. 793\u2013803. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115690","DOI":"10.1109\/ASE.2017.8115690"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Lin, W., Ding, M., Lin, K., Mei, G., Ding, Z.: Formal synthesis of neural Craig interpolant via counterexample guided deep learning. In: 9th International Conference on Dependable Systems and Their Applications, DSA 2022, pp. 116\u2013125. IEEE (2022). https:\/\/doi.org\/10.1109\/DSA56465.2022.00023","DOI":"10.1109\/DSA56465.2022.00023"},{"key":"5_CR28","unstructured":"Magron, V., Wang, J.: TSSOS: a Julia library to exploit sparsity for large-scale polynomial optimization. CoRR abs\/2103.00915 (2021). https:\/\/arxiv.org\/abs\/2103.00915"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Magron, V., Wang, J.: Sparse Polynomial Optimization - Theory and Practice, Series on Optimization and its Applications, vol.\u00a05. WorldScientific (2023). https:\/\/doi.org\/10.1142\/Q0382","DOI":"10.1142\/Q0382"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Marshall, M.: Positive polynomials and sums of squares. Am. Math. Soc., 146 (2008)","DOI":"10.1090\/surv\/146"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Computer Aided Verification, 15th International Conference, CAV 2003. Lecture Notes in Computer Science, vol.\u00a02725, pp. 1\u201313. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"issue":"1","key":"5_CR32","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/J.TCS.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005). https:\/\/doi.org\/10.1016\/J.TCS.2005.07.003","journal-title":"Theor. Comput. Sci."},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. Lecture Notes in Computer Science, vol.\u00a04963, pp. 413\u2013427. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_31","DOI":"10.1007\/978-3-540-78800-3_31"},{"issue":"1\u20132","key":"5_CR34","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/S10107-013-0680-X","volume":"146","author":"J Nie","year":"2014","unstructured":"Nie, J.: Optimality conditions and finite convergence of Lasserre\u2019s hierarchy. Math. Program. 146(1\u20132), 97\u2013121 (2014). https:\/\/doi.org\/10.1007\/S10107-013-0680-X","journal-title":"Math. Program."},{"issue":"3","key":"5_CR35","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981\u2013998 (1997). https:\/\/doi.org\/10.2307\/2275583","journal-title":"J. Symb. Log."},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J. 42(3), 969\u2013984 (1993). https:\/\/www.jstor.org\/stable\/24897130","DOI":"10.1512\/iumj.1993.42.42045"},{"issue":"2","key":"5_CR37","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/s10703-017-0302-y","volume":"53","author":"P Roux","year":"2018","unstructured":"Roux, P., Voronin, Y., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. Formal Methods Syst. Design 53(2), 286\u2013312 (2018). https:\/\/doi.org\/10.1007\/s10703-017-0302-y","journal-title":"Formal Methods Syst. Design"},{"issue":"11","key":"5_CR38","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.1016\/J.JSC.2010.06.005","volume":"45","author":"A Rybalchenko","year":"2010","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. J. Symb. Comput. 45(11), 1212\u20131233 (2010). https:\/\/doi.org\/10.1016\/J.JSC.2010.06.005","journal-title":"J. Symb. Comput."},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Log. Methods Comput. Sci. 4(4) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(4:1)2008","DOI":"10.2168\/LMCS-4(4:1)2008"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Srikanth, A., Sahin, B., Harris, W.R.: Complexity verification using guided theorem enumeration, pp. 639\u2013652 (2017). https:\/\/doi.org\/10.1145\/3009837.3009864","DOI":"10.1145\/3009837.3009864"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Ann. Math. 207, 87\u201397 (1974). https:\/\/doi.org\/10.1007\/BF01362149","DOI":"10.1007\/BF01362149"},{"key":"5_CR42","unstructured":"Wu, H., Wang, J., Xia, B., Li, X., Zhan, N., Gan, T.: Nonlinear Craig interpolant generation over unbounded domains by separating semialgebraic sets (2024). https:\/\/arxiv.org\/abs\/2407.00625"},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: 20th International Conference on Automated Deduction, CADE\u201920. Lecture Notes in Computer Science, vol.\u00a03632, pp. 353\u2013368. Springer (2005). https:\/\/doi.org\/10.1007\/11532231_26","DOI":"10.1007\/11532231_26"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Zhan, N., Wang, S., Zhao, H.: Formal Verification of Simulink\/Stateflow Diagrams. A Deductive Approach. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-47016-0","DOI":"10.1007\/978-3-319-47016-0"},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"Zhao, H., Zhan, N., Kapur, D., Larsen, K.G.: A \u201chybrid\u201d approach for synthesizing optimal controllers of hybrid systems: a case study of the oil pump industrial example. In: Formal Methods - 18th International Symposium, FM 2012, Lecture Notes in Computer Science, vol.\u00a07436, pp. 471\u2013485. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_38","DOI":"10.1007\/978-3-642-32759-9_38"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:03:08Z","timestamp":1725933788000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}