Hardware Verification Integrating Deductive With Algorithmic Technologies.

摘要

The work supported under this grant can be divided into four closely related areas: (1) Verification of real-time and hybrid systems; (2) Static analysis; (3) Automata-based deductive verification of real-time systems; and (4) Abstraction and modularity in deductive verification. The results obtained in these areas have been reported in conference and journal papers referenced in the report. Most of the methods developed have been implemented and evaluated for their utility in the framework of the Stanford Temporal Prover (STeP).