@article(BJP+12,
 author       = {Roderick Bloem and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Yaniv 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},
)
@article(BrowneCJLM97,
 author       = {Anca Browne and Edmund M. Clarke and Somesh Jha and David E. Long and Wilfredo R. Marrero},
 year         = {1997},
 title        = {An Improved Algorithm for the Evaluation of Fixpoint Expressions},
 journal      = {Theor. Comput. Sci.},
 volume       = {178},
 number       = {1-2},
 pages        = {237--255},
 doi          = {10.1016/S0304-3975(96)00228-9},
)
@proceedings(DBLP:journals/corr/CernyKM16,
 editor       = {Pavol Cern{\'{y}} and Viktor Kuncak and Parthasarathy Madhusudan},
 year         = {2016},
 title        = {Proceedings Fourth Workshop on Synthesis, {SYNT} 2015, San Francisco, CA, USA, 18th July 2015},
 series       = {{EPTCS}},
 volume       = {202},
 doi          = {10.4204/EPTCS.202},
)
@inproceedings(CimattiRST08,
 author       = {Alessandro Cimatti and Marco Roveri and Viktor Schuppan and Andrei Tchaltsev},
 year         = {2008},
 title        = {Diagnostic Information for Realizability},
 booktitle    = {VMCAI},
 series       = {LNCS},
 volume       = {4905},
 publisher    = {Springer},
 pages        = {52--67},
 doi          = {10.1007/978-3-540-78163-9_9},
)
@article(DIppolitoBPU13,
 author       = {Nicol{\'{a}}s D'Ippolito and V{\'{\i}}ctor A. Braberman and Nir Piterman and Sebasti{\'{a}}n Uchitel},
 year         = {2013},
 title        = {Synthesizing nonanomalous event-based controllers for liveness goals},
 journal      = {{ACM} Trans. Softw. Eng. Methodol.},
 volume       = {22},
 number       = {1},
 pages        = {9},
 doi          = {10.1145/2430536.2430543},
)
@inproceedings(DAC99,
 author       = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett},
 year         = {1999},
 title        = {Patterns in Property Specifications for Finite-State Verification},
 booktitle    = {ICSE},
 publisher    = {{ACM}},
 pages        = {411--420},
 doi          = {10.1145/302405.302672},
)
@inproceedings(Ehlers11,
 author       = {R{\"{u}}diger Ehlers},
 year         = {2011},
 title        = {Generalized {R}abin(1) Synthesis with Applications to Robust System Synthesis},
 booktitle    = {{NASA} Formal Methods},
 series       = {LNCS},
 volume       = {6617},
 publisher    = {Springer},
 pages        = {101--115},
 doi          = {10.1007/978-3-642-20398-5\_9},
)
@inproceedings(EhlersR16,
 author       = {R{\"{u}}diger Ehlers and Vasumathi Raman},
 year         = {2016},
 title        = {Slugs: Extensible {GR(1)} Synthesis},
 editor       = {Swarat Chaudhuri and Azadeh Farzan},
 booktitle    = {Computer Aided Verification - 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9780},
 publisher    = {Springer},
 pages        = {333--339},
 doi          = {10.1007/978-3-319-41540-6_18},
)
@inproceedings(FilippidisMH16,
 author       = {Ioannis Filippidis and Richard M. Murray and Gerard J. Holzmann},
 year         = {2015},
 title        = {A multi-paradigm language for reactive synthesis},
 editor       = {Cern{\'{y}}},
 pages        = {73--97},
 doi          = {10.4204/EPTCS.202.6},
)
@proceedings(2001automata,
 editor       = {Erich Gr{\"{a}}del and Wolfgang Thomas and Thomas Wilke},
 year         = {2002},
 title        = {Automata, Logics, and Infinite Games: {A} Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]},
 series       = {Lecture Notes in Computer Science},
 volume       = {2500},
 publisher    = {Springer},
 doi          = {10.1007/3-540-36387-4},
)
@article(JacobsBBEHKPRRS15,
 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(JacobsBBK0KKLNP16,
 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},
 editor       = {Piskac and Dimitrova},
 pages        = {149--177},
 doi          = {10.4204/EPTCS.229.12},
)
@inproceedings(JacobsBBKPRRSST16,
 author       = {Swen Jacobs and Roderick Bloem and Romain Brenguier 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 Second Reactive Synthesis Competition {(SYNTCOMP} 2015)},
 editor       = {Cern{\'{y}}},
 pages        = {27--57},
 doi          = {10.4204/EPTCS.202.4},
)
@article(KonighoferHB13,
 author       = {Robert K{\"{o}}nighofer and Georg Hofferek and Roderick Bloem},
 year         = {2013},
 title        = {Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies},
 journal      = {{STTT}},
 volume       = {15},
 number       = {5-6},
 pages        = {563--583},
 doi          = {10.1007/s10009-011-0221-y},
)
@article(Kozen83,
 author       = {Dexter Kozen},
 year         = {1983},
 title        = {Results on the Propositional mu-Calculus},
 journal      = {Theor. Comput. Sci.},
 volume       = {27},
 pages        = {333--354},
 doi          = {10.1016/0304-3975(82)90125-6},
)
@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} Trans. Robotics},
 volume       = {25},
 number       = {6},
 pages        = {1370--1381},
 doi          = {10.1109/TRO.2009.2030225},
)
@proceedings(DBLP:journals/taosd/2013-10,
 editor       = {Gary T. Leavens and Shigeru Chiba and {\'{E}}ric Tanter},
 year         = {2013},
 title        = {Transactions on Aspect-Oriented Software Development {X}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7800},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-36964-3},
)
@inproceedings(MPR16,
 author       = {Shahar Maoz and Or Pistiner and Jan Oliver Ringert},
 year         = {2016},
 title        = {Symbolic {BDD} and {ADD} Algorithms for Energy Games},
 editor       = {Piskac and Dimitrova},
 pages        = {35--54},
 doi          = {10.4204/EPTCS.229.5},
)
@inproceedings(MaozR15,
 author       = {Shahar Maoz and Jan Oliver Ringert},
 year         = {2015},
 title        = {{GR(1)} synthesis for {LTL} specification patterns},
 editor       = {Elisabetta Di Nitto and Mark Harman and Patrick Heymans},
 booktitle    = {Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, {ESEC/FSE} 2015, Bergamo, Italy, August 30 - September 4, 2015},
 publisher    = {{ACM}},
 pages        = {96--106},
 doi          = {10.1145/2786805.2786824},
)
@inproceedings(MaozR15synt,
 author       = {Shahar Maoz and Jan Oliver Ringert},
 year         = {2015},
 title        = {{Synthesizing a Lego Forklift Controller in GR(1): A Case Study}},
 booktitle    = {Proc. 4th Workshop on Synthesis, {SYNT} 2015 colocated with CAV 2015},
 series       = {{EPTCS}},
 volume       = {202},
 pages        = {58--72},
 doi          = {10.4204/EPTCS.202.5},
)
@inproceedings(MR16,
 author       = {Shahar Maoz and Jan Oliver Ringert},
 year         = {2016},
 title        = {On well-separation of {GR(1)} specifications},
 editor       = {Thomas Zimmermann and Cleland{-}Huang, Jane and Zhendong Su},
 booktitle    = {Proceedings of the 24th {ACM} {SIGSOFT} International Symposium on Foundations of Software Engineering, {FSE} 2016, Seattle, WA, USA, November 13-18, 2016},
 publisher    = {{ACM}},
 pages        = {362--372},
 doi          = {10.1145/2950290.2950300},
)
@inproceedings(MaozS11,
 author       = {Shahar Maoz and Yaniv Sa'ar},
 year         = {2011},
 title        = {{AspectLTL}: an aspect language for {LTL} specifications},
 editor       = {Paulo Borba and Shigeru Chiba},
 booktitle    = {AOSD},
 publisher    = {{ACM}},
 pages        = {19--30},
 doi          = {10.1145/1960275.1960280},
)
@inproceedings(MaozS12,
 author       = {Shahar Maoz and Yaniv Sa'ar},
 year         = {2012},
 title        = {Assume-Guarantee Scenarios: Semantics and Synthesis},
 booktitle    = {MODELS},
 series       = {LNCS},
 volume       = {7590},
 publisher    = {Springer},
 pages        = {335--351},
 doi          = {10.1007/978-3-642-33666-9\_22},
)
@article(MaozS13AOSD,
 author       = {Shahar Maoz and Yaniv Sa'ar},
 year         = {2013},
 title        = {Two-Way Traceability and Conflict Debugging for AspectLTL Programs},
 journal      = {T. Aspect-Oriented Software Development},
 pages        = {39--72},
 doi          = {10.1007/978-3-642-36964-3\_2},
)
@proceedings(DBLP:journals/corr/PiskacD16,
 editor       = {Ruzica Piskac and Rayna Dimitrova},
 year         = {2016},
 title        = {Proceedings Fifth Workshop on Synthesis, SYNT at CAV 2016, Toronto, Canada, July 17-18, 2016},
 series       = {{EPTCS}},
 volume       = {229},
 doi          = {10.4204/EPTCS.229},
)
@inproceedings(PitermanPS06,
 author       = {Nir Piterman and Amir Pnueli and Yaniv Sa'ar},
 year         = {2006},
 title        = {Synthesis of Reactive(1) Designs},
 booktitle    = {VMCAI},
 pages        = {364--380},
 doi          = {10.1007/11609773\_24},
)
@inproceedings(PR89,
 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},
)
@inproceedings(PnueliSZ10,
 author       = {Amir Pnueli and Yaniv Sa'ar and Lenore D. Zuck},
 year         = {2010},
 title        = {{JTLV}: {A} Framework for Developing Verification Algorithms},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {6174},
 publisher    = {Springer},
 pages        = {171--174},
 doi          = {10.1007/978-3-642-14295-6\_18},
)
@inproceedings(RyzhykW16,
 author       = {Leonid Ryzhyk and Adam Walker},
 year         = {2016},
 title        = {Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned},
 editor       = {Piskac and Dimitrova},
 pages        = {84--99},
 doi          = {10.4204/EPTCS.229.8},
)
@inproceedings(SchlaipferHB11,
 author       = {Matthias Schlaipfer and Georg Hofferek and Roderick Bloem},
 year         = {2011},
 title        = {Generalized Reactivity(1) Synthesis without a Monolithic Strategy},
 editor       = {Kerstin Eder and Louren{\c{c}}o, Jo{\~{a}}o and Onn Shehory},
 booktitle    = {Hardware and Software: Verification and Testing - 7th International Haifa Verification Conference, {HVC} 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {7261},
 publisher    = {Springer},
 pages        = {20--34},
 doi          = {10.1007/978-3-642-34188-5_6},
)
@misc(CUDD,
 author       = {Fabio Somenzi},
 title        = {{CUDD}: {BDD} package, {U}niversity of {C}olorado, {B}oulder.},
 howpublished = {\url{http://vlsi.colorado.edu/\~fabio/CUDD/cudd.pdf}},
)
@inproceedings(WalkerR14,
 author       = {Adam Walker and Leonid Ryzhyk},
 year         = {2014},
 title        = {Predicate abstraction for reactive synthesis},
 booktitle    = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland, October 21-24, 2014},
 publisher    = {{IEEE}},
 pages        = {219--226},
 doi          = {10.1109/FMCAD.2014.6987617},
)
@inproceedings(YangBOBCJRS98,
 author       = {Bwolen Yang and Randal E. Bryant and David R. O'Hallaron and Armin Biere and Olivier Coudert and Geert Janssen and Rajeev K. Ranjan and Fabio Somenzi},
 year         = {1998},
 title        = {A Performance Study of BDD-Based Model Checking},
 editor       = {Ganesh Gopalakrishnan and Phillip J. Windley},
 booktitle    = {Formal Methods in Computer-Aided Design, Second International Conference, {FMCAD} '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {1522},
 publisher    = {Springer},
 pages        = {255--289},
 doi          = {10.1007/3-540-49519-3_18},
)
@inproceedings(Zeller99,
 author       = {Andreas Zeller},
 year         = {1999},
 title        = {Yesterday, My Program Worked. Today, It Does Not. Why?},
 booktitle    = {ESEC/FSE},
 series       = {LNCS},
 volume       = {1687},
 publisher    = {Springer},
 pages        = {253--267},
 doi          = {10.1007/3-540-48166-4_16},
)
@article(ZellerH02,
 author       = {Andreas Zeller and Ralf Hildebrandt},
 year         = {2002},
 title        = {Simplifying and Isolating Failure-Inducing Input},
 journal      = {{IEEE} Trans. Software Eng.},
 volume       = {28},
 number       = {2},
 pages        = {183--200},
 doi          = {10.1109/32.988498},
)
@misc(optimizationWebsite,
 title        = {SYNTECH GR(1) Performance Website},
 note         = {\url{http://smlab.cs.tau.ac.il/syntech/performance/}},
)