Automated deduction: decision procedures, theorem proving,
automated-based techniques.
Semantics, specification, and verification of reactive, embedded, real-time, and hybrid systems.
Systematic development, automatic synthesis and control.
Temporal logic and its applications. Automatic and machine-supported
verification systems. Static analysis.
The STeP (Stanford Temporal
Prover) system supports the computer-aided formal verification of
reactive, real-time and hybrid systems based on their temporal specification.
Selected Books
- Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems:
Progress. Unpublished, 1996. Click here to download.
-
Zohar Manna. Mathematical
theory of computation. McGraw Hill, 1974
Translations:
Czech Italian Japanese Hungarian Bulgarian Russian
Verification:
Theory and Practice (Dedicated to Zohar Manna on his 64th Birthday).
Springer-Verlag, LNCS 2772, 2004.
Recent Courses
-
CS156
(Fall 2008) Calculus of Computation. This course presents an
introduction to software verification. It covers the foundation of reasoning
about programs from first principles: specifications and program annotations
are represented by first-order logic formulas; program statements are
represented by first-order transformation relations. It also covers decision
procedures for arithmetic over the reals, for arithmetic over the integers,
for recursive data structures and arrays, and for combinations of theories.
-
CS 157 Introduction
to logic for computer science. An elementary exposition, from a computational
point of view, of propositional logic, predicate logic, axiomatic theories,
and theories with equality and induction. Basic notions: interpretations,
models, validity, proof. Automated deduction: polarity, skolemization,
unification, resolution, equality, strategy along with applications.
-
CS 256 (Spring 2008) Formal
methods for reactive and concurrent systems. This course covers specification
and verification of reactive systems, that is, systems that maintain an
ongoing interaction with their environment. Verification methods are presented
for proving that such reactive systems meet their specifications, expressed
in temporal logic. Verification methods include deductive methods based
on theorem proving, as well as algorithmic methods based on model checking.
The course also places emphasis on temporal logics , their expressive power
and the applications of automata theory in formal methods.
- CS 357
Topics
in Formal Methods. This course covers specification and verification
of reactive systems, with emphasis on real-time and hybrid systems. Verification
methods are discussed for proving that such reactive systems meet their
specifications, with emphasis on methods that combine deductive and algorithmic
techniques, tree and alternating automata and their applications to Formal
Methods.
The
STeP
Group home page
The Stanford home page.
The Computer Science Department home page.
The Theory Division home page.
