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