@InProceedings{DFMV:CAV2015,
  Title                    = {Meeting a Powertrain Verification Challenge},
  Author                   = {Parasara Sridhar Duggirala and Chuchu Fan and Sayan Mitra and Mahesh Viswanathan},
  Booktitle                = {In the Proceedings of International Conference on Computer Aided Verification (CAV 2015)},
  Year                     = {2015},

  Address                  = {San Francisco},
  Pages                    = {536--543},
  Publisher                = {Springer},
  Series                   = {LNCS},
  Volume                   = {9206},

  Abstract                 = {We present the verification of a benchmark powertrain control system using the hybrid system verification tool C2E2. This model comes from a suite of benchmarks that were posed as a challenge problem for the hybrid systems community, and to our knowledge, we are reporting its first verification. For this work, we implemented the algorithm reported in [FanM:2015] in C2E2, to automatically compute local discrepancy (rate of convergence or divergence of trajectories) of the model. We verify the key requirements of the model, specified in signal temporal logic (STL), for a set of driver behaviors.},
  Codeurl                  = {https://publish.illinois.edu/c2e2-tool/},
  Keywords                 = {Automotive systems},
  Owner                    = {mitras},
  Pdfurl                   = {research/2015/cav2015.pdf},
  Timestamp                = {2015.05.04}
}