TitleDeveloping Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata
Publication TypeConference Paper
Year of Publication2003
AuthorsMitra, S., and M. Archer
Conference NameFirst International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003)
Conference LocationRome, 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.

Full Text


NRL Publication Release Number