Temporal Verification and Development of Reactive Programs
Zohar Manna · 1996
Abstract : 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.