|Title||Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata|
|Publication Type||Conference Paper|
|Year of Publication||2003|
|Authors||Mitra, S., and M. Archer|
|Conference Name||First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003)|
|Conference Location||Rome, Italy|
In this paper we discuss how we intend to develop a specialized theorem proving environment for the Hybrid I/O 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.
|NRL Publication Release Number|| |