Temporal Verification and Development of Reactive Programs

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1996
Accession Number
ADA329718

Entities

People

  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Automata
  • Automata Theory
  • Complex Systems
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Hybrid Systems
  • Language
  • Simulations
  • Software Development
  • Specifications
  • Standards
  • Students
  • Verification

Readers

  • Mathematical Modeling and Probability Theory.
  • Research Science/Academic Research