Differences
This shows you the differences between two versions of the page.
| Last revision Both sides next revision | |||
|
lat1 [2009/09/18 12:47] vkuncak created |
lat1 [2009/09/18 12:47] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Logic and Automata Theory ====== | ====== Logic and Automata Theory ====== | ||
| + | |||
| + | **In the course, you will learn how specify and verify properties that | ||
| + | give formal meaning to words such as 'eventually' and 'until' and how to | ||
| + | automatically verify that systems satisfy such properties. You will | ||
| + | learn about more general types of finite state machines: machines run | ||
| + | continuously, such as a web server, and machines that accept not only | ||
| + | words (strings) but also trees (tree automata). You will learn about | ||
| + | some of the widely used results such as decision procedures for linear | ||
| + | integer arithmetic, and some classic deep results such as the decision | ||
| + | procedure for monadic second-order logic over (possibly infinite) trees. | ||
| + | You will also see how these results can be applied to verification, but | ||
| + | also synthesis of systems that are correct by construction.** | ||
| ====== Introductory Lecture: Today 1pm-2pm in BC 355 ====== | ====== Introductory Lecture: Today 1pm-2pm in BC 355 ====== | ||