Accession Number : ADA329718

Title :   Temporal Verification and Development of Reactive Programs

Descriptive Note : Final rept. 15 Feb 93-29 Jun 96

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Manna, Zohar

PDF Url : ADA329718

Report Date : NOV 1996

Pagination or Media Count : 12

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.

Descriptors :   *SOFTWARE ENGINEERING, *SYSTEMS ANALYSIS, *COMPUTER PROGRAM VERIFICATION, ALGORITHMS, REAL TIME, COMPUTER LOGIC.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE