@techreport{TR-IC-13-06,
   number = {IC-13-06},
   author = {Rachid Rebiha and Arnaldo V. Moura and Nadir Matringe},
   title = {Transcendental Invariants Generation for Non-linear Hybrid
                   Systems},
   month = {February},
   year = {2013},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 26 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       We  present  the  first verification methods that automatically
       generate  bases  of invariants expressed by multivariate formal
       power  series  and  transcendental  functions.  We  discuss the
       convergence  of  solutions  generated  over hybrid systems that
       exhibit  non-linear models augmented with parameters. We reduce
       the  invariant  generation  problem  to linear algebraic matrix
       systems,  from  which  one  can  provide  effective methods for
       solving the original problem. We obtain very general sufficient
       conditions  for  the  existence  and  the computation of formal
       power series invariants over multivariate polynomial continuous
       differential   systems.  The  formal  power  series  invariants 
       generated   are   often  composed  by  the  expansion  of  some 
       well-known  transcendental  functions  like  "log" or "exp" and
       have  an  analysable closed-form. This facilitates their use to
       verify  safety properties. Moreover, we generate inequality and
       equality  invariants.  Our  examples,  dealing  with non-linear
       continuous  evolution  similar  to  those present today in many
       critical  hybrid  embedded  systems,  show  the strength of our
       results  and  prove  that some of them are beyond the limits of
       other recent approaches.
  }
}