@inproceedings(AlurMT13,
 author       = {Rajeev Alur and Salar Moarref and Ufuk Topcu},
 year         = {2013},
 title        = {Counter-strategy guided refinement of {GR(1)} temporal logic specifications},
 booktitle    = {Formal Methods in Computer-Aided Design, {FMCAD} 2013, Portland, OR, USA, October 20-23, 2013},
 publisher    = {{IEEE}},
 pages        = {26--33},
 url          = {http://dx.doi.org/10.1109/FMCAD.2013.6679387},
)
@inproceedings(BloemJK14,
 author       = {Roderick Bloem and Swen Jacobs and Ayrat Khalimov},
 year         = {2014},
 title        = {Parameterized Synthesis Case Study: {AMBA} {AHB}},
 editor       = {Krishnendu Chatterjee and R{\"{u}}diger Ehlers and Susmit Jha},
 booktitle    = {Proceedings 3rd Workshop on Synthesis, {SYNT} 2014, Vienna, Austria, July 23-24, 2014.},
 series       = {{EPTCS}},
 volume       = {157},
 pages        = {68--83},
 url          = {http://dx.doi.org/10.4204/EPTCS.157.9},
)
@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},
 url          = {http://dx.doi.org/10.1016/j.jcss.2011.08.007},
)
@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},
 url          = {http://doi.acm.org/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},
 url          = {http://doi.acm.org/10.1145/302405.302672},
)
@inproceedings(EhlersT14,
 author       = {R{\"{u}}diger Ehlers and Ufuk Topcu},
 year         = {2014},
 title        = {Resilience to intermittent assumption violations in reactive synthesis},
 editor       = {Martin Fr{\"{a}}nzle and John Lygeros},
 booktitle    = {17th International Conference on Hybrid Systems: Computation and Control (part of {CPS} Week), HSCC'14, Berlin, Germany, April 15-17, 2014},
 publisher    = {{ACM}},
 pages        = {203--212},
 url          = {http://doi.acm.org/10.1145/2562059.2562128},
)
@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},
 url          = {http://dx.doi.org/10.1007/s10009-011-0207-9},
)
@inproceedings(KleinP10,
 author       = {Uri Klein and Amir Pnueli},
 year         = {2010},
 title        = {Revisiting Synthesis of {GR(1)} Specifications},
 editor       = {Sharon Barner and Ian G. Harris and Daniel Kroening and Orna Raz},
 booktitle    = {Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, {HVC} 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {6504},
 publisher    = {Springer},
 pages        = {161--181},
 url          = {http://dx.doi.org/10.1007/978-3-642-19583-9_16},
)
@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},
 url          = {http://dx.doi.org/10.1007/s10009-011-0221-y},
)
@inproceedings(Kress-GazitFP07,
 author       = {Kress{-}Gazit, Hadas and Georgios E. Fainekos and George J. Pappas},
 year         = {2007},
 title        = {{Where's Waldo? Sensor-Based Temporal Logic Motion Planning}},
 booktitle    = {2007 {IEEE} International Conference on Robotics and Automation, {ICRA} 2007, 10-14 April 2007, Roma, Italy},
 publisher    = {{IEEE}},
 pages        = {3116--3121},
 url          = {http://dx.doi.org/10.1109/ROBOT.2007.363946},
)
@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},
 url          = {http://dx.doi.org/10.1109/TRO.2009.2030225},
)
@inproceedings(MR15patterns,
 author       = {Shahar Maoz and Jan Oliver Ringert},
 year         = {2015},
 title        = {GR(1) Synthesis for LTL Specification Patterns},
 booktitle    = {ESEC/FSE},
 publisher    = {ACM},
 pages        = {96--106},
 url          = {http://dx.doi.org/10.1145/2786805.2786824},
 note         = {\url{http://smlab.cs.tau.ac.il/syntech/patterns/}},
)
@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},
 url          = {http://doi.acm.org/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},
 url          = {http://dx.doi.org/10.1007/978-3-642-33666-9_22},
)
@inproceedings(MaozS13,
 author       = {Shahar Maoz and Yaniv Sa'ar},
 year         = {2013},
 title        = {Counter play-out: executing unrealizable scenario-based specifications},
 booktitle    = {ICSE},
 publisher    = {{IEEE} / {ACM}},
 pages        = {242--251},
 url          = {http://dl.acm.org/citation.cfm?id=2486821},
)
@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},
 volume       = {10},
 pages        = {39--72},
 url          = {http://dx.doi.org/10.1007/978-3-642-36964-3_2},
)
@inproceedings(PitermanPS06,
 author       = {Nir Piterman and Amir Pnueli and Yaniv Sa'ar},
 year         = {2006},
 title        = {Synthesis of Reactive(1) Designs},
 booktitle    = {VMCAI},
 series       = {LNCS},
 volume       = {3855},
 publisher    = {Springer},
 pages        = {364--380},
 url          = {http://dx.doi.org/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},
 url          = {http://doi.acm.org/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},
 url          = {http://dx.doi.org/10.1007/978-3-642-14295-6_18},
)
@inproceedings(RamanPK13,
 author       = {Vasumathi Raman and Nir Piterman and Kress{-}Gazit, Hadas},
 year         = {2013},
 title        = {Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations},
 booktitle    = {2013 {IEEE} International Conference on Robotics and Automation, Karlsruhe, Germany, May 6-10, 2013},
 publisher    = {{IEEE}},
 pages        = {4075--4081},
 url          = {http://dx.doi.org/10.1109/ICRA.2013.6631152},
)
@book(RRW14,
 author       = {Jan Oliver Ringert and Bernhard Rumpe and Andreas Wortmann},
 year         = {2014},
 title        = {{Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton}},
 series       = {Aachener Informatik-Berichte, Software Engineering},
 volume       = {20},
 publisher    = {Shaker Verlag},
)
@misc(materials,
 title        = {SYNTECH forklift website},
 note         = {\url{http://smlab.cs.tau.ac.il/syntech/forklift/}},
)
@misc(patternCatalog,
 title        = {SYNTECH {GR(1)} patterns website},
 note         = {\url{http://smlab.cs.tau.ac.il/syntech/patterns/}},
)