{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:52:43Z","timestamp":1764402763600,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545768"},{"type":"electronic","value":"9783662545775"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54577-5_7","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"118-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Efficient Certified Resolution Proof Checking"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/s10817-013-9289-2","volume":"52","author":"E Alkassar","year":"2014","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C.: A framework for the verification of certifying computations. J. Autom. Reason. 52(3), 241\u2013273 (2014)","journal-title":"J. Autom. Reason."},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-25379-9_12"},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"7_CR4","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"issue":"2\u20134","key":"7_CR5","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"7_CR6","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-40229-1_4","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 25\u201344. Springer, Cham (2016). doi:10.1007\/978-3-319-40229-1_4"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. In: STOC, pp. 86\u201397 (1989)","DOI":"10.1145\/73007.73015"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Bras, R.L., Gomes, C.P., Selman, B.: On the Erd\u0151s discrepancy problem. In: CP, pp. 440\u2013448 (2014)","DOI":"10.1007\/978-3-319-10428-7_33"},{"issue":"2\/3","key":"7_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M., Hunt, W., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. CoRR, abs\/1610.06984 (2016)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"7_CR12","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Checking the Boolean Pythagorean Triples conjecture. http:\/\/imada.sdu.dk\/~petersk\/bpt\/"},{"key":"7_CR13","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Grit format, formalization, and checkers. http:\/\/imada.sdu.dk\/~petersk\/grit\/. Source codes also available from: https:\/\/github.com\/peter-sk\/grit"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-319-22102-1_10","volume-title":"Interactive Theorem Proving","author":"L Cruz-Filipe","year":"2015","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Formalizing size-optimal sorting networks: extracting a certified proof checker. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 154\u2013169. Springer, Cham (2015). doi:10.1007\/978-3-319-22102-1_10"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-20615-8_4","volume-title":"Intelligent Computer Mathematics","author":"L Cruz-Filipe","year":"2015","unstructured":"Cruz-Filipe, L., Schneider-Kamp, P.: Optimizing a certified proof checker for a large-scale computer-generated proof. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 55\u201370. Springer, Cham (2015). doi:10.1007\/978-3-319-20615-8_4"},{"key":"7_CR16","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Formalizing a SAT proof checker in Coq. In: First Coq Workshop (2009)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-14808-8_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"A Darbari","year":"2010","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified SAT solving through verified SAT proof checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 260\u2013274. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14808-8_18"},{"key":"7_CR18","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10886\u201310891 (2003)"},{"key":"7_CR19","unstructured":"Heule, M.: The DRAT format and DRAT-trim checker. CoRR, abs\/1610.06229 (2016). https:\/\/github.com\/marijnheule\/drat-trim"},{"key":"7_CR20","unstructured":"Heule, M., Biere, A.: Proofs for satisfiability problems. In: All About Proofs, Proofs for All (APPA), July 2014. http:\/\/www.easychair.org\/smart-program\/VSL2014\/APPA-index.html"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Heule, M., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD, pp. 181\u2013188 (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38574-2_24","volume-title":"Automated Deduction \u2013 CADE-24","author":"MJH Heule","year":"2013","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 345\u2013359. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38574-2_24"},{"issue":"8","key":"7_CR23","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1002\/stvr.1549","volume":"24","author":"M Heule","year":"2014","unstructured":"Heule, M., Hunt Jr., W.A., Wetzler, N.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verif. Reliab. 24(8), 593\u2013607 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-319-21401-6_40","volume-title":"Automated Deduction \u2013 CADE-25","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591\u2013606. Springer, Cham (2015). doi:10.1007\/978-3-319-21401-6_40"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). doi:10.1007\/978-3-319-40970-2_15"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., Biere, A.: Efficient extraction of skolem functions from QRAT proofs. In: FMCAD, pp. 107\u2013114 (2014)","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A., Sinz, C., Kr\u00f6ning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201\u2013214. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-72788-0_21"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11814948_8","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"T Jussila","year":"2006","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 54\u201360. Springer, Heidelberg (2006). doi:10.1007\/11814948_8"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. CoRR, abs\/1405.3097 (2014)","DOI":"10.1016\/j.artint.2015.03.004"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219\u2013226. Springer, Cham (2014). doi:10.1007\/978-3-319-09284-3_17"},{"key":"7_CR31","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224, 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-04222-5_18","volume-title":"Frontiers of Combining Systems","author":"S Lescuyer","year":"2009","unstructured":"Lescuyer, S., Conchon, S.: Improving Coq propositional reasoning using a lazy CNF conversion scheme. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 287\u2013303. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-04222-5_18"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-69407-6_39"},{"issue":"50","key":"7_CR34","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Maric","year":"2010","unstructured":"Maric, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010)","journal-title":"Theor. Comput. Sci."},{"issue":"3:19","key":"7_CR35","first-page":"1","volume":"7","author":"F Maric","year":"2011","unstructured":"Maric, F., Janicic, P.: Formalization of abstract state transition systems for SAT. LMCS 7(3:19), 1\u201337 (2011)","journal-title":"LMCS"},{"issue":"2","key":"7_CR36","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-88387-6_3","volume-title":"Automated Technology for Verification and Analysis","author":"N Shankar","year":"2008","unstructured":"Shankar, N.: Trust and automation in verification tools. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 4\u201317. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-88387-6_3"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600\u2013611. Springer, Heidelberg (2006). doi:10.1007\/11753728_60"},{"key":"7_CR39","unstructured":"Smith, D.R., Westfold, S.J.: Synthesis of satisfiability solvers. Technical report, Kestrel Institute (2008)"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008)","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-02777-2_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A Gelder","year":"2009","unstructured":"Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 141\u2013146. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02777-2_15"},{"issue":"4","key":"7_CR42","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Van Gelder","year":"2012","unstructured":"Van Gelder, A.: Producing and verifying extremely large propositional refutations - have your cake and eat it too. Ann. Math. Artif. Intell. 65(4), 329\u2013372 (2012)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"7_CR43","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T Weber","year":"2009","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Appl. Logic 7(1), 26\u201340 (2009)","journal-title":"J. Appl. Logic"},{"key":"7_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39634-2_18","volume-title":"Interactive Theorem Proving","author":"N Wetzler","year":"2013","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 229\u2013244. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2_18"},{"key":"7_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). doi:10.1007\/978-3-319-09284-3_31"},{"key":"7_CR46","unstructured":"Wetzler, N.D.: Efficient, mechanically-verified validation of satisfiability solvers. Ph.D. thesis, The University of Texas at Austin (2015)"},{"key":"7_CR47","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880\u201310885 (2003)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54577-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:34:38Z","timestamp":1750188878000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}