{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:19Z","timestamp":1775873659178,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["759102-SVIS"],"award-info":[{"award-number":["759102-SVIS"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1655166"],"award-info":[{"award-number":["1655166"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011643","name":"Blavatnik Family Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100011643","id-type":"DOI","asserted-by":"publisher"}]},{"name":"United States-Israel Binational Science Foundation","award":["2016260, 2012259"],"award-info":[{"award-number":["2016260, 2012259"]}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Pazi"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192414","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"662-677","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Modularity for decidability of deductive verification with applications to distributed systems"],"prefix":"10.1145","author":[{"given":"Marcelo","family":"Taube","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuliano","family":"Losa","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"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"}]},{"given":"James R.","family":"Wilcox","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doug","family":"Woos","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Automated Reasoning","author":"Alberti Francesco","unstructured":"Francesco Alberti , Silvio Ghilardi , and Elena Pagani . 2016. Counting Constraints in Flat Array Fragments . In Automated Reasoning . Springer , Cham , 65-81. Francesco Alberti, Silvio Ghilardi, and Elena Pagani. 2016. Counting Constraints in Flat Array Fragments. In Automated Reasoning. Springer, Cham, 65-81."},{"key":"e_1_3_2_2_2_1","volume-title":"Rami Gokhan Kici, and Ranjit Jhala","author":"Bakst Alexander","year":"2017","unstructured":"Alexander Bakst , Klaus von Gleissenthall , Rami Gokhan Kici, and Ranjit Jhala . 2017 . Verifying distributed programs via canonical sequentialization. PACMPL 1, OOPSLA ( 2017), 110:1-110:27. Alexander Bakst, Klaus von Gleissenthall, Rami Gokhan Kici, and Ranjit Jhala. 2017. Verifying distributed programs via canonical sequentialization. PACMPL 1, OOPSLA (2017), 110:1-110:27."},{"key":"e_1_3_2_2_3_1","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings. 97-109","author":"Berdine Josh","unstructured":"Josh Berdine , Cristiano Calcagno , and Peter W . O'Hearn. 2004. A Decidable Fragment of Separation Logic . In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings. 97-109 . Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. 2004. A Decidable Fragment of Separation Logic. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings. 97-109."},{"key":"e_1_3_2_2_4_1","volume-title":"Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Casteran . 2004. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions . Springer . Yves Bertot and Pierre Casteran. 2004. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Springer."},{"key":"e_1_3_2_2_5_1","volume-title":"Decidability of Parameterized Verification","author":"Bloem Roderick","unstructured":"Roderick Bloem , Swen Jacobs , Ayrat Khalimov , Igor Konnov , Sasha Rubin , Helmut Veith , and Josef Widder . 2015. Decidability of Parameterized Verification . Morgan & Claypool Publishers . Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. 2015. Decidability of Parameterized Verification. Morgan & Claypool Publishers."},{"key":"e_1_3_2_2_6_1","volume-title":"7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. 427-442","author":"Bradley Aaron R.","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B. Sipma . 2006. What's Decidable About Arrays?. In Verification, Model Checking, and Abstract Interpretation , 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. 427-442 . Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What's Decidable About Arrays?. In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. 427-442."},{"key":"e_1_3_2_2_7_1","first-page":"119","volume-title":"Formal Verification of Multi-Paxos for Distributed Consensus. In FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21","author":"Chand Saksham","unstructured":"Saksham Chand , Yanhong A. Liu , and Scott D. Stoller . 2016 . Formal Verification of Multi-Paxos for Distributed Consensus. In FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21 . Springer , 119 - 136 . Saksham Chand, Yanhong A. Liu, and Scott D. Stoller. 2016. Formal Verification of Multi-Paxos for Distributed Consensus. In FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21. Springer, 119-136."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1881833.1881837"},{"key":"e_1_3_2_2_9_1","volume-title":"VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs","author":"Cohen Ernie","year":"2009","unstructured":"Ernie Cohen , Markus Dahlweid , Mark A. Hillebrand , Dirk Leinenbach , Michal Moskal , Thomas Santen , Wolfram Schulte , and Stephan Tobies . 2009 . VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Lecture Notes in Computer Science), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674 . Springer , 23-42. Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Lecture Notes in Computer Science), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 23-42."},{"key":"e_1_3_2_2_10_1","unstructured":"CoreOS 2014. etcd: A highly-available key value store for shared configuration and service discovery. https:\/\/github.com\/coreos\/etcd.  CoreOS 2014. etcd: A highly-available key value store for shared configuration and service discovery. https:\/\/github.com\/coreos\/etcd."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_2_14_1","volume-title":"Navas","author":"Dutertre Bruno","year":"2018","unstructured":"Bruno Dutertre , Dejan Jovanovic , and Jorge A . Navas . 2018 . Verification of Fault-Tolerant Protocols with Sally. In NASA Formal Methods, Aaron Dutle, Cesar Munoz, and Anthony Narkawicz (Eds.). Springer International Publishing , Cham, 113-120. Bruno Dutertre, Dejan Jovanovic, and Jorge A. Navas. 2018. Verification of Fault-Tolerant Protocols with Sally. In NASA Formal Methods, Aaron Dutle, Cesar Munoz, and Anthony Narkawicz (Eds.). Springer International Publishing, Cham, 113-120."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_2_16_1","volume-title":"ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings.","author":"Garcia-Perez Alvaro","year":"2018","unstructured":"Alvaro Garcia-Perez , Alexey Gotsman , Yuri Meshman , and Ilya Sergey . 2018 . Paxos Consensus, Deconstructed and Abstracted. In Programming Languages and Systems - 27th European Symposium on Programming , ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Alvaro Garcia-Perez, Alexey Gotsman, Yuri Meshman, and Ilya Sergey. 2018. Paxos Consensus, Deconstructed and Abstracted. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_2_19_1","volume-title":"First International Workshop, TACAS. 89-110","author":"Henriksen Jesper G.","year":"1995","unstructured":"Jesper G. Henriksen , Jakob L. Jensen , Michael E. Jurgensen , Nils Klarlund , Robert Paige , Theis Rauhe , and Anders Sandholm . 1995 . Mona: Monadic Second-Order Logic in Practice. In Tools and Algorithms for Construction and Analysis of Systems , First International Workshop, TACAS. 89-110 . Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jurgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. 1995. Mona: Monadic Second-Order Logic in Practice. In Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS. 89-110."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_2_21_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, Language, and Analysis . The MIT Press . Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_3_2_2_24_1","volume-title":"Computer Aided Verification","author":"Konnov Igor","unstructured":"Igor Konnov , Helmut Veith , and Josef Widder . 2015. SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms . In Computer Aided Verification . Springer , Cham , 85-102. Igor Konnov, Helmut Veith, and Josef Widder. 2015. SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In Computer Aided Verification. Springer, Cham, 85-102."},{"key":"e_1_3_2_2_25_1","volume-title":"PSI 2015","author":"Konnov Igor V.","year":"2015","unstructured":"Igor V. Konnov , Helmut Veith , and Josef Widder . 2015 . What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference , PSI 2015 , in Memory of Helmut Veith, Kazan and Innopolis, Russia , August 24-27, 2015, Revised Selected Papers (Lecture Notes in Computer Science), Manuel Mazzara and Andrei Voronkov (Eds.), Vol. 9609. Springer, 6-21. Igor V. Konnov, Helmut Veith, and Josef Widder. 2015. What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Lecture Notes in Computer Science), Manuel Mazzara and Andrei Voronkov (Eds.), Vol. 9609. Springer, 6-21."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_2_27_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA."},{"key":"e_1_3_2_2_28_1","volume-title":"Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino . 2010 . Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning . Springer , 348-370. K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348-370."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994595"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926455"},{"key":"e_1_3_2_2_34_1","first-page":"217","volume-title":"CAV 2017, Heidelberg, Germany, July 24- 28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.)","volume":"10427","author":"Maric Ognjen","unstructured":"Ognjen Maric , Christoph Sprenger , and David A. Basin . 2017. Cutoff Bounds for Consensus Algorithms. In Computer Aided Verification - 29th International Conference , CAV 2017, Heidelberg, Germany, July 24- 28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.) , Vol. 10427 . Springer , 217 - 237 . Ognjen Maric, Christoph Sprenger, and David A. Basin. 2017. Cutoff Bounds for Consensus Algorithms. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24- 28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.), Vol. 10427. Springer, 217-237."},{"key":"e_1_3_2_2_35_1","volume-title":"FMCAD 2016","author":"McMillan Kenneth L.","year":"2016","unstructured":"Kenneth L. McMillan . 2016 . Modular specification and verification of a cache-coherent interface. In 2016 Formal Methods in Computer-Aided Design , FMCAD 2016 , Mountain View, CA, USA , October 3-6, 2016, Ruzica Piskac and Muralidhar Talupur (Eds.). IEEE, 109-116. Kenneth L. McMillan. 2016. Modular specification and verification of a cache-coherent interface. In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, Ruzica Piskac and Muralidhar Talupur (Eds.). IEEE, 109-116."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_2_37_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002. Isabelle\/ HOL : A Proof Assistant for Higher-Order Logic . Vol. 2283 . Springer Science & Business Media . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/ HOL: A Proof Assistant for Higher-Order Logic. Vol. 2283. Springer Science & Business Media."},{"key":"e_1_3_2_2_38_1","volume-title":"2014 USENIX Annual Technical Conference, USENIX ATC '14","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John K. Ousterhout . 2014. In Search of an Understandable Consensus Algorithm . In 2014 USENIX Annual Technical Conference, USENIX ATC '14 , Philadelphia, PA, USA , June 19-20, 2014 . 305-319. https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/ongaro Diego Ongaro and John K. Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In 2014 USENIX Annual Technical Conference, USENIX ATC '14, Philadelphia, PA, USA, June 19-20, 2014. 305-319. https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/ongaro"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908129"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192414","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192414","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":46,"alternative-id":["10.1145\/3192366.3192414","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192414","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192414","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}