Re: What comes after PVS?

[Pertti Kellomäki <pk@cs.tut.fi>]

Since I will not be able to attend the tutorials at FME, I'll ask the 
questions
here on the list. I would be very interested in using the ICS decision 
procedures
as part of a compiler I am writing. Are they available for such use? If 
so, what
steps should I take in order to get hold of them?

This is a very exciting development for small-time experimental tool 
builders
such as myself. Generating proof obligations to be discharged with an 
external
tool is awkward, and rather frustrating if it simply involves hitting 
"G" repeatedly
in PVS.
-- 
pertti