{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:13:33Z","timestamp":1784837613598,"version":"3.55.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present the tool PyLTA, which can model check parameterized distributed algorithms against LTL specifications. The parameters typically include the number of processes and a bound on faulty processes, and the considered algorithms are round-based and either synchronous or asynchronous.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_4","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"28-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["PyLTA: A Verification Tool for Parameterized Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Bastien","family":"Thomas","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ocan","family":"Sankur","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"A.\u00a0R. Balasubramanian, Javier Esparza, and Marijana Lazi\u0107. Complexity of verification and synthesis of threshold automata. In Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201920), volume 12302 of Lecture Notes in Computer Science, pages 144\u2013160. Springer, 2020.","DOI":"10.1007\/978-3-030-59152-6_8"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Piotr Berman and Juan\u00a0A. Garay. Cloture votes: n\/4-resilient distributed consensus in t+1 rounds. Mathematical Systems Theory, 26(1):3\u201319, 1993.","DOI":"10.1007\/BF01187072"},{"key":"4_CR3","unstructured":"Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard automata for the verification of safety and liveness of distributed algorithms. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 15:1\u201315:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.","DOI":"10.1007\/978-3-031-02011-7"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT Solver. In Nir Piterman and Scott Smolka, editors, Proceedings of TACAS, volume 7795 of LNCS. Springer, 2013.","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752\u2013794, sep 2003.","DOI":"10.1145\/876638.876643"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In Michael\u00a0I. Schwartzbach and Thomas Ball, editors, Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pages 415\u2013426. ACM, 2006.","DOI":"10.1145\/1133255.1134029"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Andrei Damian, Cezara Dr\u0103goi, Alexandru Militaru, and Josef Widder. Communication-closed asynchronous protocols. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV\u201919), volume 11562 of Lecture Notes in Computer Science, pages 344\u2013363. Springer, 2019.","DOI":"10.1007\/978-3-030-25543-5_20"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, and Sergio Mover. Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 271\u2013291. Springer, 2016.","DOI":"10.1007\/978-3-319-41528-4_15"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916), volume 9938 of Lecture Notes in Computer Science, pages 122\u2013129. Springer, October 2016.","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"4_CR11","unstructured":"Marco Gario and Andrea Micheli. Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In SMT Workshop 2015, 2015."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Thomas\u00a0A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth\u00a0L. McMillan. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201904, page 232\u2013244, New York, NY, USA, 2004. Association for Computing Machinery.","DOI":"10.1145\/964001.964021"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Igor Konnov, Marijana Lazi\u0107, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL\u201917), pages 719\u2013734, 2017.","DOI":"10.1145\/3009837.3009860"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Igor Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252:95\u2013109, 2017.","DOI":"10.1016\/j.ic.2016.03.006"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Igor Konnov and Josef Widder. Bymc: Byzantine model checker. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III, volume 11246 of Lecture Notes in Computer Science, pages 327\u2013342. Springer, 2018.","DOI":"10.1007\/978-3-030-03424-5_22"},{"key":"4_CR16","unstructured":"Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in parameterized systems: All flavors of threshold automata. In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR\u201918), volume 118 of LIPIcs, pages 19:1\u201319:17, 2018."},{"key":"4_CR17","unstructured":"Nancy\u00a0A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Amir Pnueli, Jessie Xu, and Lenore\u00a0D. Zuck. Liveness with (0, 1, infty)-counter abstraction. In Proceedings of the 14th International Conference on Computer Aided Verification, CAV \u201902, page 107\u2013122, Berlin, Heidelberg, 2002.Springer-Verlag.","DOI":"10.1007\/3-540-45657-0_9"},{"key":"4_CR19","unstructured":"Erez Shinan. Lark. https:\/\/github.com\/lark-parser\/lark\/, 2018-2022."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger. Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919), volume 11428 of Lecture Notes in Computer Science, pages 357\u2013374, 2019.","DOI":"10.1007\/978-3-030-17465-1_20"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Stefano Tonetta. Abstract model checking without computing the abstraction. In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, volume 5850 of Lecture Notes in Computer Science, pages 89\u2013105. Springer, 2009.","DOI":"10.1007\/978-3-642-05089-3_7"}],"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-031-30820-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:02:45Z","timestamp":1690974165000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}