@inproceedings{4616,
  abstract     = {We present a model checking procedure and its implementation for the automatic verification of embedded systems. Systems are represented by hybrid automata - machines with finite control and real-valued variables modeling continuous environment parameters such as time, pressure, and temperature. System properties are specified in a real-time temporal logic and verified by symbolic computation. The verification procedure, implemented in Mathematica, is used to prove digital controllers and distributed algorithms correct. The verifier checks safety, liveness, time-bounded, and duration properties of hybrid automata},
  author       = {Alur, Rajeev and Henzinger, Thomas A and Ho, Pei},
  booktitle    = {1993 Proceedings Real-Time Systems Symposium},
  isbn         = {0-8186-4480-X},
  location     = {Raleigh, NC, United States of America},
  pages        = {2 -- 11},
  publisher    = {IEEE},
  title        = {{Automatic symbolic verification of embedded systems}},
  doi          = {10.1109/REAL.1993.393520 },
  year         = {1993},
}