{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:39:33Z","timestamp":1767137973726,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319948201","type":"print"},{"value":"9783319948218","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-94821-8_5","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"68-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Backwards and Forwards with Separation Logic"],"prefix":"10.1007","author":[{"given":"Callum","family":"Bannister","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-25379-9_18","volume-title":"Certified Programs and Proofs","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: VeriSmall: verified smallfoot shape analysis. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 231\u2013246. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-25379-9_18"},{"key":"5_CR3","unstructured":"Bannister, C., H\u00f6fner, P., Klein, G.: Forward and backward reasoning in separation logic. Isabelle theories (2018). \nhttps:\/\/github.com\/sel4proj\/Jormungand\/tree\/ITP18"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-32347-8_21","volume-title":"Interactive Theorem Proving","author":"J Bengtson","year":"2012","unstructured":"Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! A framework for higher-order. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315\u2013331. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_21"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11575467_5"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-41202-8_6","volume-title":"Formal Methods and Software Engineering","author":"A Boyton","year":"2013","unstructured":"Boyton, A., Andronick, J., Bannister, C., Fernandez, M., Gao, X., Greenaway, D., Klein, G., Lewis, C., Sewell, T.: Formally verified system initialisation. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 70\u201385. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-41202-8_6"},{"key":"5_CR8","first-page":"23","volume-title":"Machine Intelligence","author":"R Burstal","year":"1972","unstructured":"Burstal, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 23\u201350. Edinburgh University Press, Edinburgh (1972)"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011). \nhttps:\/\/doi.org\/10.1145\/2049697.2049700","DOI":"10.1145\/2049697.2049700"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Logic in Computer Science (LICS 2007), pp. 366\u2013378. IEEE (2007). \nhttps:\/\/doi.org\/10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108\u2013119. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-45294-X_10"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) International Conference on Functional Programming (ICFP 2011), pp. 418\u2013430. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/2034773.2034828","DOI":"10.1145\/2034773.2034828"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Hall, M.W., Padua, D.A. (eds.) Programming Language Design and Implementation (PLDI 2011), pp. 234\u2013245. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1993498.1993526","DOI":"10.1145\/1993498.1993526"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167\u2013182. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_16"},{"issue":"6","key":"5_CR15","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.jlap.2011.04.003","volume":"80","author":"HH Dang","year":"2011","unstructured":"Dang, H.H., H\u00f6fner, P., M\u00f6ller, B.: Algebraic separation logic. J. Logic Algebraic Programm. 80(6), 221\u2013247 (2011). \nhttps:\/\/doi.org\/10.1016\/j.jlap.2011.04.003","journal-title":"J. Logic Algebraic Programm."},{"key":"5_CR16","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-12029-9_20","volume-title":"Fundamental Approaches to Software Engineering","author":"D Distefano","year":"2010","unstructured":"Distefano, D., Filipovi\u0107, I.: Memory leaks detection in java by bi-abductive inference. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 278\u2013292. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-12029-9_20"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11691372_19"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci. 19, 19\u201332 (1967)","journal-title":"Math. Aspects Comput. Sci."},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-1-84882-912-1_5","volume-title":"Reflections on the Work of C.A.R. Hoare","author":"M Gordon","year":"2010","unstructured":"Gordon, M., Collavizza, H.: Forward with hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 101\u2013121. Springer, London (2010). \nhttps:\/\/doi.org\/10.1007\/978-1-84882-912-1_5"},{"issue":"10","key":"5_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). \nhttps:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: Giacobazzi, R., Cousot, R. (eds.) Principles of Programming Languages (POPL 2013), pp. 523\u2013536. ACM (2013). \nhttps:\/\/doi.org\/10.1145\/2429069.2429131","DOI":"10.1145\/2429069.2429131"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-319-21401-6_34","volume-title":"Automated Deduction - CADE-25","author":"Z H\u00f3u","year":"2015","unstructured":"H\u00f3u, Z., Gor\u00e9, R., Tiu, A.: Automated theorem proving for assertions in separation logic with all connectives. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 501\u2013516. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_34"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-66107-0_19","volume-title":"Interactive Theorem Proving","author":"Z H\u00f3u","year":"2017","unstructured":"H\u00f3u, Z., San\u00e1n, D., Tiu, A., Liu, Y.: Proof tactics for assertions in separation logic. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 285\u2013303. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66107-0_19"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (POPL 2001), vol. 36, pp. 14\u201326. ACM (2001). \nhttps:\/\/doi.org\/10.1145\/373243.375719","DOI":"10.1145\/373243.375719"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304\u2013311. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17164-2_21"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Principles of Programming Languages (POPL 2015), pp. 637\u2013650. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. Trans. Comput. Syst. 32(1), 2:1\u20132:70 (2014). \nhttps:\/\/doi.org\/10.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-32347-8_22","volume-title":"Interactive Theorem Proving","author":"G Klein","year":"2012","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332\u2013337. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_22"},{"key":"5_CR30","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Separation algebra. Archive of Formal Proofs, Formal proof development (2012). \nhttp:\/\/isa-afp.org\/entries\/Separation_Algebra.shtml"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Principles of Programming Languages (POPL 2017), pp. 205\u2013217. ACM (2017). \nhttps:\/\/doi.org\/10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Lee, W., Park, S.: A proof system for separation logic with magic wand. In: Jagannathan, S., Sewell, P. (eds.) Principles of Programming Languages (POPL 2014), pp. 477\u2013490. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2535838.2535871","DOI":"10.1145\/2535838.2535871"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"2","key":"5_CR34","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1093\/logcom\/exu032","volume":"26","author":"E Maclean","year":"2016","unstructured":"Maclean, E., Ireland, A., Grov, G.: Proof automation for functional correctness in separation logic. J. Logic Comput. 26(2), 641\u2013675 (2016). \nhttps:\/\/doi.org\/10.1093\/logcom\/exu032","journal-title":"J. Logic Comput."},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 121\u2013135. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45085-6_10"},{"key":"5_CR36","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/978-94-010-0413-8_11","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science (LICS 2002), pp. 55\u201374 (2002). \nhttps:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: An introduction to separation logic. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 22, pp. 285\u2013310. IOS Press (2009). \nhttps:\/\/doi.org\/10.3233\/978-1-58603-976-9-285","DOI":"10.3233\/978-1-58603-976-9-285"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Grove, D., Blackburn, S. (eds.) Programming Language Design and Implementation (PLDI 2015), pp. 77\u201387. ACM (2015). \nhttps:\/\/doi.org\/10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"key":"5_CR42","unstructured":"Tuerk, T.: A Separation Logic Framework for HOL. Ph.D. thesis, University of Cambridge, UK (2011)"},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"}],"updated-by":[{"DOI":"10.1007\/978-3-319-94821-8_38","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2018,9,12]],"date-time":"2018-09-12T00:00:00Z","timestamp":1536710400000}}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,9,11]],"date-time":"2018-09-11T18:30:47Z","timestamp":1536690647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","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":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}