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

Re: What comes after PVS?

Since I will not be able to attend the tutorials at FME, I'll ask the 
here on the list. I would be very interested in using the ICS decision 
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 
such as myself. Generating proof obligations to be discharged with an 
tool is awkward, and rather frustrating if it simply involves hitting 
"G" repeatedly
in PVS.