I. Suzuki, "Proving properties of a ring of finite state machines, " Inf. Process. Lett., vol. 28, no. 4, pp. 213-214, 1988.
S. M. German and A. P. Sistla, "Reasoning about systems with many processes, " J. ACM, vol. 39, no. 3, pp. 675-735, 1992.
J. Esparza, A. Finkel, and R. Mayr, "On the verification of broadcast protocols, " in LICS. IEEE Computer Society, 1999, pp. 352-359.
E. A. Emerson and V. Kahlon, "Reducing model checking of the many to the few, " in CADE, ser. LNCS, vol. 1831. Springer, 2000, pp. 236-254.
E. A. Emerson and K. S. Namjoshi, "On reasoning about rings, " Foundations of Computer Science, vol. 14, no. 4, pp. 527-549, 2003.
E. A. Emerson and V. Kahlon, "Model checking guarded protocols, " in LICS. IEEE Computer Society, 2003, pp. 361-370.
E. M. Clarke, M. Talupur, T. Touili, and H. Veith, "Verification by network decomposition, " in CONCUR, ser. LNCS, vol. 3170. Springer, 2004, pp. 276-291.
B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, "Parameterized model checking of token-passing systems, " in VMCAI, ser. LNCS, vol. 8318. Springer, 2014, pp. 262-281.
B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith, "Parameterized model checking of rendezvous systems, " in CONCUR, ser. LNCS, vol. 8704. Springer, 2014, pp. 109-124.
B. Aminof and S. Rubin, "Model checking parameterised multi-token systems via the composition method, " in IJCAR, ser. LNCS, vol. 9706. Springer, 2016, pp. 499-515.
B. Jobstmann, A. Griesmayer, and R. Bloem, "Program repair as a game, " in 17th Conference on Computer Aided Verification (CAV'05). Springer, 2005, pp. 226-238, lNCS 3576.
P. C. Attie, K. D. A. Bab, and M. Sakr, "Model and program repair via sat solving, " ACM Transactions on Embedded Computing Systems (TECS), vol. 17, no. 2, pp. 1-25, 2017.
R. Bloem, G. Hofferek, B. Konighofer, R. Konighofer, S. Auserlechner, and R. Spork, "Synthesis of synchronization using uninterpreted functions, " in 2014 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2014, pp. 35-42.
J. McClurg, H. Hojjat, and P. C erny, "Synchronization synthesis for network programs, " in International Conference on Computer Aided Verification. Springer, 2017, pp. 301-321.
P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay, "General decidability theorems for infinite-state systems, " in Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. IEEE, 1996, pp. 313-321.
A. Finkel and P. Schnoebelen, "Well-structured transition systems everywhere!" Theoretical Computer Science, vol. 256, no. 1-2, pp. 63-92, 2001.
S. Jacobs, M. Sakr, and M. Volp, "Parameterized repair of concurrent systems, " 2021. [Online]. Available: Https: //doi. org/10. 48550/arXiv. 2111. 03322
A. Pnueli, J. Xu, and L. D. Zuck, "Liveness with (0, 1, infty)-counter abstraction, " in CAV, ser. Lecture Notes in Computer Science, vol. 2404. Springer, 2002, pp. 107-122.
N. Jaber, S. Jacobs, C. Wagner, M. Kulkarni, and R. Samanta, "Parameterized verification of systems with global synchronization and guards, " in CAV (1), ser. Lecture Notes in Computer Science, vol. 12224. Springer, 2020, pp. 299-323.
W. Czerwinski, S. Lasota, R. Lazic, J. Leroux, and F. Mazowiecki, "The reachability problem for petri nets is not elementary, " J. ACM, vol. 68, no. 1, pp. 7: 1-7: 28, 2021.
G. Delzanno, A. Sangnier, and G. Zavattaro, "Parameterized verification of ad hoc networks, " in CONCUR, ser. LNCS, vol. 6269. Springer, 2010, pp. 313-327.
N. Jaber, C. Wagner, S. Jacobs, M. Kulkarni, and R. Samanta, "Quicksilver: Modeling and parameterized verification for distributed agreementbased systems, " Proc. ACM Program. Lang., vol. 5, no. OOPSLA, pp. 1-31, 2021.
M. Burrows, "The chubby lock service for loosely-coupled distributed systems, " in OSDI. USENIX Association, 2006, pp. 335-350.
D. Canepa and M. G. Potop-Butucaru, "Stabilizing flocking via leader election in robot networks, " in SSS, ser. Lecture Notes in Computer Science, vol. 4838. Springer, 2007, pp. 52-66.
C. Chang and J. Tsai, "Distributed collaborative surveillance system based on leader election protocols, " IET Wirel. Sens. Syst., vol. 6, no. 6, pp. 198-205, 2016.
E. A. Emerson and V. Kahlon, "Exact and efficient verification of parameterized cache coherence protocols, " in CHARME, ser. LNCS, vol. 2860. Springer, 2003, pp. 247-262.
B. Demsky and M. Rinard, "Automatic detection and repair of errors in data structures, " in Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'03), 2003, pp. 78-95.
A. Griesmayer, R. Bloem, and B. Cook, "Repair of Boolean programs with an application to C, " in 18th Conference on Computer Aided Verification (CAV'06), 2006, pp. 358-371, LNCS 4144.
S. Forrest, T. Nguyen, W. Weimer, and C. L. Goues, "A genetic programming approach to automated software repair, " in Genetic and Evolutionary Computation Conference (GECCO'09). ACM, 2009, pp. 947-954.
M. Monperrus, "Automatic software repair: A bibliography, " ACM Comput. Surv., vol. 51, no. 1, pp. 17: 1-17: 24, 2018.
B. Finkbeiner and S. Schewe, "Bounded synthesis, " STTT, vol. 15, no. 5-6, pp. 519-539, 2013.
S. Bansal, K. S. Namjoshi, and Y. Sa'ar, "Synthesis of coordination programs from linear temporal specifications, " Proc. ACM Program. Lang., vol. 4, no. POPL, pp. 54: 1-54: 27, 2020. [Online]. Available: Https: //doi. org/10. 1145/3371122
M. Vechev, E. Yahav, and G. Yorsh, "Abstraction-guided synthesis of synchronization, " in Proceedings of the 37th annual ACM SIGPLANSIGACT symposium on Principles of programming languages, 2010, pp. 327-338.
H. Frenkel, O. Grumberg, C. Pasareanu, and S. Sheinvald, "Assume, guarantee or repair, " in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2020, pp. 211-227.
B. Finkbeiner and S. Jacobs, "Lazy synthesis, " in VMCAI, ser. LNCS, vol. 7148. Springer, 2012, pp. 219-234.
J. Esparza, "Keeping a crowd safe: On the complexity of parameterized verification (invited talk), " in STACS, ser. LIPIcs, vol. 25. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2014, pp. 1-10.
R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder, Decidability of Parameterized Verification, ser. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.
E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of model checking. Springer, 2018, vol. 10.
G. Basler, M. Mazzucchi, T. Wahl, and D. Kroening, "Symbolic counter abstraction for concurrent software, " in International Conference on Computer Aided Verification. Springer, 2009, pp. 64-78.
S. Auserlechner, S. Jacobs, and A. Khalimov, "Tight cutoffs for guarded protocols with fairness, " in VMCAI, ser. LNCS, vol. 9583. Springer, 2016, pp. 476-494.
S. Jacobs and M. Sakr, "Analyzing guarded protocols: Better cutoffs, more systems, more expressivity, " in International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 2018, pp. 247-268.
J. Esparza, M. A. Raskin, and C. Weil-Kennedy, "Parameterized analysis of immediate observation petri nets, " in Petri Nets, ser. Lecture Notes in Computer Science, vol. 11522. Springer, 2019, pp. 365-385.
