The REACT Research Group

The REACT research group, under the supervision of Professor Zohar Manna, studies the specification, verification and synthesis of concurrent, reactive, real-time and hybrid systems.

Our main ongoing implementation effort is the STeP (Stanford Temporal Prover) verification system.

We are sponsored in part by the National Science Foundation (NSF), and by DARPA's Information Technology Office under the project: Software Development Technologies for Reactive, Real-Time and Hybrid Systems. On-line project information includes:

• 1995 Project Summary (at ITO).
• The 1996 Project Summary (local).
• The 1996 project summary diagram (also available in postscript).
• The 1997 project summary diagram (also available in postscript).

We are also investigating hardware verification, under the project: Hardware Verification: Integrating Algorithmic with Deductive Technologies.

• The 1997 project summary diagram (also available in postscript).

The current REACT group (the STeP team).

Ph.D. Alumni:

• Luca de Alfaro. Thesis: Formal Verification of Probabilistic Systems.
• Arjun Kapur. Thesis: Interval and Point-Based Approaches to Hybrid System Verification.
• Anuchit Anuchitanukul. Thesis: Synthesis of Reactive Programs.
• Hugh McGuire. Thesis: Two Methods for Checking Formulas of Temporal Logic.
• Eddie Chang. Thesis: Compositional Verification of Reactive and Real-time Systems.
• Rajeev Alur. Thesis: Techniques for Automatic Verification of Real-Time Systems.
• Tom Henzinger. Thesis: The Temporal Specification and Verification of Real-Time Systems.

The Stanford home page.

The Computer Science Department home page.

The Theory Division home page.