{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:38Z","timestamp":1749318098122,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319899626"},{"type":"electronic","value":"9783319899633"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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":[[2018]]},"DOI":"10.1007\/978-3-319-89963-3_8","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T14:53:00Z","timestamp":1523631180000},"page":"132-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Non-linear Arithmetic Procedure for Control-Command Software Verification"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Roux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Iguernlala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Conchon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"8_CR1","volume-title":"The B-Book - Assigning Programs to Meanings","author":"J-R Abrial","year":"2005","unstructured":"Abrial, J.-R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"8_CR2","unstructured":"MOSEK ApS: The MOSEK C Optimizer API Manual Version 7.1 (Rev. 40) (2015)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F Besson","year":"2007","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48\u201362. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74464-1_4"},{"key":"8_CR5","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernlala, M., Lescuyer, S., Mebsout, A.: Alt-Ergo, Version 0.99.1. CNRS, Inria, Universit\u00e9 Paris-Sud 11, and OCamlPro, December 2014. \n                      http:\/\/alt-ergo.lri.fr\/"},{"issue":"1-4","key":"8_CR6","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1080\/10556789908805765","volume":"11","author":"Brian Borchers","year":"1999","unstructured":"Borchers, B.: CSDP, A C Library for Semidefinite Programming. Optimization Methods and Software (1999)","journal-title":"Optimization Methods and Software"},{"key":"8_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"S Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-31365-3_8","volume-title":"Automated Reasoning","author":"F Bobot","year":"2012","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Mahboubi, A., Mebsout, A., Melquiond, G.: A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 67\u201381. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31365-3_8"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Conchon, S., Contejean, \u00c9., Iguernelala, M.: Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation. In: Logical Methods in Computer Science, Selected Papers of TACAS (2012)","DOI":"10.2168\/LMCS-8(3:16)2012"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31424-7_55"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-28756-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cox","year":"2012","unstructured":"Cox, A., Sankaranarayanan, S., Chang, B.-Y.E.: A bit too precise? Bounded verification of quantized digital filters. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 33\u201347. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28756-5_4"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C - a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"8_CR13","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR14","unstructured":"de Oliveira, D.C.B., Monniaux, D.: Experiments on the feasibility of using a floating-point simplex in an SMT solver. In: PAAR@IJCAR (2012)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-79719-7_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"G Faure","year":"2008","unstructured":"Faure, G., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: SAT modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77\u201390. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-79719-7_8"},{"key":"8_CR16","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: \n                      \n                        \n                      \n                      $$\\delta $$\n                      \n                        \n                          \u03b4\n                        \n                      \n                    -Complete decision procedures for satisfiability\u00a0over\u00a0the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31365-3_23"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102\u2013118. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74591-4_9"},{"key":"8_CR20","unstructured":"H\u00e4rter, V., Jansson, C., Lange, M.: VSDP: verified semidefinite programming. \n                      http:\/\/www.ti3.tuhh.de\/jansson\/vsdp\/"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and gnatprove - a competition report from builders of an industrial-strength verifying compiler. In: STTT (2015)","DOI":"10.1007\/s10009-014-0322-5"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1137\/050622870","volume":"46","author":"C Jansson","year":"2007","unstructured":"Jansson, C., Chaykin, D., Keil, C.: Rigorous error bounds for the optimal value in semidefinite programming. SIAM J. Numer. Anal. 46(1), 180\u2013200 (2007)","journal-title":"SIAM J. Numer. Anal."},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2011.08.002","volume":"47","author":"E Kaltofen","year":"2012","unstructured":"Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. J. Symb. Comput. 47(1), 1\u201315 (2012)","journal-title":"J. Symb. Comput."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"King, T., Barrett, C.W., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: FMCAD (2014)","DOI":"10.1109\/FMCAD.2014.6987606"},{"issue":"3","key":"8_CR26","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1137\/S1052623400366802","volume":"11","author":"JB Lasserre","year":"2001","unstructured":"Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796\u2013817 (2001)","journal-title":"SIAM J. Optim."},{"key":"8_CR27","unstructured":"Lasserre, J.B.: Moments, Positive Polynomials and Their Applications. Imperial College Press Optimization. Imperial College Press, World Scientific, Singapore (2009)"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1109\/TAC.2009.2017144","volume":"5","author":"J L\u00f6fberg","year":"2009","unstructured":"L\u00f6fberg, J.: Pre- and post-processing sum-of-squares programs in practice. IEEE Trans. Autom. Control 5, 1007\u20131011 (2009)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"8_CR29","first-page":"1","volume":"8","author":"V Magron","year":"2015","unstructured":"Magron, V., Allamigeon, X., Gaubert, S., Werner, B.: Formal proofs for nonlinear optimization. J. Formalized Reason. 8(1), 1\u201324 (2015)","journal-title":"J. Formalized Reason."},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-662-49122-5_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Mar\u00e9chal","year":"2016","unstructured":"Mar\u00e9chal, A., Fouilh\u00e9, A., King, T., Monniaux, D., P\u00e9rin, M.: Polyhedral approximation of multivariate polynomials using handelman\u2019s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166\u2013184. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49122-5_8"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Martin-Dorel, \u00c9., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: CPP (2017)","DOI":"10.1145\/3018610.3018622"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-642-02658-4_42","volume-title":"Computer Aided Verification","author":"D Monniaux","year":"2009","unstructured":"Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 570\u2013583. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02658-4_42"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-22863-6_19","volume-title":"Interactive Theorem Proving","author":"D Monniaux","year":"2011","unstructured":"Monniaux, D., Corbineau, P.: On the generation of positivstellensatz witnesses in degenerate cases. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 249\u2013264. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22863-6_19"},{"issue":"2","key":"8_CR34","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10817-012-9256-3","volume":"51","author":"C Mu\u00f1oz","year":"2013","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of Bernstein polynomials and applications to global optimization. J. Autom. Reason. 51(2), 151\u2013196 (2013)","journal-title":"J. Autom. Reason."},{"key":"8_CR35","unstructured":"Nuzzo, P., Puggelli, A., Seshia, S.A., Sangiovanni-Vincentelli, A.L.: CalCS: SMT solving for non-linear convex constraints. In: FMCAD (2010)"},{"issue":"2","key":"8_CR36","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","journal-title":"Math. Program."},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-02959-2_35","volume-title":"Automated Deduction \u2013 CADE-22","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485\u2013501. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02959-2_35"},{"issue":"2","key":"8_CR38","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10817-015-9339-z","volume":"57","author":"P Roux","year":"2016","unstructured":"Roux, P.: Formal proofs of rounding error bounds - with application to an automatic positive definiteness check. J. Autom. Reasoning 57(2), 135\u2013156 (2016)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P.-L., F\u00e9ron, \u00c9: A generic ellipsoid abstract domain for linear time invariant systems. In: HSCC (2012)","DOI":"10.1145\/2185632.2185651"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-662-53413-7_21","volume-title":"Static Analysis","author":"P Roux","year":"2016","unstructured":"Roux, P., Voronin, Y.-L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 424\u2013446. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-53413-7_21"},{"issue":"2","key":"8_CR41","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10543-006-0056-1","volume":"46","author":"SM Rump","year":"2006","unstructured":"Rump, S.M.: Verification of positive definiteness. BIT Num. Math. 46(2), 433\u2013452 (2006)","journal-title":"BIT Num. Math."},{"key":"8_CR42","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S096249291000005X","volume":"19","author":"SM Rump","year":"2010","unstructured":"Rump, S.M.: Verification methods: rigorous results using floating-point arithmetic. Acta Numerica 19, 287\u2013449 (2010)","journal-title":"Acta Numerica"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Shoukry, Y., Nuzzo, P., Sangiovanni-Vincentelli, A.L., Seshia, S.A., Pappas, G.J., Tabuada, P.: SMC: satisfiability modulo convex optimization. In: HSCC (2017)","DOI":"10.1145\/3049797.3049819"},{"issue":"1","key":"8_CR44","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1137\/1038003","volume":"38","author":"L Vandenberghe","year":"1996","unstructured":"Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49\u201395 (1996)","journal-title":"SIAM Rev."},{"key":"8_CR45","volume-title":"Fundamentals of matrix computations","author":"DS Watkins","year":"2004","unstructured":"Watkins, D.S.: Fundamentals of matrix computations. Wiley, New York (2004)"},{"key":"8_CR46","unstructured":"Yamashita, M., Fujisawa, K., Nakata, K., Nakata, M., Fukuda, M., Kobayashi, K., Goto, K.: A high-performance software package for semidefinite programs: SDPA 7. Technical report B-460, Tokyo Institute of Technology, Tokyo (2010)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89963-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:16:29Z","timestamp":1583205389000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89963-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899626","9783319899633"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89963-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}