1. Luca de Alfaro & Pritam Roy (2010): Solving games via three-valued abstraction refinement. Inf. Comput. 208(6), pp. 666–676, doi:10.1016/j.ic.2009.05.007.
  2. Tomás Babiak, Mojmír Kretínský, Vojtech Rehák & Jan Strejcek (2012): LTL to Büchi Automata Translation: Fast and More Deterministic. In: TACAS, LNCS 7214. Springer, pp. 95–109, doi:10.1007/978-3-642-28756-5_8.
  3. Adrian Balint, Daniel Diepold, Daniel Gall, Simon Gerber, Gregor Kapler & Robert Retz (2011): EDACC - An Advanced Platform for the Experiment Design, Administration and Analysis of Empirical Algorithms. In: LION 5. Selected Papers, LNCS 6683. Springer, pp. 586–599, doi:10.1007/978-3-642-25566-3_46.
  4. R. Bloem, R. Könighofer & M. Seidl (2014): SAT-Based Synthesis Methods for Safety Specs. In: VMCAI, LNCS 8318. Springer, pp. 1–20, doi:10.1007/978-3-642-54013-4_1.
  5. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2012): Acacia+, a Tool for LTL Synthesis. In: CAV, LNCS 7358. Springer, pp. 652–657, doi:10.1007/978-3-642-31424-7_45.
  6. Robert K. Brayton & Alan Mishchenko (2010): ABC: An Academic Industrial-Strength Verification Tool. In: CAV, LNCS 6174. Springer, pp. 24–40, doi:10.1007/978-3-642-14295-6_5.
  7. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2014): AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT, EPTCS 157. Open Publishing Association, pp. 100–116, doi:10.4204/EPTCS.157.11.
  8. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2015): Compositional Algorithms for Succinct Safety Games. In: SYNT, EPTCS 202. Open Publishing Association, pp. 98–111, doi:10.4204/EPTCS.202.7.
  9. Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere & Keijo Heljanko (2016): Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. Journal on Satisfiability, Boolean Modeling and Computation 9, pp. 135–172. Available at
  10. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li & Frank Stephan (2017): Deciding parity games in quasipolynomial time. In: Hamed Hatami, Pierre McKenzie & Valerie King: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017. ACM, pp. 252–263, doi:10.1145/3055399.3055409.
  11. Alonzo Church (1962): Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp. 23–35.
  12. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault & Laurent Xu (2016): Spot 2.0 — a framework for LTL and ω-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), LNCS 9938. Springer, pp. 122–129, doi:10.1007/978-3-319-46520-3_8.
  13. Rüdiger Ehlers (2012): Symbolic bounded synthesis. Formal Methods in System Design 40(2), pp. 232–262, doi:10.1007/s10703-011-0137-x.
  14. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe & Leander Tentrup (2017): Encodings of Bounded Synthesis. In: TACAS (1), LNCS 10205, pp. 354–370, doi:10.1007/978-3-662-54577-5_20.
  15. Peter Faymonville, Bernd Finkbeiner & Leander Tentrup (2017): BoSy: An Experimentation Framework for Bounded Synthesis. In: CAV (2), LNCS 10427. Springer, pp. 325–332, doi:10.1007/978-3-319-63390-9_17.
  16. Bernd Finkbeiner & Felix Klein (2016): Bounded Cycle Synthesis. In: CAV (1), LNCS 9779. Springer, pp. 118–135, doi:10.1007/978-3-319-41528-4_7.
  17. Bernd Finkbeiner, Markus N. Rabe & César Sánchez (2015): Algorithms for Model Checking HyperLTL and HyperCTL*. In: CAV, LNCS 9206. Springer, pp. 30–48, doi:10.1007/978-3-319-21690-4_3.
  18. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. STTT 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
  19. Johann Glaser & Clifford Wolf (2014): Methodology and Example-Driven Interconnect Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable Architectures, pp. 201–221. Springer International Publishing, Cham, doi:10.1007/978-3-319-01418-0_12.
  20. Swen Jacobs (2014): Extended AIGER Format for Synthesis. CoRR abs/1405.5793. Available at
  21. Swen Jacobs & Roderick Bloem (2016): The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond. In: SYNT@CAV 2016, EPTCS 229, pp. 133–148, doi:10.4204/EPTCS.229.11.
  22. Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2017): The first reactive synthesis competition (SYNTCOMP 2014). STTT 19(3), pp. 367–390, doi:10.1007/s10009-016-0416-3.
  23. Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016): The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results. In: SYNT@CAV, EPTCS 229, pp. 149–177, doi:10.4204/EPTCS.229.12.
  24. Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016): The Second Reactive Synthesis Competition (SYNTCOMP 2015). In: SYNT, EPTCS 202. Open Publishing Association, pp. 27–57, doi:10.4204/EPTCS.202.4.
  25. Swen Jacobs, Felix Klein & Sebastian Schirmer (2016): A High-Level LTL Synthesis Format: TLSF v1.1. In: SYNT@CAV 2016, EPTCS 229, pp. 112–132, doi:10.4204/EPTCS.229.10.
  26. Mikolás Janota, William Klieber, Joao Marques-Silva & Edmund M. Clarke (2016): Solving QBF with counterexample guided refinement. Artif. Intell. 234, pp. 1–25, doi:10.1016/j.artint.2016.01.004.
  27. Barbara Jobstmann (2007): Applications and Optimizations for LTL Synthesis. Graz University of Technology.
  28. Barbara Jobstmann & Roderick Bloem (2006): Optimizations for LTL Synthesis. In: FMCAD. IEEE Computer Society, pp. 117–124, doi:10.1109/FMCAD.2006.22.
  29. Ayrat Khalimov (2015): Specification Format for Reactive Synthesis Problems. In: SYNT, EPTCS 202. Open Publishing Association, pp. 112–119, doi:10.4204/EPTCS.202.8.
  30. Ayrat Khalimov, Swen Jacobs & Roderick Bloem (2013): PARTY Parameterized Synthesis of Token Rings. In: CAV, LNCS 8044. Springer, pp. 928–933, doi:10.1007/978-3-642-39799-8_66.
  31. Ayrat Khalimov, Swen Jacobs & Roderick Bloem (2013): Towards Efficient Parameterized Synthesis. In: VMCAI, LNCS 7737. Springer, pp. 108–127, doi:10.1007/978-3-642-35873-9_9.
  32. Alexander Legg, Nina Narodytska & Leonid Ryzhyk (2016): A SAT-Based Counterexample Guided Method for Unbounded Synthesis. In: CAV (2), LNCS 9780. Springer, pp. 364–382, doi:10.1007/978-3-319-41540-6_20.
  33. Jia Hui Liang, Vijay Ganesh, Pascal Poupart & Krzysztof Czarnecki (2016): Learning Rate Based Branching Heuristic for SAT Solvers. In: Nadia Creignou & Daniel Le Berre: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Lecture Notes in Computer Science 9710. Springer, pp. 123–140, doi:10.1007/978-3-319-40970-2_9.
  34. Donald A. Martin (1975): Borel Determinacy. Annals of Mathematics 102(2), pp. 363–371.
  35. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: TACAS, LNCS 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  36. Roman R. Redziejowski (2012): An Improved Construction of Deterministic Omega-automaton Using Derivatives. Fundam. Inform. 119(3-4), pp. 393–406, doi:10.3233/FI-2012-744.
  37. Olivier Roussel (2011): Controlling a Solver Execution with the runsolver Tool. JSAT 7(4), pp. 139–144. Available at
  38. Leonid Ryzhyk, Adam Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm & Mona Vij (2014): User-Guided Device Driver Synthesis. In: OSDI. USENIX Association, pp. 661–676. Available at
  39. M. Seidl & R. Könighofer (2014): Partial witnesses from preprocessed quantified Boolean formulas. In: DATE'14. IEEE, pp. 1–6, doi:10.7873/DATE2014.162.
  40. Leander Tentrup (2016): Solving QBF by Abstraction. CoRR abs/1604.06752. Available at
  41. Cong Tian, Jun Song, Zhenhua Duan & Zhao Duan (2015): LtlNfBa: Making LTL Translation More Practical. In: SOFL+MSVL, LNCS 9559. Springer, pp. 179–194, doi:10.1007/978-3-319-31220-0_13.
  42. James C. Tiernan (1970): An efficient search algorithm to find the elementary circuits of a graph. Commun. ACM 13(12), pp. 722–726, doi:10.1145/362814.362819.
  43. Cheng-Yin Wu, Chi-An Wu, Chien-Yu Lai & Chung-Yang R. Haung (2014): A Counterexample-Guided Interpolant Generation Algorithm for SAT-Based Model Checking. IEEE Trans. on CAD of Integrated Circuits and Systems 33(12), pp. 1846–1858, doi:10.1109/TCAD.2014.2363395.
  44. Wieslaw Zielonka (1998): Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theor. Comput. Sci. 200(1-2), pp. 135–183, doi:10.1016/S0304-3975(98)00009-7.

Comments and questions to:
For website issues: