@article(abdulla2004using,
 author       = {Parosh Aziz Abdulla and Collomb-Annichini, Aurore and Ahmed Bouajjani and Bengt Jonsson},
 year         = {2004},
 title        = {Using forward reachability analysis for verification of lossy channel systems},
 journal      = {Formal Methods in System Design},
 volume       = {25},
 number       = {1},
 pages        = {39--65},
 doi          = {10.1023/B:FORM.0000033962.51898.1a},
)
@inproceedings(bae2017modular,
 author       = {Kyungmin Bae and Sicun Gao},
 year         = {2017},
 title        = {Modular smt-based analysis of nonlinear hybrid systems},
 booktitle    = {2017 Formal Methods in Computer Aided Design (FMCAD)},
 organization = {IEEE},
 pages        = {180--187},
 doi          = {10.23919/FMCAD.2017.8102258},
)
@inproceedings(bak2015hscc,
 author       = {Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson},
 year         = {2015},
 title        = {{HyST}: A Source Transformation and Translation Tool for Hybrid Automaton Models},
 booktitle    = {Proc. of the 18th Intl. Conf. on Hybrid Systems: Computation and Control (HSCC)},
 publisher    = {ACM},
 doi          = {10.1145/2728606.2728630},
)
@techreport(BarFTRR17,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2017},
 title        = {{The SMT-LIB Standard: Version 2.6}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 note         = {Available at {\tt \url {www.SMT-LIB.org}}},
)
@inproceedings(DBLP:conf/cav/BarrettCDHJKRT11,
 author       = {Clark W. Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {Computer Aided Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1\_14},
)
@incollection(bengtsson1995,
 author       = {Johan Bengtsson and Kim Larsen and Fredrik Larsson and Paul Pettersson and Wang Yi},
 year         = {1996},
 title        = {{UPPAAL}: {A} tool suite for automatic verification of real-time systems},
 editor       = {Rajeev Alur and Thomas Henzinger and Eduardo Sontag},
 booktitle    = {Hybrid Systems III},
 series       = {LNCS},
 volume       = {1066},
 publisher    = {Springer},
 pages        = {232--243},
 doi          = {10.1007/BFb0020949},
)
@incollection(cavada2014cav,
 author       = {Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio Mover and Marco Roveri and Stefano Tonetta},
 year         = {2014},
 title        = {The nuXmv Symbolic Model Checker},
 editor       = {Armin Biere and Roderick Bloem},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {8559},
 publisher    = {Springer International Publishing},
 pages        = {334--342},
 doi          = {10.1007/978-3-319-08867-9\_22},
)
@incollection(chen2013cav,
 author       = {Xin Chen and Erika Abraham and Sriram Sankaranarayanan},
 year         = {2013},
 title        = {{Flow*}: An Analyzer for Non-linear Hybrid Systems},
 editor       = {Natasha Sharygina and Helmut Veith},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {258--263},
 doi          = {10.1007/978-3-642-39799-8\_18},
)
@incollection(cimatti2015tacas,
 author       = {Alessandro Cimatti and Alberto Griggio and Sergio Mover and Stefano Tonetta},
 year         = {2015},
 title        = {{HyComp}: An {SMT}-Based Model Checker for Hybrid Systems},
 editor       = {Christel Baier and Cesare Tinelli},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {9035},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {52--67},
 doi          = {10.1007/978-3-662-46681-0\_4},
)
@incollection(cimatti2015hycomp,
 author       = {Alessandro Cimatti and Alberto Griggio and Sergio Mover and Stefano Tonetta},
 year         = {2015},
 title        = {HyComp: An SMT-Based Model Checker for Hybrid Systems},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer},
 pages        = {52--67},
 doi          = {10.1007/978-3-662-46681-0\_4},
)
@article(cimatti2013fmsd,
 author       = {Alessandro Cimatti and Sergio Mover and Stefano Tonetta},
 year         = {2013},
 title        = {SMT-based scenario verification for hybrid systems},
 journal      = {Formal Methods in System Design},
 volume       = {42},
 number       = {1},
 pages        = {46--66},
 doi          = {10.1007/s10703-012-0158-0},
)
@inproceedings(demoura2008tacas,
 author       = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {Z3: {A}n Efficient {SMT} Solver},
 booktitle    = {Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {TACAS '08/ETAPS '08},
 publisher    = {Springer-Verlag},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@incollection(eggers2008atva,
 author       = {Andreas Eggers and Martin Fr\"{a}nzle and Christian Herde},
 year         = {2008},
 title        = {{SAT} Modulo {ODE}: A Direct {SAT} Approach to Hybrid Systems},
 editor       = {Sungdeok Cha and Jin-Young Choi and Moonzoo Kim and Insup Lee and Mahesh Viswanathan},
 booktitle    = {Automated Technology for Verification and Analysis},
 series       = {Lecture Notes in Computer Science},
 volume       = {5311},
 publisher    = {Springer Berlin / Heidelberg},
 pages        = {171--185},
 doi          = {10.1007/978-3-540-88387-6\_14},
)
@inproceedings(frehse2011cav,
 author       = {Goran Frehse and Le Guernic, Colas and Alexandre Donz\'e and Scott Cotton and Rajarshi Ray and Olivier Lebeltel and Rodolfo Ripado and Antoine Girard and Thao Dang and Oded Maler},
 year         = {2011},
 title        = {{SpaceEx}: {S}calable Verification of Hybrid Systems},
 booktitle    = {Computer Aided Verification (CAV)},
 series       = {LNCS},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-22110-1\_30},
)
@inproceedings(gao2012lics,
 author       = {Sicun Gao and J. Avigad and E.M. Clarke},
 year         = {2012},
 title        = {Delta-Decidability over the Reals},
 booktitle    = {Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on},
 pages        = {305--314},
 doi          = {10.1109/LICS.2012.41},
)
@inproceedings(gao2013fmcad,
 author       = {Sicun Gao and Soonho Kong and Edmund Clarke},
 year         = {2013},
 title        = {Satisfiability Modulo {ODE}s},
 booktitle    = {International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
 doi          = {10.1109/FMCAD.2008.ECP.14},
)
@incollection(gao2013cade,
 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},
 publisher    = {Springer},
 pages        = {208--214},
 doi          = {10.1007/978-3-642-38574-2\_14},
)
@inproceedings(ghilardi2010mcmt,
 author       = {Silvio Ghilardi and Silvio Ranise},
 year         = {2010},
 title        = {MCMT: A Model Checker Modulo Theories.},
 booktitle    = {IJCAR},
 volume       = {10},
 organization = {Springer},
 pages        = {22--29},
 doi          = {10.1007/978-3-642-14203-1\_3},
)
@inproceedings(henzinger1996lics,
 author       = {T. A. Henzinger},
 year         = {1996},
 title        = {The theory of hybrid automata},
 booktitle    = {IEEE Symposium on Logic in Computer Science (LICS)},
 publisher    = {IEEE Computer Society},
 address      = {Washington, DC, USA},
 pages        = {278},
 doi          = {10.1109/LICS.1996.561342},
)
@article(henzinger1997sttt,
 author       = {Thomas A. Henzinger and Pei-Hsin Ho and Wong-Toi, Howard},
 year         = {1997},
 title        = {{HyTech}: {A} model checker for hybrid systems},
 journal      = {Journal on Software Tools for Technology Transfer},
 volume       = {1},
 pages        = {110--122},
 doi          = {10.1007/s100090050008},
)
@incollection(janota2012solving,
 author       = {Mikol{\'a}{\v{s}} Janota and William Klieber and Marques-Silva, Joao and Edmund Clarke},
 year         = {2012},
 title        = {Solving QBF with counterexample guided refinement},
 booktitle    = {Theory and Applications of Satisfiability Testing--SAT 2012},
 publisher    = {Springer},
 pages        = {114--128},
 doi          = {10.1007/978-3-642-31612-8\_10},
)
@incollection(johnson2012forte,
 author       = {Taylor T. Johnson and Sayan Mitra},
 year         = {2012},
 title        = {A Small Model Theorem for Rectangular Hybrid Automata Networks},
 booktitle    = {Proceedings of the IFIP International Conference on Formal Techniques for Distributed Systems, Joint 14th Formal Methods for Open Object-Based Distributed Systems and 32nd Formal Techniques for Networked and Distributed Systems (FMOODS-FORTE)},
 series       = {LNCS},
 volume       = {7273},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-30793-5\_2},
)
@inproceedings(johnson2013infotech,
 author       = {Taylor T. Johnson and Sayan Mitra},
 year         = {2013},
 title        = {Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace Systems},
 booktitle    = {Proceedings of the AIAA Infotech at Aerospace Conference (AIAA Infotech 2013)},
 address      = {Boston, MA},
 doi          = {10.2514/6.2013-4811},
)
@inproceedings(johnson2014formats,
 author       = {Taylor T. Johnson and Sayan Mitra},
 year         = {2014},
 title        = {Anonymized Reachability of Rectangular Hybrid Automata Networks},
 booktitle    = {Formal Modeling and Analysis of Timed Systems (FORMATS)},
 doi          = {10.1007/978-3-319-10512-3\_10},
)
@article(jussila2007compressing,
 author       = {Toni Jussila and Armin Biere},
 year         = {2007},
 title        = {Compressing BMC encodings with QBF},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {174},
 number       = {3},
 pages        = {45--56},
 doi          = {10.1016/j.entcs.2006.12.022},
)
@inproceedings(kong2015dreach,
 author       = {Soonho Kong and Sicun Gao and Wei Chen and Edmund Clarke},
 year         = {2015},
 title        = {dReach: Delta-reachability analysis for hybrid systems},
 booktitle    = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {200--205},
 doi          = {10.1007/978-3-662-46681-0\_15},
)
@inproceedings(lynch1992timing,
 author       = {Nancy Lynch and Nir Shavit},
 year         = {1992},
 title        = {Timing-based mutual exclusion},
 booktitle    = {Real-Time Systems Symposium, 1992},
 organization = {IEEE},
 pages        = {2--11},
 doi          = {10.1109/REAL.1992.242681},
)
@article(mangassarian2010tc,
 author       = {H. Mangassarian and A. Veneris and M. Benedetti},
 year         = {2010},
 title        = {Robust {QBF} Encodings for Sequential Circuits with Applications to Verification, Debug, and Test},
 journal      = {Computers, IEEE Transactions on},
 volume       = {59},
 number       = {7},
 pages        = {981--994},
 doi          = {10.1109/TC.2010.74},
)
@inproceedings(miller2011mtv,
 author       = {C. Miller and K. Gitina and B. Becker},
 year         = {2011},
 title        = {Bounded Model Checking of Incomplete Real-time Systems Using Quantified SMT Formulas},
 booktitle    = {Microprocessor Test and Verification (MTV), 2011 12th International Workshop on},
 pages        = {22--27},
 doi          = {10.1109/MTV.2011.13},
)
@inproceedings(shmarov2017smt,
 author       = {Fedor Shmarov and Nicola Paoletti and Ezio Bartocci and Shan Lin and Scott A Smolka and Paolo Zuliani},
 year         = {2017},
 title        = {SMT-based synthesis of safe and robust PID controllers for stochastic hybrid systems},
 booktitle    = {Haifa Verification Conference},
 organization = {Springer},
 pages        = {131--146},
 doi          = {10.1007/978-3-319-70389-3\_9},
)
@incollection(tiwari2012cav,
 author       = {Ashish Tiwari},
 year         = {2012},
 title        = {{HybridSAL} Relational Abstracter},
 editor       = {P. Madhusudan and SanjitA. Seshia},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {7358},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {725--731},
 doi          = {10.1007/978-3-642-31424-7\_56},
)