Jhala, R. (2004). Program verification by lazy abstraction. University of California, Berkeley.

Majumdar, R. (2003). Symbolic algorithms for verification and control. University of California, Berkeley.

Horowitz, B. (2003). Giotto: A time-triggered language for embedded programming. University of California, Berkeley.

Mang, F. (2002). Games in open systems verification and synthesis. University of California, Berkeley.

Qadeer, S. (1999). Algorithms and Methodology for Scalable Model Checking. University of California, Berkeley.

Kopke, P. (1996). The Theory of Rectangular Hybrid Automata. Cornell University.

Ho, P. (1995). Automatic analysis of hybrid systems. Cornell University.