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

Help



Purnendu Sinha writes:
 > Is the module "Sums" used in verification of Interactive Convergence
 > Clock Synchronization Algorithm by EHDM available as theory in PVS?
 > 
 > Here "Sums" is sum(i, j, F) = \sum_{r = i}^{j} F(r). 
 > 
 > Thanks in advance.
 > 
 > --Purnendu
 > 

This is available in theory sigma_real from the NASA repository for
PVS libraries.  The dump file can be retreived from:

  http://atb-www.larc.nasa.gov/ftp/larc/PVS-library/reals.dmp

Cheers,

-- 
-- Paul S. Miner                | email: p.s.miner@larc.nasa.gov
-- 1 South Wright St. / MS 130  |   fax: (757) 864-4234
-- NASA Langley Research Center | phone: (757) 864-6201
-- Hampton, Virginia 23681-0001 |  

P.S.  I would be interested in seing any work you do on clock
synchronization in PVS.