Mark Greenstreet

Email: mrg [at] cs [dot] ubc [dot] ca
Office: ICCS 323
Phone: 604-822-3065

Curriculum Vitae

B.S., California Institute of Technology (1981); M.Sc., Princeton University (1988); Ph.D., Princeton University (1993); Senior Engineer, ESL Inc. (1982-1985); Visiting Lecturer, Aarhus University (1985-1987); Assistant Professor, University of British Columbia (1992-1997); Associate Professor, University of British Columbia (1997-).


dynamical systems
formal methods
hybrid systems
VSLI design and verification


VLSI Design and Verification

I am developing models and tools for verifying that circuits as modeled by non-linear, ordinary differential equations correctly implement digital behaviours. Part of this is developing a 'topology of discrete behaviour'. A complementary part is developing symbolic and numerical tools for verifying that real designs actually behave as intended. This work contributes to making designs reliable and provides insight that leads to higher performance design.

I strongly believe that verification must be complemented by implementation. In recent years, implementations have taken the form of a proof-of-concept chip for STARI, a high-performance communication protocol, design of a controller for a computer controlled model train, and design of a high performance arbitration circuit. I'm currently working on designs for high-speed pipelines and clock distribution networks.

Hybrid Systems

I have been developing techniques for verifying that a circuit in a continuous model correctly implements a discrete specification. This involves finding invariant sets of systems of non-linear differential equations corresponding to CMOS circuits. In the next four years, I will to apply these techniques to a wider range of designs including high-speed CMOS circuits and system-level interconnect. I will also explore applications of these methods to other engineering domains such as embedded controllers for internal combustion engines and rules for free-flight air traffic control.

Lightweight Theorem Proving

With my students, I have developed a lightweight theorem prover that allows the combination of deductive theorem proving with heuristic decision procedures in an intuitive framework. Our initial success with this approach motivates further exploration. In particular, I am interested in incorporating decision procedures for timed automata and our reachabilty procedures for systems modeled by differential equations.

Selected Publications

Greenstreet, M., "Reachability Analysis Using Polygonal Projections", with Ian Mitchell. Proceedings of the 2nd International Workshop on Hybrid Systems: Computation and Control, pages 103-116, March 1999.

Greenstreet, M. "A Light-Weight Framework for Hardware Verification", with Christoph Kern and Tarik Ono-Tesfaye. Proceedings of TACAS'99, pages 330-344, March 1999.

Greenstreet, M., "Self-Timed Meshes are Faster Than Synchronous", with Peggy B.K. Pang. Proceedings of Async97, pages 30-39, April 1997.

Greenstreet, M., "Implementing a STARI Chip". Proceedings of ICCD'95.

Latest CS Courses

2016 Winter

CPSC 513  –  Introduction to Formal Verification and Analysis
CPSC 418  –  Parallel Computation
CPSC 538G  –  Topics in Computer Systems

2015 Winter

CPSC 513  –  Integrated Systems Design
CPSC 418  –  Parallel Computation

a place of mind, The University of British Columbia


ICICS/CS Building 201-2366 Main Mall
Vancouver, B.C. V6T 1Z4 Canada
Tel: 604-822-3061 | Fax: 604-822-5485
Undergrad program:
Graduate program:

Emergency Procedures | Accessibility | Contact UBC | © Copyright The University of British Columbia