Temporal Verification and Development of Reactive Programs
Final rept. 15 Feb 93-29 Jun 96
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The REACT research group at Stanford under the supervision of Professor Zohar Manna, developed methodologies and tools for the verification and synthesis of reactive, real-time and hybrid systems based on their temporal specifications. A system, STeP Stanford Temporal Prover, has been implemented to support computer-aided verification and synthesis based on these methodologies and tools. The goal of the system is to automate the development process as much as possible, thereby reducing the errors that otherwise pervade software development. The research group consisted of Prof. Zohar Manna PI, Prof. Amir Pnueli visitor, 8 PhD students, 2 MSc students, and a programmer. One of the PhD students graduated during the period covered by this report. Several of the PhD students were supported by this AFOSR grant.
- Computer Programming and Software