{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:09Z","timestamp":1751662869956,"version":"3.41.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3\/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples.<\/jats:p>\n          <jats:p>We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class.<\/jats:p>\n          <jats:p>We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries.<\/jats:p>\n          <jats:p>Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.<\/jats:p>","DOI":"10.1145\/3371073","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Complexity and information in invariant inference"],"prefix":"10.1145","volume":"4","author":[{"given":"Yotam M. Y.","family":"Feldman","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[{"name":"University of Massachusetts, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Rajeev Alur Rastislav Bod\u00edk Eric Dallal Dana Fisman Pranav Garg Garvit Juniwal Hadas Kress-Gazit P. Madhusudan Milo M. K. Martin Mukund Raghothaman Shambwaditya Saha Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. 1\u201325.  Rajeev Alur Rastislav Bod\u00edk Eric Dallal Dana Fisman Pranav Garg Garvit Juniwal Hadas Kress-Gazit P. Madhusudan Milo M. K. Martin Mukund Raghothaman Shambwaditya Saha Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. 1\u201325."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022821128753"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022692615781"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_15"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_2_6_1","volume-title":"Proceedings of the 30th Conference on Learning Theory, COLT 2017","author":"Bshouty Nader H.","year":"2017","unstructured":"Nader H. Bshouty , Dana Drachsler-Cohen , Martin T. Vechev , and Eran Yahav . 2017 . Learning Disjunctions of Predicates . In Proceedings of the 30th Conference on Learning Theory, COLT 2017 , Amsterdam, The Netherlands , 7-10 July 2017. 346\u2013369. Nader H. Bshouty, Dana Drachsler-Cohen, Martin T. Vechev, and Eran Yahav. 2017. Learning Disjunctions of Predicates. In Proceedings of the 30th Conference on Learning Theory, COLT 2017, Amsterdam, The Netherlands, 7-10 July 2017. 346\u2013369."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"e_1_2_2_8_1","volume-title":"15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 420\u2013432","author":"Col\u00f3n Michael","year":"2003","unstructured":"Michael Col\u00f3n , Sriram Sankaranarayanan , and Henny Sipma . 2003 . Linear Invariant Generation Using Non-linear Constraint Solving. In Computer Aided Verification , 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 420\u2013432 . Michael Col\u00f3n, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 420\u2013432."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages &amp; Applications, OOPSLA 2013, part of SPLASH 2013","author":"Dillig Isil","year":"2013","unstructured":"Isil Dillig , Thomas Dillig , Boyang Li , and Kenneth L . McMillan. 2013. Inductive invariant generation via abductive inference . In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages &amp; Applications, OOPSLA 2013, part of SPLASH 2013 , Indianapolis, IN, USA , October 26-31, 2013 . 443\u2013456. Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages &amp; Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013. 443\u2013456."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_13"},{"key":"e_1_2_2_13_1","volume-title":"International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911","author":"E\u00e9n Niklas","year":"2011","unstructured":"Niklas E\u00e9n , Alan Mishchenko , and Robert K. Brayton . 2011. Efficient implementation of property directed reachability . In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911 , Austin, TX, USA, October 30 - November 02, 2011 . 125\u2013134. http:\/\/dl.acm.org\/citation.cfm?id=2157675 Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, October 30 -November 02, 2011. 125\u2013134. http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"P. Ezudheen Daniel Neider Deepak D\u2019Souza Pranav Garg and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2 OOPSLA (2018) 131:1\u2013131:25.  P. Ezudheen Daniel Neider Deepak D\u2019Souza Pranav Garg and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2 OOPSLA (2018) 131:1\u2013131:25.","DOI":"10.1145\/3276501"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_2_20_1","volume-title":"ICE: A robust framework for learning invariants. Technical Report. 69\u201387 pages","author":"Garg Pranav","year":"2013","unstructured":"Pranav Garg , Christof L\u00f6ding , P Madhusudan , and Daniel Neider . 2013 . ICE: A robust framework for learning invariants. Technical Report. 69\u201387 pages . http:\/\/hdl.handle.net\/2142\/45973 Pranav Garg, Christof L\u00f6ding, P Madhusudan, and Daniel Neider. 2013. ICE: A robust framework for learning invariants. Technical Report. 69\u201387 pages. http:\/\/hdl.handle.net\/2142\/45973"},{"key":"e_1_2_2_21_1","volume-title":"ICE: A robust framework for learning invariants. In Computer Aided Verification","author":"Garg Pranav","year":"2014","unstructured":"Pranav Garg , Christof L\u00f6ding , P Madhusudan , and Daniel Neider . 2014 . ICE: A robust framework for learning invariants. In Computer Aided Verification . Springer , 69\u201387. Pranav Garg, Christof L\u00f6ding, P Madhusudan, and Daniel Neider. 2014. ICE: A robust framework for learning invariants. In Computer Aided Verification. Springer, 69\u201387."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1995.1003"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Oded Goldreich. 2006. On Promise Problems: A Survey. In Theoretical Computer Science Essays in Memory of Shimon Even. 254\u2013290.  Oded Goldreich. 2006. On Promise Problems: A Survey. In Theoretical Computer Science Essays in Memory of Shimon Even. 254\u2013290.","DOI":"10.1007\/11685654_12"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2012.69"},{"key":"e_1_2_2_27_1","volume-title":"FMCAD 2015","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel and Alexander Ivrii . 2015 . Pushing to the Top. In Formal Methods in Computer-Aided Design , FMCAD 2015 , Austin, Texas, USA , September 27-30, 2015. 65\u201372. Arie Gurfinkel and Alexander Ivrii. 2015. Pushing to the Top. In Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015. 65\u201372."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_2_29_1","volume-title":"Tight Bounds on Proper Equivalence Query Learning of DNF. In COLT 2012 - The 25th Annual Conference on Learning Theory","author":"Hellerstein Lisa","year":"2012","unstructured":"Lisa Hellerstein , Devorah Kletenik , Linda Sellie , and Rocco A. Servedio . 2012 . Tight Bounds on Proper Equivalence Query Learning of DNF. In COLT 2012 - The 25th Annual Conference on Learning Theory , June 25-27, 2012 , Edinburgh, Scotland. 31.1\u201331.18. http:\/\/proceedings.mlr.press\/v23\/hellerstein12\/hellerstein12.pdf Lisa Hellerstein, Devorah Kletenik, Linda Sellie, and Rocco A. Servedio. 2012. Tight Bounds on Proper Equivalence Query Learning of DNF. In COLT 2012 - The 25th Annual Conference on Learning Theory, June 25-27, 2012, Edinburgh, Scotland. 31.1\u201331.18. http:\/\/proceedings.mlr.press\/v23\/hellerstein12\/hellerstein12.pdf"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_2_31_1","volume-title":"Trento","author":"Hoder Krystof","year":"2012","unstructured":"Krystof Hoder and Nikolaj Bj\u00f8rner . 2012 . Generalized Property Directed Reachability. In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference , Trento , Italy , June 17-20, 2012. Proceedings. 157\u2013171. Krystof Hoder and Nikolaj Bj\u00f8rner. 2012. Generalized Property Directed Reachability. In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. 157\u2013171."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535843"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0294-5"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(4:1)2007"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_2_2_37_1","volume-title":"CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. 17\u201334","author":"Komuravelli Anvesh","year":"2014","unstructured":"Anvesh Komuravelli , Arie Gurfinkel , and Sagar Chaki . 2014 . SMT-Based Model Checking for Recursive Programs. In Computer Aided Verification - 26th International Conference , CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. 17\u201334 . Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. 17\u201334."},{"volume-title":"22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214\u2013229","author":"Shuvendu","key":"e_1_2_2_38_1","unstructured":"Shuvendu K. Lahiri and Shaz Qadeer. 2009. Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. In Automated Deduction - CADE-22 , 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214\u2013229 . Shuvendu K. Lahiri and Shaz Qadeer. 2009. Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 214\u2013229."},{"key":"e_1_2_2_39_1","volume-title":"Interactive Program Synthesis. CoRR","author":"Le Vu","year":"2017","unstructured":"Vu Le , Daniel Perelman , Oleksandr Polozov , Mohammad Raza , Abhishek Udupa , and Sumit Gulwani . 2017. Interactive Program Synthesis. CoRR ( 2017 ). arXiv: 1703.03539 http:\/\/arxiv.org\/abs\/1703.03539 Vu Le, Daniel Perelman, Oleksandr Polozov, Mohammad Raza, Abhishek Udupa, and Sumit Gulwani. 2017. Interactive Program Synthesis. CoRR (2017). arXiv: 1703.03539 http:\/\/arxiv.org\/abs\/1703.03539"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_10"},{"key":"e_1_2_2_41_1","volume-title":"15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1\u201313","author":"McMillan Kenneth L.","year":"2003","unstructured":"Kenneth L. McMillan . 2003 . Interpolation and SAT-Based Model Checking. In Computer Aided Verification , 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1\u201313 . Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1\u201313."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5121\/ijesa.2012.2204"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_18"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390666"},{"key":"e_1_2_2_49_1","volume-title":"11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings. 53\u201368","author":"Sankaranarayanan Sriram","year":"2004","unstructured":"Sriram Sankaranarayanan , Henny B. Sipma , and Zohar Manna . 2004 . Constraint-Based Linear-Relations Analysis. In Static Analysis , 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings. 53\u201368 . Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. 2004. Constraint-Based Linear-Relations Analysis. In Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings. 53\u201368."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"volume-title":"SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388\u2013411","author":"Sharma Rahul","key":"e_1_2_2_52_1","unstructured":"Rahul Sharma , Saurabh Gupta , Bharath Hariharan , Alex Aiken , and Aditya V. Nori . 2013a. Verification as Learning Geometric Concepts. In Static Analysis - 20th International Symposium , SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388\u2013411 . Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori. 2013a. Verification as Learning Geometric Concepts. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 388\u2013411."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542501"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1968.1972"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"e_1_2_2_62_1","volume-title":"VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. 521\u2013538","author":"Vizel Yakir","year":"2017","unstructured":"Yakir Vizel , Arie Gurfinkel , Sharon Shoham , and Sharad Malik . 2017 . IC3 - Flipping the E in ICE. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference , VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. 521\u2013538 . Yakir Vizel, Arie Gurfinkel, Sharon Shoham, and Sharad Malik. 2017. IC3 - Flipping the E in ICE. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. 521\u2013538."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371073","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371073","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371073"],"URL":"https:\/\/doi.org\/10.1145\/3371073","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}