Accession Number:

ADA465057

Title:

Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata

Descriptive Note:

Conference paper

Corporate Author:

MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s):

Report Date:

2003-09-08

Pagination or Media Count:

8.0

Abstract:

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.

Subject Categories:

  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE