@Article{PDMV:FMSD2015,
  author    = {Pavithra Prabhakar and Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan},
  title     = {Hybrid Automata-based CEGAR for Rectangular Hybrid Systems},
  journal   = {In Formal Methods in System Design (FMSD)},
  year      = {2015},
  volume    = {46},
  number    = {2},
  pages     = {105---134},
  abstract  = {In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) for systems modelled as hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well. We present a counterexample guided abstraction refinement method for systems modelled as initialized rectangular hybrid automata along the lines of the general framework and show the completeness of the method. The advantages of our approach are illustrated by examples where it performs better than existing methods. Finally, we demonstrate the feasibility of our approach by performing several experiments using a prototype tool that implements our CEGAR algorithm.},
  biburl    = {http://dblp.uni-trier.de/rec/bibtex/journals/fmsd/PrabhakarDM015},
  codeurl   = {http://publish.illinois.edu/hare-tool/},
  keywords  = {Hybrid systems, Verification},
  owner     = {mitras},
  publisher = {Springer},
  url       = {http://link.springer.com/article/10.1007/s10703-015-0225-4},
}