Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
In this paper we discuss how we intend to develop a specialized theorem proving environment for the Hybrid IO Automata HIOA framework over the PVS theorem prover, and some of the issues involved. In particular, we describe approaches to using PVS that allow and encourage the development of useful proof strategies, and note some desired PVS features that would further help us to do so for our HIOA environment.