[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Array bounds checking




 Hi !
I have been told that pvs is specially good at handling Praesburger's
arithmetics, with the example of array bounds checking. Could you point me
to the theorems & lemmas used / articles about this process ?

Thanks,
  David

===
 David Teller
  David.Teller@ens-lyon.fr
   Editions Vigdor, ddt@vigdor.com
    http://www.vigdor.com

Les Mots appartiennent  ceux qui savent s'en servir.
N'est-ce pas ?