@article(artstein1983stabilization,
 author       = {Zvi Artstein},
 year         = {1983},
 title        = {Stabilization with relaxed controls},
 journal      = {Nonlinear Analysis: Theory, Methods \& Applications},
 volume       = {7},
 number       = {11},
 pages        = {1163 -- 1173},
 doi          = {10.1016/0362-546X(83)90049-4},
 url          = {http://www.sciencedirect.com/science/article/pii/0362546X83900494},
)
@inproceedings(dimitrova2014deductive,
 author       = {Rayna Dimitrova and Rupak Majumdar},
 year         = {2014},
 title        = {Deductive control synthesis for alternating-time logics},
 booktitle    = {2014 International Conference on Embedded Software, {EMSOFT} 2014, New Delhi, India, October 12-17, 2014},
 pages        = {14:1--14:10},
 doi          = {10.1145/2656045.2656054},
)
@inproceedings(DBLP:conf/cade/GaoKC13,
 author       = {Sicun Gao and Soonho Kong and Edmund M. Clarke},
 year         = {2013},
 title        = {dReal: An {SMT} Solver for Nonlinear Theories over the Reals},
 booktitle    = {Automated Deduction - {CADE-24} - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
 pages        = {208--214},
 doi          = {10.1007/978-3-642-38574-2\_14},
 url          = {https://doi.org/10.1007/978-3-642-38574-2_14},
)
@inproceedings(ghaoui1994synthesis,
 author       = {L. El Ghaoui and V. Balakrishnan},
 year         = {1994},
 title        = {Synthesis of fixed-structure controllers via numerical optimization},
 booktitle    = {Proceedings of 1994 33rd IEEE Conference on Decision and Control},
 volume       = {3},
 pages        = {2678--2683 vol.3},
 doi          = {10.1109/CDC.1994.411398},
)
@article(girard2010approximately,
 author       = {A. Girard and G. Pola and P. Tabuada},
 year         = {2010},
 title        = {Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {55},
 number       = {1},
 pages        = {116--126},
 doi          = {10.1109/TAC.2009.2034922},
)
@article(habets2006reachability,
 author       = {L. C. G. J. M. Habets and P. J. Collins and J. H. van Schuppen},
 year         = {2006},
 title        = {Reachability and control synthesis for piecewise-affine hybrid systems on simplices},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {51},
 number       = {6},
 pages        = {938--948},
 doi          = {10.1109/TAC.2006.876952},
)
@article(habets2004control,
 author       = {L.C.G.J.M. Habets and J.H. van Schuppen},
 year         = {2004},
 title        = {A control problem for affine dynamical systems on a full-dimensional polytope},
 journal      = {Automatica},
 volume       = {40},
 number       = {1},
 pages        = {21 -- 35},
 doi          = {10.1016/j.automatica.2003.08.001},
 url          = {http://www.sciencedirect.com/science/article/pii/S0005109803002620},
)
@article(helwa2013monotonic,
 author       = {M. K. Helwa and M. E. Broucke},
 year         = {2011},
 title        = {Monotonic reach control on polytopes},
 pages        = {4741--4746},
 doi          = {10.1109/CDC.2011.6160866},
)
@inproceedings(huang2015controller,
 author       = {Z. Huang and Y. Wang and S. Mitra and G. E. Dullerud and S. Chaudhuri},
 year         = {2015},
 title        = {Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm},
 booktitle    = {2015 54th IEEE Conference on Decision and Control (CDC)},
 pages        = {7434--7439},
 doi          = {10.1109/CDC.2015.7403394},
)
@inproceedings(mazo2010pessoa,
 author       = {Manuel Mazo Jr. and Anna Davitian and Paulo Tabuada},
 year         = {2010},
 title        = {{PESSOA:} {A} Tool for Embedded Controller Synthesis},
 booktitle    = {Computer Aided Verification, 22nd International Conference, {CAV} 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
 pages        = {566--569},
 doi          = {10.1007/978-3-642-14295-6\_49},
 url          = {https://doi.org/10.1007/978-3-642-14295-6_49},
)
@article(kloetzer2008fully,
 author       = {M. Kloetzer and C. Belta},
 year         = {2008},
 title        = {A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {53},
 number       = {1},
 pages        = {287--297},
 doi          = {10.1109/TAC.2007.914952},
)
@inproceedings(kong2013exponential,
 author       = {Hui Kong and Fei He and Xiaoyu Song and William N. N. Hung and Ming Gu},
 year         = {2013},
 title        = {Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems},
 booktitle    = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
 pages        = {242--257},
 doi          = {10.1007/978-3-642-39799-8\_17},
 url          = {https://doi.org/10.1007/978-3-642-39799-8_17},
)
@book(liberzon2012switching,
 author       = {Daniel Liberzon},
 year         = {2012},
 title        = {Switching in systems and control},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/978-1-4612-0017-8},
)
@inproceedings(lin2007reachability,
 author       = {Z. Lin and M. E. Broucke},
 year         = {2007},
 title        = {Reachability and control of affine hypersurface systems on polytopes},
 booktitle    = {2007 46th IEEE Conference on Decision and Control},
 pages        = {733--738},
 doi          = {10.1109/CDC.2007.4434805},
)
@article(liu2013synthesis,
 author       = {J. Liu and N. Ozay and U. Topcu and R. M. Murray},
 year         = {2013},
 title        = {Synthesis of Reactive Switching Protocols From Temporal Logic Specifications},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {58},
 number       = {7},
 pages        = {1771--1785},
 doi          = {10.1109/TAC.2013.2246095},
)
@techreport(mouelhi:hal-00743982,
 author       = {Sebti Mouelhi and Antoine Girard and Gregor G{\"o}ssler},
 year         = {2012},
 title        = {{CoSyMA: A Tool for Controller Synthesis Using Multi-scale Abstractions}},
 type         = {Research Report},
 number       = {RR-8108},
 institution  = {{INRIA}},
 url          = {https://hal.inria.fr/hal-00743982},
)
@inproceedings(mouelhi2013cosyma,
 author       = {Sebti Mouelhi and Antoine Girard and G{\"{o}}{\ss}ler, Gregor},
 year         = {2013},
 title        = {CoSyMA: a tool for controller synthesis using multi-scale abstractions},
 booktitle    = {Proceedings of the 16th international conference on Hybrid systems: computation and control, {HSCC} 2013, April 8-11, 2013, Philadelphia, PA, {USA}},
 pages        = {83--88},
 doi          = {10.1145/2461328.2461343},
)
@inproceedings(DeMoura+Bjorner/08/Z3,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3:} An Efficient {SMT} Solver},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, {TACAS} 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
 url          = {https://doi.org/10.1007/978-3-540-78800-3_24},
)
@inproceedings(nilssonincremental,
 author       = {P. Nilsson and N. Ozay},
 year         = {2014},
 title        = {Incremental synthesis of switching protocols via abstraction refinement},
 booktitle    = {53rd IEEE Conference on Decision and Control},
 pages        = {6246--6253},
 doi          = {10.1109/CDC.2014.7040368},
)
@inproceedings(ozay2013computing,
 author       = {N. Ozay and J. Liu and P. Prabhakar and R. M. Murray},
 year         = {2013},
 title        = {Computing augmented finite transition systems to synthesize switching protocols for polynomial switched systems},
 booktitle    = {2013 American Control Conference},
 pages        = {6237--6244},
 doi          = {10.1109/ACC.2013.6580816},
)
@inproceedings(prajna2002introducing,
 author       = {S. Prajna and A. Papachristodoulou and P. A. Parrilo},
 year         = {2002},
 title        = {Introducing SOSTOOLS: a general purpose sum of squares programming solver},
 booktitle    = {Proceedings of the 41st IEEE Conference on Decision and Control, 2002.},
 volume       = {1},
 pages        = {741--746 vol.1},
 doi          = {10.1109/CDC.2002.1184594},
)
@inproceedings(Ravanbakhsh-Others/2015/Counter-LMI,
 author       = {H. Ravanbakhsh and S. Sankaranarayanan},
 year         = {2015},
 title        = {Counter-Example Guided Synthesis of control Lyapunov functions for switched systems},
 booktitle    = {2015 54th IEEE Conference on Decision and Control (CDC)},
 pages        = {4232--4239},
 doi          = {10.1109/CDC.2015.7402879},
)
@inproceedings(Ravanbakhsh-Others/2016/EMSOFT,
 author       = {Hadi Ravanbakhsh and Sriram Sankaranarayanan},
 year         = {2016},
 title        = {Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework},
 booktitle    = {Proceedings of the 13th International Conference on Embedded Software},
 series       = {EMSOFT '16},
 publisher    = {ACM},
 pages        = {8:1--8:10},
 doi          = {10.1145/2968478.2968485},
)
@article(roszak2006necessary,
 author       = {Bartek Roszak and Mireille E. Broucke},
 year         = {2006},
 title        = {Necessary and sufficient conditions for reachability on a simplex},
 journal      = {Automatica},
 volume       = {42},
 number       = {11},
 pages        = {1913 -- 1918},
 doi          = {10.1016/j.automatica.2006.06.003},
 url          = {http://www.sciencedirect.com/science/article/pii/S0005109806002445},
)
@inproceedings(rungger2016scots,
 author       = {Matthias Rungger and Majid Zamani},
 year         = {2016},
 title        = {{SCOTS:} {A} Tool for the Synthesis of Symbolic Controllers},
 booktitle    = {Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, {HSCC} 2016, Vienna, Austria, April 12-14, 2016},
 pages        = {99--104},
 doi          = {10.1145/2883817.2883834},
)
@phdthesis(solar2008program,
 author       = {Solar Lezama, Armando},
 year         = {2008},
 title        = {Program Synthesis By Sketching},
 school       = {EECS Department, University of California, Berkeley},
 url          = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html},
)
@article(sontag1989universal,
 author       = {Eduardo D. Sontag},
 year         = {1989},
 title        = {A ‘universal’ construction of Artstein's theorem on nonlinear stabilization},
 journal      = {Systems \& Control Letters},
 volume       = {13},
 number       = {2},
 pages        = {117 -- 123},
 doi          = {10.1016/0167-6911(89)90028-5},
 url          = {http://www.sciencedirect.com/science/article/pii/0167691189900285},
)
@article(taly2011synthesizing,
 author       = {Ankur Taly and Sumit Gulwani and Ashish Tiwari},
 year         = {2011},
 title        = {Synthesizing switching logic using constraint solving},
 journal      = {{STTT}},
 volume       = {13},
 number       = {6},
 pages        = {519--535},
 doi          = {10.1007/s10009-010-0172-8},
 url          = {https://doi.org/10.1007/s10009-010-0172-8},
)
@inproceedings(taly2010switching,
 author       = {Ankur Taly and Ashish Tiwari},
 year         = {2010},
 title        = {Switching logic synthesis for reachability},
 booktitle    = {Proceedings of the 10th International conference on Embedded software, {EMSOFT} 2010, Scottsdale, Arizona, USA, October 24-29, 2010},
 pages        = {19--28},
 doi          = {10.1145/1879021.1879025},
)
@inproceedings(tan2004searching,
 author       = {Weehong Tan and Andrew Packard},
 year         = {2004},
 title        = {Searching for control {L}yapunov functions using sums of squares programming},
 booktitle    = {Allerton conference on communication, control and computing},
 pages        = {210--219},
)
@article(tazaki2012discrete,
 author       = {Y. Tazaki and J. i. Imura},
 year         = {2012},
 title        = {Discrete Abstractions of Nonlinear Systems Based on Error Propagation Analysis},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {57},
 number       = {3},
 pages        = {550--564},
 doi          = {10.1109/TAC.2011.2161789},
)
@book(thomas2002automata,
 author       = {Wolfgang Thomas and Thomas Wilke},
 year         = {2002},
 title        = {Automata, logics, and infinite games: a guide to current research},
 volume       = {2500},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/3-540-36387-4},
)
@article(wieland2007constructive,
 author       = {Peter Wieland and Frank Allgöwer},
 year         = {2007},
 title        = {CONSTRUCTIVE SAFETY USING CONTROL BARRIER FUNCTIONS},
 journal      = {IFAC Proceedings Volumes},
 volume       = {40},
 number       = {12},
 pages        = {462 -- 467},
 doi          = {10.3182/20070822-3-ZA-2920.00076},
 url          = {http://www.sciencedirect.com/science/article/pii/S1474667016355690},
 note         = {7th IFAC Symposium on Nonlinear Control Systems},
)
@article(wongpiromsarn2016automata,
 author       = {T. Wongpiromsarn and U. Topcu and A. Lamperski},
 year         = {2016},
 title        = {Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {61},
 number       = {11},
 pages        = {3344--3355},
 doi          = {10.1109/TAC.2015.2511722},
)
@inproceedings(wongpiromsarn2011tulip,
 author       = {Tichakorn Wongpiromsarn and Ufuk Topcu and Necmiye Ozay and Huan Xu and Richard M. Murray},
 year         = {2011},
 title        = {TuLiP: A Software Toolbox for Receding Horizon Temporal Logic Planning},
 booktitle    = {Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control},
 series       = {HSCC '11},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {313--314},
 doi          = {10.1145/1967701.1967747},
)
@article(xu2015robustness,
 author       = {Xiangru Xu and Paulo Tabuada and Jessy W. Grizzle and Aaron D. Ames},
 year         = {2015},
 title        = {Robustness of Control Barrier Functions for Safety Critical Control**This work is partially supported by the National Science Foundation Grants 1239055, 1239037 and 1239085.},
 journal      = {IFAC-PapersOnLine},
 volume       = {48},
 number       = {27},
 pages        = {54 -- 61},
 doi          = {10.1016/j.ifacol.2015.11.152},
 url          = {http://www.sciencedirect.com/science/article/pii/S2405896315024106},
 note         = {Analysis and Design of Hybrid Systems ADHS},
)
@article(zamani2012symbolic,
 author       = {M. Zamani and G. Pola and M. Mazo and P. Tabuada},
 year         = {2012},
 title        = {Symbolic Models for Nonlinear Control Systems Without Stability Assumptions},
 journal      = {IEEE Transactions on Automatic Control},
 volume       = {57},
 number       = {7},
 pages        = {1804--1809},
 doi          = {10.1109/TAC.2011.2176409},
)