[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

The Reactive Synthesis Competition (SYNTCOMP): 2018–2021

  • Competitions and Challenges
  • Regular
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018–2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality—that is, the total size in terms of logic and memory elements—of solutions.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abraham, R.: Symbolic LTL reactive synthesis (2021). http://essay.utwente.nl/87386/

  2. Apt, K.R., Grädel, E. (eds.): Lectures in Game Theory for Computer Scientists Cambridge University Press, Cambridge (2011). http://www.cambridge.org/gb/knowledge/isbn/item5760379

    Google Scholar 

  3. Babiak, T., Badie, T., Duret-Lutz, A., et al.: Compositional approach to suspension and other improvements to LTL translation. In: Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN’13). Lecture Notes in Computer Science, vol. 7976, pp. 81–98. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-39176-7_6

    Chapter  Google Scholar 

  4. Babiak, T., Blahoudek, F., Duret-Lutz, A., et al.: The Hanoi omega-automata format. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification – 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015. Proceedings, Part I, Lecture Notes in Computer Science, vol. 9206, pp. 479–486. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-21690-4_31

    Chapter  Google Scholar 

  5. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    Google Scholar 

  6. Balint, A., Diepold, D., Gall, D., et al.: EDACC – an advanced platform for the experiment design, administration and analysis of empirical algorithms. In: Coello, C.A.C. (ed.) Selected Papers, Learning and Intelligent Optimization – 5th International Conference, LION 5, Rome, Italy, January 17–21, 2011. Lecture Notes in Computer Science, vol. 6683, pp. 586–599. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-25566-3_46

    Chapter  Google Scholar 

  7. Biere, A.: Hardware model checking competition (2007). http://fmv.jku.at/hwmcc/

  8. Biere, A.: Aiger format and toolbox (2011). http://fmv.jku.at/aiger/

  9. Bloem, R., Könighofer, R., Seidl, M.: Sat-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19–21, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8318, pp. 1–20. Springer, Berlin (2014). https://doi.org/10.1007/978-3-642-54013-4_1

    Chapter  Google Scholar 

  10. Bohy, A.: Antichain based algorithms for the synthesis of reactive systems. PhD thesis, University of Mons (2014)

  11. Bohy, A., Bruyère, V., Filiot, E., et al.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV, LNCS, vol. 7358, pp. 652–657. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-31424-7_45

    Chapter  Google Scholar 

  12. Boker, U., Kupferman, O., Steinitz, A.: Parityizing rabin and streett. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, Chennai, India, December 15-18, 2010, LIPIcs, vol. 8, pp. 412–423. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010). https://doi.org/10.4230/LIPIcs.FSTTCS.2010.412

    Chapter  Google Scholar 

  13. Bruyère, V., Pérez, G.A., Raskin, J., et al.: Partial solvers for generalized parity games. In: Filiot, E., Jungers, R.M., Potapov, I. (eds.) Reachability Problems – 13th International Conference, RP 2019, Brussels, Belgium, September 11–13, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11674, pp. 63–78. Springer, Berlin (2019). https://doi.org/10.1007/978-3-030-30806-3_6

    Chapter  Google Scholar 

  14. Cadilhac, M., Pérez, G.A.: Acacia-bonsai: a modern implementation of downset-based LTL realizability. In: Tools and Algorithms for the Construction and Analysis of Systems – 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023. Paris, France, April 22-27, 2023, Proceedings, Part II, Lecture Notes in Computer Science, vol. 13994, pp. 192–207. Springer, Berlin (2023).

    Google Scholar 

  15. Camacho, A., Muise, C.J., Baier, J.A., et al.: LTL realizability via safety and reachability games. In: IJCAI. ijcai.org pp. 4683–4691 (2018)

    Google Scholar 

  16. Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using Muller conditions. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, Glasgow, Scotland (Virtual Conference), July 12–16, 2021, LIPIcs, vol. 198, pp. 123:1–123:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.ICALP.2021.123

    Chapter  Google Scholar 

  17. Casares, A., Duret-Lutz, A., Meyer, K.J., et al.: Practical applications of the alternating cycle decomposition. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems – 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022. Proceedings, Part II, Lecture Notes in Computer Science, vol. 13244, pp. 99–117. Springer, Berlin (2022). https://doi.org/10.1007/978-3-030-99527-0_6

    Chapter  Google Scholar 

  18. Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: Seidl, H. (ed.) Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24–April 1, 2007. Proceedings, Lecture Notes in Computer Science, vol. 4423, pp. 153–167. Springer, Berlin (2007). https://doi.org/10.1007/978-3-540-71389-0_12

    Chapter  Google Scholar 

  19. Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. 1, pp. 3–50. Am. Math. Soc., Providence (1957)

    Google Scholar 

  20. Church, A.: Logic, arithmetic, and automata. J. Symb. Log. 29(4) (1964)

  21. Clarke, E.M., Henzinger, T.A., Veith, H., et al. (eds.): Handbook of Model Checking Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-10575-8

    Book  Google Scholar 

  22. de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. Inf. Comput. 208(6), 666–676 (2010). https://doi.org/10.1016/j.ic.2009.05.007

    Article  MathSciNet  Google Scholar 

  23. De Berg, M., Cheong, O., van Kreveld, M.J., et al.: Computational Geometry: Algorithms and Applications, 3rd edn. Springer, Berlin (2008). https://www.worldcat.org/oclc/227584184

    Book  Google Scholar 

  24. Duret-Lutz, A., Lewkowicz, A., Fauchille, A., et al.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16). Lecture Notes in Computer Science, vol. 9938, pp. 122–129. Springer, Berlin (2016). https://doi.org/10.1007/978-3-319-46520-3_8

    Chapter  Google Scholar 

  25. Ehlers, R.: Symbolic bounded synthesis. In: International Conference on Computer Aided Verification, pp. 365–379. Springer, Berlin (2010)

    Chapter  Google Scholar 

  26. Ehlers, R.: Unbeast: symbolic bounded synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 272–275. Springer, Berlin (2011)

    Google Scholar 

  27. Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’18), pp. 384–393. ACM, New York (2018). https://doi.org/10.1145/3209108.3209161

    Chapter  Google Scholar 

  28. Esparza, J., Kretínský, J., Sickert, S.: A unified translation of linear temporal logic to \(\omega \)-automata. J. ACM 67(6), 33:1–33:61 (2020). https://doi.org/10.1145/3417995

    Article  MathSciNet  Google Scholar 

  29. Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification – 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017. Proceedings, Part II, Lecture Notes in Computer Science, vol. 10427, pp. 325–332. Springer, Berlin (2017). https://doi.org/10.1007/978-3-319-63390-9_17

    Chapter  Google Scholar 

  30. Finkbeiner, B., Klein, F.: Bounded cycle synthesis. In: Chaudhuri, S., Farzan, A. (eds.) Proceedings, Part I, Computer Aided Verification – 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17–23, 2016. Lecture Notes in Computer Science, vol. 9779, pp. 118–135. Springer, Berlin (2016). https://doi.org/10.1007/978-3-319-41528-4_7

    Chapter  Google Scholar 

  31. Finkbeiner, B., Klein, F., Piskac, R., et al.: Synthesizing functional reactive programs. In: Eisenberg, R.A. (ed.) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019, pp. 162–175. ACM, New York (2019). https://doi.org/10.1145/3331545.3342601

    Chapter  Google Scholar 

  32. Finkbeiner, B., Klein, F., Piskac, R., et al.: Temporal stream logic: synthesis beyond the bools. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification – 31st International Conference, CAV 2019, New York City, NY, USA, July 15–18, 2019. Proceedings, Part I, Lecture Notes in Computer Science, vol. 11561, pp. 609–629. Springer, Berlin (2019). https://doi.org/10.1007/978-3-030-25540-4_35

    Chapter  Google Scholar 

  33. Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. In: Proceedings for the 13th NASA Formal Methods Symposium (NFM’21) (2021). https://doi.org/10.1007/978-3-030-76384-8_8

    Chapter  Google Scholar 

  34. Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14–16, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5799, pp. 182–196. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-04761-9_15

    Chapter  Google Scholar 

  35. Geier, G., Heim, P., Klein, F., et al.: Syntroids: synthesizing a game for FPGAs using temporal logic specifications. In: Barrett, C.W., Yang, J. (eds.) Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22–25, 2019, pp. 138–146. IEEE, Los Alamitos (2019). https://doi.org/10.23919/FMCAD.2019.8894261

    Chapter  Google Scholar 

  36. Jacobs, S.: Extended AIGER format for synthesis. CoRR (2014). http://arxiv.org/abs/1405.5793. arXiv:1405.5793

  37. Jacobs, S., Perez, G.A.: Data and scripts used for the SYNTCOMP report 2018–2021 (2023). https://doi.org/10.5281/zenodo.7588780

  38. Jacobs, S., Sakr, M.: AIGEN: random generation of symbolic transition systems. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification – 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 435–446. Springer, Berlin (2021). https://doi.org/10.1007/978-3-030-81688-9_20

    Chapter  Google Scholar 

  39. Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17–18, 2016, pp. 112–132 (2016). https://doi.org/10.4204/EPTCS.229.10

    Chapter  Google Scholar 

  40. Jacobs, S., Basset, N., Bloem, R., et al.: The 4th reactive synthesis competition (SYNTCOMP 2017): benchmarks, participants & results. In: Fisman, D., Jacobs, S. (eds.) Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, pp. 116–143 (2017). https://doi.org/10.4204/EPTCS.260.10

    Chapter  Google Scholar 

  41. Jacobs, S., Bloem, R., Brenguier, R., et al.: The first reactive synthesis competition (SYNTCOMP 2014). Int. J. Softw. Tools Technol. Transf. 19(3), 367–390 (2017) https://doi.org/10.1007/s10009-016-0416-3

    Article  Google Scholar 

  42. Kretínský, J., Meggendorfer, T., Sickert, S.: Owl: a library for \(\omega \)-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis – 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7–10, 2018. Proceedings, Lecture Notes in Computer Science, vol. 11138, pp. 543–550. Springer, Berlin (2018). https://doi.org/10.1007/978-3-030-01090-4_34

    Chapter  Google Scholar 

  43. Lijzenga, O., van Dijk, T.: Symbolic parity game solvers that yield winning strategies. In: Raskin, J., Bresolin, D. (eds.) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21–22, 2020, pp. 18–32 (2020). https://doi.org/10.4204/EPTCS.326.2

    Chapter  Google Scholar 

  44. Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games. CoRR (2008). http://arxiv.org/abs/0806.2923. arXiv:0806.2923

  45. Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Inform. 57(1–2), 3–36 (2020). https://doi.org/10.1007/s00236-019-00349-3

    Article  MathSciNet  Google Scholar 

  46. Meyer, P.J., Sickert, S.: Modernising Strix. Presented at the 10th Workshop on Synthesis (2021)

  47. Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings, Part I, Lecture Notes in Computer Science, vol. 10981, pp. 578–586. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-96145-3_31

    Chapter  Google Scholar 

  48. Müller, D., Sickert, S.: LTL to deterministic Emerson–Lei automata. In: Bouyer, P., Orlandini, A., Pietro, P.S. (eds.) Proceedings of the Eighth International Symposium on Games, Automata, Logics and Formal Verification (GandALF’17), pp. 180–194 (2017). https://doi.org/10.4204/EPTCS.256.13

    Chapter  Google Scholar 

  49. Pérez, G.A.: The extended HOA format for synthesis. CoRR (2019). http://arxiv.org/abs/1912.05793. arXiv:1912.05793

  50. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). https://doi.org/10.2168/LMCS-3(3:5)2007

  51. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, 31 October–1 November 1977, pp. 46–57. IEEE Comput. Soc., Providence (1977). https://doi.org/10.1109/SFCS.1977.32

    Chapter  Google Scholar 

  52. Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical “paritizing” of Emerson–Lei automata. In: Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA’20). Lecture Notes in Computer Science, vol. 12302, pp. 127–143. Springer, Berlin (2020). https://doi.org/10.1007/978-3-030-59152-6_7

    Chapter  Google Scholar 

  53. Renkin, F., Schlehuber, P., Duret-Lutz, A., et al.: Improvements to ltlsynt. Presented at the 10th Workshop on Synthesis (2021) https://hal.archives-ouvertes.fr/hal-03523385

  54. Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., et al.: Effective reductions of Mealy machines. In: Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE’22). Lecture Notes in Computer Science, vol. 13273, pp. 114–130. Springer, Berlin (2022).

    Chapter  Google Scholar 

  55. Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, 24–26 October 1988, pp. 319–327. IEEE Comput. Soc., New York (1988). https://doi.org/10.1109/SFCS.1988.21948

    Chapter  Google Scholar 

  56. Seidl, M., Könighofer, R.: Partial witnesses from preprocessed quantified Boolean formulas. In: Fettweis, G.P., Nebel, W. (eds.) Design, Automation & Test in Europe Conference & Exhibition, DATE 2014, Dresden, Germany, March 24–28, 2014. European Design and Automation Association, pp. 1–6 (2014). https://doi.org/10.7873/DATE.2014.162

    Chapter  Google Scholar 

  57. Sickert, S., Esparza, J.: An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: Hermanns, H., Zhang, L., Kobayashi, N., et al. (eds.) LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8–11, 2020, pp. 831–844. ACM, New York (2020). https://doi.org/10.1145/3373718.3394743

    Chapter  Google Scholar 

  58. Somenzi, F.: CUDD package, release 2.4.1 (2005). http://vlsi.colorado.edu/~fabio/CUDD/

  59. Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning – 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19–22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 367–373. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-08587-6_28

    Chapter  Google Scholar 

  60. Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: SAT, Lecture Notes in Computer Science, vol. 11628, pp. 388–405. Springer, Berlin (2019)

    Google Scholar 

  61. Van Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), pp. 291–308. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-89960-2_16

    Chapter  Google Scholar 

  62. Van Dijk, T., Rubbens, B.: Simple fixpoint iteration to solve parity games. In: Leroux, J., Raskin, J. (eds.) Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019, Bordeaux, France, 2–3 September 2019, pp. 123–139 (2019). https://doi.org/10.4204/EPTCS.305.9

    Chapter  Google Scholar 

  63. Van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675–696 (2017). https://doi.org/10.1007/s10009-016-0433-2

    Article  Google Scholar 

  64. Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs (extended abstract). In: DeMillo, R.A. (ed.) Proceedings of the 16th Annual ACM Symposium on Theory of Computing, Washington, DC, USA, April 30–May 2, 1984, pp. 446–456. ACM, New York (1984). https://doi.org/10.1145/800057.808711

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CISPA Helmholtz Center for Information Security, Stuhlsatzenhaus 5, Saarbrücken, 66123, Germany

    Swen Jacobs & Bernd Finkbeiner

  2. University of Antwerp – Flanders Make, Middelheimlaan 1, Antwerpen, 2020, Belgium

    Guillermo A. Pérez

  3. University of Twente, Enschede, The Netherlands

    Remco Abraham & Tom van Dijk

  4. University of Mons, Mons, Belgium

    Véronique Bruyère, Charly Delfosse, Gaëtan Staquet & Clément Tamines

  5. DePaul University, Chicago, USA

    Michaël Cadilhac

  6. EPITA Research Laboratory, Kremlin-Bicêtre, France

    Maximilien Colange, Alexandre Duret-Lutz, Thibaud Michaud, Adrien Pommellet, Florian Renkin & Philipp Schlehuber-Caissier

  7. Saarland University, Saarbrücken, Germany

    Peter Faymonville, Felix Klein & Leander Tentrup

  8. Université libre de Bruxelles, Brussels, Belgium

    Ayrat Khalimov

  9. Technische Universität, München, Germany

    Michael Luttenberger, Klara Meyer & Salomon Sickert

  10. University of Luxembourg, Luxembourg, Luxembourg

    Mouhammad Sakr

  11. Independent Researcher, Sydney, Australia

    Adam Walker

Authors
  1. Swen Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Guillermo A. Pérez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Remco Abraham
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Véronique Bruyère
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Michaël Cadilhac
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Maximilien Colange
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Charly Delfosse
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Tom van Dijk
    View author publications

    You can also search for this author in PubMed Google Scholar

  9. Alexandre Duret-Lutz
    View author publications

    You can also search for this author in PubMed Google Scholar

  10. Peter Faymonville
    View author publications

    You can also search for this author in PubMed Google Scholar

  11. Bernd Finkbeiner
    View author publications

    You can also search for this author in PubMed Google Scholar

  12. Ayrat Khalimov
    View author publications

    You can also search for this author in PubMed Google Scholar

  13. Felix Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

  14. Michael Luttenberger
    View author publications

    You can also search for this author in PubMed Google Scholar

  15. Klara Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  16. Thibaud Michaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  17. Adrien Pommellet
    View author publications

    You can also search for this author in PubMed Google Scholar

  18. Florian Renkin
    View author publications

    You can also search for this author in PubMed Google Scholar

  19. Philipp Schlehuber-Caissier
    View author publications

    You can also search for this author in PubMed Google Scholar

  20. Mouhammad Sakr
    View author publications

    You can also search for this author in PubMed Google Scholar

  21. Salomon Sickert
    View author publications

    You can also search for this author in PubMed Google Scholar

  22. Gaëtan Staquet
    View author publications

    You can also search for this author in PubMed Google Scholar

  23. Clément Tamines
    View author publications

    You can also search for this author in PubMed Google Scholar

  24. Leander Tentrup
    View author publications

    You can also search for this author in PubMed Google Scholar

  25. Adam Walker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Swen Jacobs or Guillermo A. Pérez.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Jacobs, S., Pérez, G.A., Abraham, R. et al. The Reactive Synthesis Competition (SYNTCOMP): 2018–2021. Int J Softw Tools Technol Transfer 26, 551–567 (2024). https://doi.org/10.1007/s10009-024-00754-1

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-024-00754-1

Keywords