Our laboratory began building tools to support formal methods in the 1970's and we expect to continue doing so for many years to come. Currently, our most widely used tool is the PVS verification system, but we also provide the ICS decision procedures and the SAL toolkit. Some of our users have told us they are perplexed by the range of tools we offer and do not know which is best for their purposes; others have said they are worried that the arrival of our newer tools may signal a weakened commitment to the older ones; still others say they hesitate to adopt the newer tools because their initial incarnations offered only modest capabilities and they wondered where we plan to take them, while others have questions about our licensing terms.
This document attempts to answer these questions: we explain the role that each tool plays within our overall strategy, the synergies between them, and their current capabilities. We then describe the new capabilities that we are developing and using in-house and that will soon be made available in new releases of our tools; finally, we describe directions we expect to explore in future and our plans for existing and new tools.
gzipped postscript
, or
pdf
@techreport{Roadmap03,
Author= {{Formal Methods Program}},
Title= {Formal Methods Roadmap: PVS, ICS, and SAL},
Number= {SRI-CSL-03-05},
Institution= {Computer Science Laboratory, SRI International},
Address= {Menlo Park, CA},
Month= oct,
Year= 2003
}