\documentclass[11pt]{article}
\input{macros-course}

\begin{document}
\handout{schedule}{6.897 Schedule: Version 1}{February 6, 2001}

\begin{description}
\item[Lecture 1] Tuesday, February 6 \\
   Lynch\\
   Overview; State machines, invariants, and levels of abstraction

\item[Lecture 2] Thursday, February 8\\
   Lynch \\
   Other views of state machines, invariants, and abstraction: 
   Manna, Pnueli, and Lamport

\item[Lecture 3] Tuesday, February 13\\
   Lynch \\
   Abstraction relations; Statecharts \\
   {\bf Due:}  Hand in choice of case study area 

\item[Lecture 4] Thursday, February 15\\
   Lynch \\
   Model-checking overview

\item[Lecture 5] Thursday, February 22\\
   ??? \\ % [[[Rui?  TLC expert?]]] \\
   SPIN model-checker

\item[Lecture 6] Tuesday, February 27\\
   ??? \\ % [[[Rui?  TLC expert?]]] \\
   TLC model-checker

\item[Lecture 7] Thursday, March 1 \\
   Ernst\\
   Invariant discovery

\item[Lecture 8] Tuesday, March 6 \\ 
   Garland\\
   Theorem proving

\item[Lecture 9] Thursday, March 8 \\ 
   Garland\\
   Theorem proving, LP

\item[Lecture 10] Tuesday, March 13  \\
   Garland\\
   Theorem proving, LP, IOA

\item[Lecture 11] Thursday, March 15 \\
   Lynch \\
   Simple systems: liveness

\item[Lecture 12] Tuesday, March 20\\
   Attie \\
   Liveness, temporal logic 

\item[Lecture 13] Thursday, March 22 \\
   Lynch\\
   Composition

\item[Lecture 14] Tuesday, April 3\\
   Lynch, Attie \\
   Composition, dynamic systems

\item[Lecture 15] Thursday, April 5\\
   Attie, Jackson \\
   Dynamic systems, relational models

\item[Lecture 16] Tuesday, April 10\\
   Jackson \\ % [[[verify]]]
   Relational models 

\item[Lecture 17] Thursday, April 12 \\
   Lynch\\
   Timed systems

\item[Lecture 18] Thursday, April 19\\
   Lynch \\
   Timed systems

\item[Lecture 19] Tuesday, April 24 \\
   Alur \\
   Timed systems, Uppaal

\item[Lecture 20] Thursday, April 26\\
   Lynch \\
   Timed systems

\item[Lecture 21] Tuesday, May 1 \\ 
   Lynch \\
   Hybrid systems

\item[Lecture 22] Thursday, May 3\\
   Lynch \\
   Hybrid systems

\item[Lecture 23] Tuesday, May 8\\
   ??? \\
   Hytech

\item[Lecture 24] Thursday, May 10\\
   Lynch \\
   Hybrid systems

\item[Lecture 25] Tuesday, May 15 \\ 
   Lynch \\
   Probabilistic systems

\item[Lecture 26] Thursday, May 17\\
   Lynch \\
   Probabilistic systems
   {\bf Due:}  Hand in final ``portfolio'' of case study examples
\end{description}
\end{document}






