The course will consist of two parts. This first part will cover basic topics in formal methods. The topics will be covered from a historical perspective, with readings from original sources and/or a discussion of the historical context. A list of topics appears below.

1. First Order Logic and Set theory. Set theory and first order logic form the foundations of mathematics and formal reasoning. We will cover the syntax and semantics of first-order logic, basic model theory, basic proof theory, Godel's completeness theorem, the compactness theorem, the Lowenheim-Skolem theorems, Godel's incompleteness theorem, and non-standard models. We will cover aspects of axiomatic set theory. We will discuss how logic is used to model and reason about computation.
2. Undecidability and Decision Procedures. A long standing goal in mathematics and computer science is to automate proof discovery and mathematical reasoning. We will cover basic undecidability results. We will also discuss recent developments in decision procedures, including the DPLL algorithm for deciding SAT (Boolean Satisfiability) and the SMT (Satisfiability modulo theories) framework.
3. Reactive Systems. Reactive systems are non-terminating systems that interact with an environment. To reason about such systems, we will study various temporal logics and calculi, automata on infinite objects, the notions of safety and liveness, and the theory of refinement.
4. Tools and Applications. We will discuss current verification tools, including interactive theorem provers, SMT solvers, and model checkers. We will discuss applications to hardware verification, software verification, databases, and security.

The second part of the course will consist of student presentations and a class project.

1. Presentations. Students will be given the opportunity to select a topic that they want to study in more detail. Students will select a small set of papers on the topic and they will prepare and deliver a presentation in class. I will routinely throw out ideas for presentations.
2. Projects. Students will select a semester-long research project to work on. I will routinely throw out project ideas. Students can work alone or in small groups (preferred). We will have a mini-conference at the end of the semester to which every group will submit a project report. The reports will be evaluated by a program committee consisting of all the students in the class. We will use a conference management system like Easychair for this purpose. The best project will receive a prize.

The intended audience is Ph.D. students who want to explore the use of formal methods in their research (e.g., students in FM, PL, Security, or Databases). The prerequisite is "mathematical maturity," but what is lacking in maturity can often be compensated for with enthusiasm. Motivated Undergraduate and Masters students are also welcome. If you're not sure if this class is appropriate for you, feel free to contact me.

Grades will be based on class participation and homeworks (30%), a class presentation (30%), and a class project (40%).