@misc(bhavetool,
 author       = {Bhave et al.},
 year         = {2015},
 title        = {{PTA-BMC}},
 howpublished = {\url{http://www.cse.iitb.ac.in/~devendra/pta-bmc.html}},
)
@misc(cora,
 author       = {Larsen et al.},
 year         = {2006},
 title        = {{UPPAAL-CORA}},
 howpublished = {\url{http://people.cs.aau.dk/~adavid/cora/index.html}},
)
@article(journals/tcs/AlurD94,
 author       = {Rajeev Alur and David L. Dill},
 year         = {1994},
 title        = {A Theory of Timed Automata},
 journal      = {Theor. Comput. Sci},
 volume       = {126},
 number       = {2},
 pages        = {183--235},
 doi          = {10.1016/0304-3975(94)90010-8},
)
@article(Alur:2004:OPW:1026907.1026909,
 author       = {Rajeev Alur and La Torre, Salvatore and George J. Pappas},
 year         = {2004},
 title        = {Optimal Paths in Weighted Timed Automata},
 journal      = {Theor. Comput. Sci.},
 volume       = {318},
 pages        = {297--322},
 doi          = {10.1016/j.tcs.2003.10.038},
)
@incollection(bmc-ta,
 author       = {G. Audemard and A. Cimatti and A. Kornilowicz and R. Sebastiani},
 year         = {2002},
 title        = {Bounded Model Checking for Timed Systems},
 booktitle    = {Formal Techniques for Networked and Distributed Sytems — FORTE 2002},
 series       = {LNCS},
 volume       = {2529},
 publisher    = {Springer},
 pages        = {243--259},
 doi          = {10.1007/3-540-36135-9\_16},
)
@inproceedings(BGA2001,
 author       = {Gerd Behrmann and Ansgar Fehnker and Thomas Hune and Kim Larsen and Paul Pettersson and Judi Romijn and Frits Vaandrager},
 year         = {2001},
 title        = {Minimum-Cost Reachability for Priced Time Automata},
 booktitle    = {HSCC},
 series       = {LNCS},
 volume       = {2034},
 publisher    = {Springer},
 pages        = {147--161},
 doi          = {10.1007/3-540-45351-2\_15},
)
@article(behrmann2005optimal,
 author       = {Gerd Behrmann and Kim G Larsen and Jacob I Rasmussen},
 year         = {2005},
 title        = {Optimal scheduling using priced timed automata},
 journal      = {Performance Evaluation Review},
 volume       = {32},
 number       = {4},
 pages        = {34--40},
 doi          = {10.1145/1059816.1059823},
)
@article(Bouyer:2007:ORP:1288667.1288679,
 author       = {Patricia Bouyer and Thomas Brihaye and V{\'e}ronique Bruy\`{e}re and Jean-Fran\c{c}ois Raskin},
 year         = {2007},
 title        = {On the Optimal Reachability Problem of Weighted Timed Automata},
 journal      = {FMSD},
 volume       = {31},
 number       = {2},
 pages        = {135--175},
 doi          = {10.1007/s10703-007-0035-4},
)
@inproceedings(DBLP:conf/hybrid/BouyerBL04,
 author       = {Patricia Bouyer and Ed Brinksma and Kim Guldstrand Larsen},
 year         = {2004},
 title        = {Staying Alive as Cheaply as Possible},
 booktitle    = {HSCC},
 pages        = {203--218},
 doi          = {10.1007/978-3-540-24743-2\_14},
)
@inproceedings(Bouyer:2010:TAO:1755952.1755963,
 author       = {Patricia Bouyer and Uli Fahrenberg and Kim G. Larsen and Nicolas Markey},
 year         = {2010},
 title        = {Timed Automata with Observers Under Energy Constraints},
 booktitle    = {HSCC},
 publisher    = {ACM},
 pages        = {61--70},
 doi          = {10.1145/1755952.1755963},
)
@incollection(de2008z3,
 author       = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {Z3: An efficient SMT solver},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@article(Fahrenberg2009179,
 author       = {Uli Fahrenberg and Kim G. Larsen},
 year         = {2009},
 title        = {Discount-Optimal Infinite Runs in Priced Timed Automata},
 journal      = {ENTCS (INFINITY)},
 volume       = {239},
 pages        = {179 -- 191},
 doi          = {10.1016/j.entcs.2009.05.039},
)
@inproceedings(FJ13,
 author       = {John Fearnley and Marcin Jurdzinski},
 year         = {2013},
 title        = {Reachability in Two-Clock Timed Automata Is PSPACE-Complete},
 booktitle    = {ICALP},
 pages        = {212--223},
 doi          = {10.1007/978-3-642-39212-2\_21},
)
@inproceedings(ivanov2010remes,
 author       = {Dinko Ivanov and Marin Orli{\'c} and Cristina Seceleanu and Aneta Vulgarakis},
 year         = {2010},
 title        = {REMES tool-chain: a set of integrated tools for behavioral modeling and analysis of embedded systems},
 booktitle    = {Automated software engineering},
 organization = {ACM},
 pages        = {361--362},
 doi          = {10.1145/1858996.1859076},
)
@incollection(jiang2012modeling,
 author       = {Zhihao Jiang and Miroslav Pajic and Salar Moarref and Rajeev Alur and Rahul Mangharam},
 year         = {2012},
 title        = {Modeling and verification of a dual chamber implantable pacemaker},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer},
 pages        = {188--203},
 doi          = {10.1007/978-3-642-28756-5\_14},
)
@article(5491259,
 author       = {M. Jongerden and A. Mereacre and H. Bohnenkamp and B. Haverkort and J. Katoen},
 year         = {2010},
 title        = {Computing Optimal Schedules of Battery Usage in Embedded Systems},
 journal      = {Industrial Informatics, IEEE Transactions on},
 volume       = {6},
 number       = {3},
 pages        = {276--286},
 doi          = {10.1109/TII.2010.2051813},
)
@incollection(jovanovic2012solving,
 author       = {Dejan Jovanovi{\'c} and De Moura, Leonardo},
 year         = {2012},
 title        = {Solving non-linear arithmetic},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer},
 pages        = {339--354},
 doi          = {10.1007/978-3-642-31365-3\_27},
)
@inproceedings(DBLP:conf/formats/JurdzinskiT08,
 author       = {Marcin Jurdzinski and Ashutosh Trivedi},
 year         = {2008},
 title        = {Concavely-Priced Timed Automata},
 booktitle    = {FORMATS},
 pages        = {48--62},
 doi          = {10.1007/978-3-540-85778-5\_5},
)
@inproceedings(LMS04,
 author       = {F. Laroussinie and N. Markey and Ph. Schnoebelen},
 year         = {2004},
 title        = {Model Checking Timed Automata with One or Two Clocks},
 booktitle    = {CONCUR},
 series       = {LNCS},
 volume       = {3170},
 publisher    = {Springer},
 pages        = {387--401},
 doi          = {10.1007/978-3-540-28644-8\_25},
)
@book(Min67,
 author       = {Marvin L. Minsky},
 year         = {1967},
 title        = {Computation: finite and infinite machines},
 publisher    = {Prentice-Hall, Inc.},
)