CS330: Formal Methods and Models
George Mason University, Computer Science, Fall 2019

Instructor: Prof. Foteini Baldimtsi (foteini@gmu.edu)
Office Hours: Wednesday's 3:00PM-5:00PM, Office: Engineering 5333
Lectures: Mondays and Wednesdays 1:30PM-2:45PM, Location: Sandbridge Hall 107

Teaching Assistant: Michael Crawshaw (mcrawsha@masonlive.gmu.edu). 
Office hours:  Thursdays 3pm-4pm, Fridays 1pm-2pm, Office: Engineering 4456


Course Summary

This course is an introduction to two kinds of formal systems - languages (which are treated as sets of strings) and logics - with important applications to computer science. The study of formal languages underlies important aspects of compilers and other language processing systems, as well as the theory of computation. Various systems of logic and automatic reasoning are put to use in artificial intelligence, database theory and software engineering. The entire course will give you practice in precise thinking and proof methods that play a role in the analysis of algorithms.

Prerequisites: CS211 and Math125 (C or better in both). Exposure to Discrete Mathematics (as in MATH125) is important for success in this course.

Objectives: Will understand the concepts and relevance of logic, formal languages and automata theory, and computability.
Will be able to able to do mechanical formal proofs, program correctness proofs and solve problems in first-order logic.
Will be able to solve problems in elementary machine models: designing finite-state, pushdown and Turing machines.
Will be able to solve problems in formal languages: writing regular expressions, regular grammars, and context-free grammars.


Required Materials

Text Book: Logic and Languages Models for Computer Science, 3rd edition. Authors: Dana Richards and Henry Hamberger

Available at the campus bookstore. Note that the 3rd edition is substantially different from the 2nd.


Grading

Assignments: 15% (1 weekly assigned problem, lowest grade dropped)
Quizzes: 25%  (~10 quizzes, lowest grade dropped)

Midterm + Final:
 60%. Of these exams the highest score will count 35%, and the lowest 25%

Homework: Every Monday you will receive a set of 3-5 practice HW problems. One of them will have to be submitted on Blackboard and will be graded.
It will be very hard to do well in this course if you do not do all of the practice homework by yourself, including  all optional problems. You are strongly encouraged to do all of the problems, and to ask questions, in class and in office hours, when you do not understand any of them. Don't start the homework the day before it is due! 
No extensions will be given for homework since we will be solving the assigned problems in class. Group work is not allowed when solving homework - any deviation from this policy will be considered a violation of the GMU Honor Code.
 
Quizzes: Quizzes are short: 1-3 questions and will be given every Wednesday covering the material of last week. Some of the quizzes will be on paper and some will be electronic (you will be notified ahead of time whether that week's quiz is automated or not). For electronic quizzes you will need a laptop or phone to answer the questions, as the results will be tallied immediately. Each single quiz is worth about 2% of your grade. 

Important Exam Dates
Midterm: (tentative) Wednesday 10/09, 1:30pm - 2:45pm
Final: (tentative) Wednesday 12/11, 1:30pm - 4:15pm

Final and Midterm are closed book. On sheet of paper with handwritten notes on one side allowed - has to be submitted along with exam and include student's name. Cannot be photocopied or copying another student's notes.

CS330 Adviser Forms

It is a departmental requirement that students in CS330 must see their adviser and discuss their degree progress. The form can be downloaded here. Be sure to fill out the form before seeing your adviser. Also, if you do it earlier in the semester, you will have a much shorter wait to see your adviser, and you will have more time to correct any problems. Students not fulfilling this requirement will receive an Incomplete grade. (Non-majors and graduate students are not included.) 

Communications and HW submissions

We will use Piazza to communicate with you. You are welcome to set up study groups and discuss course materials with other students. If you have a question about the course you should: (a) Come to office hours, OR (b) Post on Piazza. Do not use private posts/emails to ask technical questions. The rest of the class is probably also interested in your question, so make it public!  

HW submission and electronic quizzes will happen through Blackboard.

Use of Electronics in Class

You will need either a laptop or a phone in order to complete some of the quizzes in class. If you don't own either of these devices please let me know ahead of time to prepare a printed quiz for you. Other than for use with quizzes, I encourage you to leave your devices off. You will find that you learn a lot more, and retain the information better, if you remove the distraction!

Class Schedule (Tentative):

Week  Topic  Suggested Readings  HWS + Quizzes
Week 1
08/26 & 08/28 
Introduction & Class logistics. Math Prelims. Propositional Logic and Proofs
Chapters 1 & 2 08/28
HW1 out
Week 2
09/4
Propositional Logic and Proofs Chapter 2
09/2 HW 1 in
09/4 Quiz 1
HW2 out
Week 3
09/09 & 09/11
Propositional Logic and Proofs
Rules of Inference
Chapter 3

09/09 HW2 in
09/11 Quiz 2
HW3 out 
Week 4
09/16 & 09/18
Predicate Logic and Mathematical Induction Chapter 4  09/16 HW3 in
09/18 Quiz 3
HW4 out
Week 5
09/23 & 09/25
Predicate Logic and Mathematical Induction Chapter 5
        09/25 HW4 in
        09/23 Quiz 4
        HW5 out
 Week 6
 09/30 & 10/02
Program Verification         Chapter 6      09/30 HW5 in
    10/02 Quiz 5
        HW6 out
Week 7        
10/07 & 10/09
Review and Midterm   10/07 HW6 in
Week 8  
10/15 (Tuesday) & 10/16
Formal Languages Chapter 7
    10/16 HW 7 out
Week 9
10/21 & 10/23
 Regular Expressions and Grammars Chapter 8  10/21 HW 7 in
   10/23 Quiz 6
    HW 8 out
 Week 10
10/28 & 10/30
Regular Expressions and Grammars  Chapter 8  10/28 HW 8 in
   10/30 Quiz 7
 HW 9 out
 Week 11
11/04 & 11/06
Finite Automata, Regular Languages  Chapter 9 11/04 HW 9 in
   11/06 Quiz 8
HW 10 out
Week 12
11/11 & 11/13
Finite Automata, Regular Languages  Chapter 9     11/11 HW 10 in
   11/13 Quiz 9
    HW 11 out
 Week 13
11/18 & 11/20
Context Free grammars  Chapter 10       11/13 HW 11 in
   11/20 Quiz 10
        HW 12 out
 Week 14
11/25
Push Down Automata  Chapter 11     11/25 HW 12 in
 Week 15
12/02 & 12/04
Turing Machines + Review  Chapter 12      12/04 Quiz 11