@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(AudemardS09,
 author       = {Gilles Audemard and Laurent Simon},
 year         = {2009},
 title        = {Predicting Learnt Clauses Quality in Modern {SAT} Solvers},
 booktitle    = {{IJCAI}},
 pages        = {399--404},
 url          = {http://ijcai.org/Proceedings/09/Papers/074.pdf},
)
@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},
)
@article(BloemJPPS12,
 author       = {R. Bloem and B. Jobstmann and N. Piterman and A. Pnueli and Y. Sa'ar},
 year         = {2012},
 title        = {Synthesis of Reactive(1) designs},
 journal      = {J. Comput. Syst. Sci.},
 volume       = {78},
 number       = {3},
 pages        = {911--938},
 doi          = {10.1016/j.jcss.2011.08.007},
)
@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},
)
@article(BloemGJPPW07,
 author       = {Roderick Bloem and Stefan J. Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
 year         = {2007},
 title        = {Specify, Compile, Run: Hardware from {PSL}},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {190},
 number       = {4},
 pages        = {3--16},
 doi          = {10.1016/j.entcs.2007.09.004},
)
@inproceedings(BloemJK14a,
 author       = {Roderick Bloem and Swen Jacobs and Ayrat Khalimov},
 year         = {2014},
 title        = {Parameterized Synthesis Case Study: {AMBA} {AHB}},
 booktitle    = {{SYNT}},
 series       = {{EPTCS}},
 volume       = {157},
 pages        = {68--83},
 doi          = {10.4204/EPTCS.157.9},
)
@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(VIS,
 author       = {Robert K. Brayton and Gary D. Hachtel and Sangiovanni{-}Vincentelli, Alberto L. and Fabio Somenzi and Adnan Aziz and Szu{-}Tsung Cheng and Stephen A. Edwards and Sunil P. Khatri and Yuji Kukimoto and Abelardo Pardo and Shaz Qadeer and Rajeev K. Ranjan and Shaker Sarwary and Thomas R. Shiple and Gitanjali Swamy and Tiziano Villa},
 year         = {1996},
 title        = {{VIS:} {A} System for Verification and Synthesis},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {1102},
 publisher    = {Springer},
 pages        = {428--432},
 doi          = {10.1007/3-540-61474-5\_95},
)
@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},
)
@inproceedings(BurchCL91,
 author       = {Jerry R. Burch and Edmund M. Clarke and David E. Long},
 year         = {1991},
 title        = {Symbolic Model Checking with Partitioned Transistion Relations},
 booktitle    = {{VLSI}},
 pages        = {49--58},
)
@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(Church62,
 author       = {Alonzo Church},
 year         = {1962},
 title        = {Logic, arithmetic and automata},
 booktitle    = {Proceedings of the international congress of mathematicians},
 pages        = {23--35},
)
@inproceedings(Ehlers11,
 author       = {R{\"{u}}diger Ehlers},
 year         = {2011},
 title        = {Unbeast: Symbolic Bounded Synthesis},
 booktitle    = {{TACAS}},
 series       = {LNCS},
 volume       = {6605},
 publisher    = {Springer},
 pages        = {272--275},
 doi          = {10.1007/978-3-642-19835-9\_25},
)
@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(FaymonvilleFRT15,
 author       = {Peter Faymonville and Bernd Finkbeiner and Markus N. Rabe and Leander Tentrup},
 year         = {2015},
 title        = {Encodings of Reactive Synthesis},
 booktitle    = {Proceedings of QUANTIFY},
 url          = {http://fmv.jku.at/quantify15/Faymonville-et-al-QUANTIFY2015.pdf},
)
@inproceedings(FinkbeinerJ12,
 author       = {Bernd Finkbeiner and Swen Jacobs},
 year         = {2012},
 title        = {Lazy Synthesis},
 booktitle    = {{VMCAI}},
 series       = {LNCS},
 volume       = {7148},
 publisher    = {Springer},
 pages        = {219--234},
 doi          = {10.1007/978-3-642-27940-9\_15},
)
@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},
)
@inproceedings(go01,
 author       = {Paul Gastin and Denis Oddoux},
 year         = {2001},
 title        = {Fast {LTL} to B{\"u}chi automata translation},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {2102},
 publisher    = {Springer},
 pages        = {53--65},
 doi          = {10.1007/3-540-44585-4\_6},
)
@article(GodhalCH13,
 author       = {Yashdeep Godhal and Krishnendu Chatterjee and Thomas A. Henzinger},
 year         = {2013},
 title        = {Synthesis of {AMBA} {AHB} from formal specification: a case study},
 journal      = {{STTT}},
 volume       = {15},
 number       = {5-6},
 pages        = {585--601},
 doi          = {10.1007/s10009-011-0207-9},
)
@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},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
 publisher    = {Open Publishing Association},
)
@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         = {2016},
 title        = {The First Reactive Synthesis Competition {(SYNTCOMP} 2014)},
 journal      = {STTT},
 doi          = {10.1007/s10009-016-0416-3},
 note         = {Published online first, journal issue to appear.},
)
@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} 2016},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
 publisher    = {Open Publishing Association},
)
@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(MorgensternGS13,
 author       = {A. Morgenstern and M. Gesell and K. Schneider},
 year         = {2013},
 title        = {Solving Games Using Incremental Induction},
 booktitle    = {IFM'13},
 series       = {LNCS 7940},
 publisher    = {Springer},
 pages        = {177--191},
 doi          = {10.1007/978-3-642-38613-8\_13},
)
@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},
)
@inproceedings(PandaS95,
 author       = {Shipra Panda and Fabio Somenzi},
 year         = {1995},
 title        = {Who are the variables in your neighborhood},
 booktitle    = {{ICCAD}},
 publisher    = {{IEEE} Computer Society / {ACM}},
 pages        = {74--77},
 doi          = {10.1109/ICCAD.1995.479994},
)
@inproceedings(RolliniAFHS13,
 author       = {Simone Fulvio Rollini and Leonardo Alt and Grigory Fedyukovich and Antti Eero Johannes Hyv{\"{a}}rinen and Natasha Sharygina},
 year         = {2013},
 title        = {PeRIPLO: {A} Framework for Producing Effective Interpolants in SAT-Based Software Verification},
 booktitle    = {{LPAR}},
 series       = {LNCS},
 volume       = {8312},
 publisher    = {Springer},
 pages        = {683--693},
 doi          = {10.1007/978-3-642-45221-5\_45},
)
@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(Rudell93,
 author       = {Richard Rudell},
 year         = {1993},
 title        = {Dynamic variable ordering for ordered binary decision diagrams},
 booktitle    = {ICCAD},
 publisher    = {{IEEE} Computer Society},
 pages        = {42--47},
 doi          = {10.1145/259794.259802},
)
@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},
 url          = {http://dx.doi.org/10.7873/DATE2014.162},
)
@incollection(somenzi99,
 author       = {Fabio Somenzi},
 year         = {1999},
 title        = {Binary Decision Diagrams},
 booktitle    = {Calculational system design},
 volume       = {173},
 publisher    = {IOS Press},
 pages        = {303},
)
@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(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},
)