Program Analysis and Verification Group

The Program Analysis and Verification Group (PAVG) is a research group led by Dr. David C. Luckham of the Computer Science Department and Electrical Engineering Department of Stanford University.

Group Members

Current Research: Complex Event Processing

Complex event processing is a new technology developed from Rapide and its analysis toolset. It can be applied to extracting and analyzing information from any kind of distributed message-based system. It is developed from the Rapide concepts of (1) causal event modeling, (2) event patterns and pattern matching, and (3) event pattern maps and constraints. Complex event processing can be applied to a wide variety of Enterprise monitoring and management problems, from low level network management to high level enterprise intelligence gathering.

Previous PAVG Work

• For the past few years, the PAVG has been working on the Rapide language and toolset. Rapide is a language for the definition and simulation of system architectures. Rapide uses a partially-ordered event set execution model to represent true concurrency. In addition, the language includes embedded formal specifications.

• An early version of Rapide, known as Rapide-0.2, explored issues of simulation, the event-based computation model, and implementation that were later developed in the full language.

• Anna (1980-1990), a formal specification language and verification toolset for sequential Ada programs.

• TSL (1983-1990), a specification language and conformance testing tools for concurrent Ada programs.

• VAL (1986-1990), an annotation language for VHDL.

• ADAM (1980), the first tasking compiler for Ada, based on the 1980 preliminary Ada language design, implemented in LISP. Adam was used as the basis for the first Rational Inc. validated Ada compiler (1983).

• The Stanford Pascal Verifier project (1973 - 79).