@misc(termite,
 title        = {Termite Driver Synthesis Tool},
 howpublished = {\url{http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/}},
)
@misc(V3,
 title        = {V3 - An Extensible Framework for Hardware Verification},
 howpublished = {\url{http://dvlab.ee.ntu.edu.tw/~publication/V3/}},
)
@inproceedings(dealfaro,
 author       = {Luca de Alfaro and Pritam Roy},
 year         = {2007},
 title        = {Solving Games Via Three-Valued Abstraction Refinement},
 booktitle    = {CONCUR},
 series       = {LNCS},
 volume       = {4703},
 publisher    = {Springer},
 pages        = {74--89},
 doi          = {10.1007/978-3-540-74407-8\_6},
)
@article(AlurMN05,
 author       = {Rajeev Alur and P. Madhusudan and Wonhong Nam},
 year         = {2005},
 title        = {Symbolic computational techniques for solving games},
 journal      = {{STTT}},
 volume       = {7},
 number       = {2},
 pages        = {118--128},
 doi          = {10.1007/s10009-004-0179-0},
)
@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},
)
@manual(aiger,
 author       = {Armin Biere},
 title        = {{AIGER} Format and Toolbox},
 address      = {\url{http://fmv.jku.at/aiger/}},
)
@manual(HWMCC,
 author       = {Armin Biere},
 title        = {Hardware Model Checking Competition},
 address      = {\url{http://fmv.jku.at/hwmcc/}},
)
@inproceedings(BloemEKKL14,
 author       = {R. Bloem and U. Egly and P. Klampfl and R. K{\"{o}}nighofer and F. Lonsing},
 year         = {2014},
 title        = {{SAT}-based methods for circuit synthesis},
 booktitle    = {FMCAD'14},
 publisher    = {IEEE},
 pages        = {31--34},
 doi          = {10.1109/FMCAD.2014.6987592},
)
@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(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},
)
@manual(IIMC,
 author       = {Aaron Bradley and Fabio Somenzi and Michael Dooley and Zyad Hassan and Yan Zhang},
 title        = {Incremental Inductive Model Checker},
 address      = {\url{http://ecee.colorado.edu/wpmu/iimc/}},
)
@inproceedings(Bradley11,
 author       = {Aaron R. Bradley},
 year         = {2011},
 title        = {{SAT}-Based Model Checking without Unrolling},
 booktitle    = {VMCAI},
 series       = {LNCS},
 volume       = {6538},
 publisher    = {Springer},
 pages        = {70--87},
 doi          = {10.1007/978-3-642-18275-4\_7},
)
@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},
 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       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
 publisher    = {Open Publishing Association},
)
@article(bryant86,
 author       = {Randal E. Bryant},
 year         = {1986},
 title        = {Graph-Based Algorithms for Boolean Function Manipulation},
 journal      = {{IEEE} Trans. Computers},
 volume       = {35},
 number       = {8},
 pages        = {677--691},
 doi          = {10.1109/TC.1986.1676819},
)
@article(BL69,
 author       = {J.R. B\"uchi and L.H. Landweber},
 year         = {1969},
 title        = {Solving sequential conditions by finite-state strategies},
 journal      = {Trans. Amer. Math. Soc.},
 volume       = {138},
 pages        = {295--311},
 doi          = {10.2307/1994916},
)
@article(ChenDSB12,
 author       = {Yushan Chen and Xu Chu Ding and Alin Stefanescu and Calin Belta},
 year         = {2012},
 title        = {Formal Approach to the Deployment of Distributed Robotic Teams},
 journal      = {{IEEE} Transactions on Robotics},
 volume       = {28},
 number       = {1},
 pages        = {158--171},
 doi          = {10.1109/TRO.2011.2163434},
)
@inproceedings(ChinchaliLTBM12,
 author       = {Sandeep Chinchali and Scott C. Livingston and Ufuk Topcu and Joel W. Burdick and Richard M. Murray},
 year         = {2012},
 title        = {Towards formal synthesis of reactive controllers for dexterous robotic manipulation},
 booktitle    = {{ICRA}},
 publisher    = {{IEEE}},
 pages        = {5183--5189},
 doi          = {10.1109/ICRA.2012.6225257},
)
@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(EmersonC82,
 author       = {E. Allen Emerson and Edmund M. Clarke},
 year         = {1982},
 title        = {Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons},
 journal      = {Sci. Comput. Program.},
 volume       = {2},
 number       = {3},
 pages        = {241--266},
 doi          = {10.1016/0167-6423(83)90017-5},
)
@manual(acacia,
 author       = {Emmanuel Filiot},
 title        = {Acacia+},
 address      = {\url{http://lit2.ulb.ac.be/acaciaplus/}},
)
@inproceedings(fjr10,
 author       = {Emmanuel Filiot and Naiyong Jin and Jean{-}Fran{\c{c}}ois Raskin},
 year         = {2010},
 title        = {Compositional Algorithms for {LTL} Synthesis},
 booktitle    = {{ATVA}},
 series       = {LNCS},
 volume       = {6252},
 publisher    = {Springer},
 pages        = {112--127},
 doi          = {10.1007/978-3-642-15643-4\_10},
)
@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(Huffman52,
 author       = {David A. Huffman},
 year         = {1952},
 title        = {A Method for the Construction of Minimum-Redundancy Codes},
 journal      = {Proceedings of the IRE},
 volume       = {40},
 number       = {9},
 pages        = {1098--1101},
 doi          = {10.1109/JRPROC.1952.273898},
)
@article(Jacobs15,
 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         = {2015},
 title        = {The First Reactive Synthesis Competition {(SYNTCOMP} 2014)},
 journal      = {CoRR},
 volume       = {abs/1506.08726},
 url          = {http://arxiv.org/abs/1506.08726},
)
@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},
)
@misc(aisy,
 author       = {Ayrat Khalimov},
 title        = {Aisy: {S}imple synthesis tool from {AIGER} circuits format.},
 howpublished = {\url{https://bitbucket.org/art_haali/aisy-classroom}},
)
@inproceedings(Khalimov15,
 author       = {Ayrat Khalimov},
 year         = {2015},
 title        = {Specification Format for Reactive Synthesis Problems},
 booktitle    = {SYNT},
 series       = {this volume of EPTCS},
 publisher    = {Open Publishing Association},
 publisher    = {Open Publishing Association},
)
@article(Kress-GazitFP09,
 author       = {Kress{-}Gazit, Hadas and Georgios E. Fainekos and George J. Pappas},
 year         = {2009},
 title        = {Temporal-Logic-Based Reactive Mission and Motion Planning},
 journal      = {{IEEE} Transactions on Robotics},
 volume       = {25},
 number       = {6},
 pages        = {1370--1381},
 doi          = {10.1109/TRO.2009.2030225},
)
@inproceedings(LonsingE14,
 author       = {Florian Lonsing and Uwe Egly},
 year         = {2014},
 title        = {Incremental {QBF} Solving},
 booktitle    = {CP},
 series       = {LNCS},
 volume       = {8656},
 publisher    = {Springer},
 pages        = {514--530},
 doi          = {10.1007/978-3-319-10428-7\_38},
)
@incollection(SMVSystem,
 author       = {Kenneth L. McMillan},
 year         = {1993},
 title        = {The SMV System},
 booktitle    = {Symbolic Model Checking},
 publisher    = {Springer},
 pages        = {61--85},
 doi          = {10.1007/978-1-4615-3190-6\_4},
)
@techreport(SMVLang,
 author       = {Kenneth L McMillan},
 year         = {1999},
 title        = {The SMV language},
 type         = {Technical Report},
 institution  = {Cadence Berkeley Labs},
 url          = {http://web.cs.wpi.edu/~kfisler/Courses/525V/S02/Readings/smv-cadence.pdf},
)
@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},
)
@misc(attoparsec,
 author       = {Bryan O'Sullivan},
 title        = {Attoparsec},
 howpublished = {\url{https://hackage.haskell.org/package/attoparsec}},
)
@inproceedings(PnueliR89,
 author       = {Amir Pnueli and Roni Rosner},
 year         = {1989},
 title        = {On the Synthesis of a Reactive Module},
 booktitle    = {POPL},
 publisher    = {{ACM} Press},
 pages        = {179--190},
 doi          = {10.1145/75277.75293},
)
@article(Rabin69,
 author       = {Michael O. Rabin},
 year         = {1969},
 title        = {Decidability of second-order theories and automata on infinite trees},
 journal      = {Trans. Amer. Math. Soc.},
 volume       = {141},
 pages        = {1--35},
 doi          = {10.1090/S0002-9947-1969-0246760-1},
)
@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},
 doi          = {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},
)
@inproceedings(Thomas95,
 author       = {Wolfgang Thomas},
 year         = {1995},
 title        = {On the Synthesis of Strategies in Infinite Games},
 booktitle    = {{STACS}},
 pages        = {1--13},
 doi          = {10.1007/3-540-59042-0\_57},
)
@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},
)