@InProceedings{BadLeuSma09,
  author = 	 {Bahareh Badban and Stefan Leue and Jan-Georg Smaus},
  title = 	 {Automated Invariant Generation for the Verification
                  of Real-Time Systems},
  booktitle = 	 {Proceedings of the 2nd International Workshop on
                  Invariant Generation},
  year =	 2009,
  editor =	 {Andrew Ireland and Laura Kovacs},
  subproject =   {R3},
  access =       {open},
  bibtex =       {badban-etal-wing2009.bib},
  pdf =          {badban-etal-wing2009.pdf},
  abstract =     {We present an approach to automatically generating 
                  invariants for timed automata models. The CIPM algorithm 
                  that we propose first computes new invariants for timed 
                  automata control locations taking their originally defined 
                  invariants as well as the constrains on clock variables 
                  imposed by incoming state transitions into account. In 
                  doing so the CIPM algorithm also prunes idle transitions, 
                  which are transitions that can never be taken, from the 
                  automaton. We discsuss a prototype implementation of the 
                  CIPM algorithm as well as some initial experimental 
                  results.},
}