Sakallah This research is on the temporal modeling of latch- controlled synchronous digital systems. The use of level- sensitive latches, as opposed to edge-triggered flip-flops, has become quite common in recent years because latches are easily implemented in MOS VLSI, the leading technology for building digital systems. A consistent theoretical framework for describing the timing constraints which must be satisfied by such systems for proper operation is being developed. This framework is being used to develop efficient algorithms for timing verification and optimal clocking. Both of these problems require the solution of large linear programs (LPs). The special structures of these LPs will be utilized to reduce the solution time so that the algorithms can be used in an interactive design environment. The practical significance of this framework and associated algorithms is being assessed experimentally on actual industrial VLSI designs.