CS 330: Formal Methods and Models
George Mason University Department of Computer Science
Section DL1: Spring 2021 - 9:00-10:15am Tue/Thu - Online
Instructor: Ivan Avramovic
Email: iavramo2-at-gmu.edu
Hours: Monday/Wednesday 10:30-11:30 (see Piazza for the link)

Assistants: (see Piazza for hours and contact info)

Negar Nejatishahidin (GTA)
Minhyuk Ko (UTA)
Suresh Patil (UTA)

Prerequisites: CS211 and MATH125 (C or better in both)
Textbook: Hamburger and Richards, Logic and Language Models for Computer Science, Third Edition
Other requirements:
A computer with reliable Internet, web browser, and audio for use with Blackboard Collaborate Ultra videoconferencing
A scanner, camera, or digital drawing tool to use to prepare digital uploads of quizzes and exams

Lectures: Lectures will be synchronous via Blackboard Collaborate Ultra within the Blackboard section for this course (look in the toolbar on the lefthand side). Each lecture will be recorded and made available online.
Course resources:
Piazza for questions and discussion. Please note that while Piazza now requests donations, it is due to a change in Piazza's business model independent from any input from the university; students should not feel obligated to provide donations.
Blackboard to view grades.
GradeScope to for quizzes, tests, and turn-in homework assignments.

Webpage: course webpage can be found at https://cs.gmu.edu/~iavramo2/classes/cs330s21.html
Schedule: see below for schedule

Description

This course is an introduction to two kinds of formal systems - languages 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. The programming assignments provide practical experience with some theoretical topics.

Outcomes

  1. Students will understand the concepts and relevance of logic, formal languages and automata theory, and computability.
  2. Students will be able to do mechanical formal proofs, program correctness proofs and solve problems in first-order logic.
  3. Students will be able to solve problems in elementary machine models: designing finite-state, pushdown and turing machines.
  4. Students will be able to solve problems in formal languages: writing regular expressions, regular grammars, and context-free grammars.
Topics

Grades

Policies

Honor Code

All graded work in this class is individual. Any direct contribution on a quiz, exam, or assignment will be treated as a violation of George Mason's Honor Code and will typically result in failing the class.

Some kinds of participation in online study sites violate the GMU Honor code: these include accessing exam or quiz questions for this class; accessing exam, quiz, or assignment answers for this class; uploading of any of the instructor's materials or exams; and uploading any of your own answers or finished work. Always consult with the course instructors before using these sites.

As a practical matter, we are more reliant on student integrity than ever during an online semester. Please respect the importance of upholding the Honor Code, since it affects the meaningfulness of your degree and the degrees of other students.

Privacy statment

All course materials posted to Blackboard or other course site are private to this class; by federal law, any materials that identify specific students (via their name, voice, or image) must not be shared with anyone not enrolled in this class. All of our synchronous meetings in this class will be recorded to provide necessary information for students in this class. Recordings will be stored on Blackboard and will only be accessible to students taking this course during this semester.

Disability accomodations

Disability Services at George Mason University is committed to providing equitable access to learning opportunities for all students by upholding the laws that ensure equal treatment of people with disabilities. Students seeking accommodations for this class, please first visit Disability Services (ods@gmu.edu; 703-993-2474) for detailed information about the Disability Services registration process. Then please discuss the approved accommodations with the instructor. The Disability Services office can be found in Student Union Building I (SUB I), Suite 2500.

Diversity and inclusion

George Mason University promotes a diverse, inclusive, and anti-racist environment, under the belief that a just and equitable learning environment is a strong learning environment. Students are valued as individuals, irrespective of differences in race, ethnicity, national origin, first language, economic status, gender, gender expression and identity, sexual orientation, religion, disability, or age. As an important member of the GMU community, the Department of Computer Science is integral to the goal of cultivating an environemnt which is committed to inclusion and anti-racism.

Students who prefer to be addressed by a specific name or gender pronouns should share this information with the instructor (he/him). Additionally, name and pronouns can be changed in the GMU records.

Title IX

As a faculty member and designated "Responsible Employee," the instructor is required to report all disclosures of sexual assault, interpersonal violence, and stalking to Mason's Title IX Coordinator, per university policy 1412. Students who wish to speak with someone confidentially, should contact the Student Support and Advocacy Center (ssac@gmu.edu; 703-993-3686) or Counseling and Psychological Services (caps@gmu.edu; 703-993-2380). Assistance may also be sought from GMU's Title IX Coordinator (titleix@gmu.edu; 703-993-8730).

COVID-19

This class is fully online during the Fall semester, so it is not necessary to be on campus to participate in the class. For information regarding the virus and university policy regarding the virus, consult the Safe Return to Campus page.

Schedule

Week Date Topic Assignments/Notes
week 1 Jan 26 Introduction; Mathematical Preliminaries, Sections 1.1-1.6
Jan 28 Propositional Logic, Sections 2.1-2.6 Practice HW 2.4, 2.6, 2.7, 2.10a, 2.11
week 2 Feb 2 Quiz 1 (Ch 1 and 2), Feb 3-5
Feb 4 Proofs by Deduction, Sections 3.1-3.7 Week 1 GradeScope HW due; Practice HW 3.8, 3.9, 3.11 (2nd-6th)
week 3 Feb 9 Quiz 2 (Ch 3), Feb 10-12
Feb 11 Predicate Logic, Sections 4.1-4.5 Week 2 GradeScope HW due; Practice HW 4.1, 4.3, 4.7, 4.8a,b
week 4 Feb 16 Quiz 3 (Ch 4), Feb 17-19
Feb 18 Mathematical Induction, Sections 5.1,5.2,5.4,5.5 Week 3 GradeScope HW due; Practice HW 5.2-5.4, 5.6
week 5 Feb 23 Quiz 4 (Ch 5), Feb 24-26
Feb 25 Program Verification, Sections 6.1-6.4 Week 4 GradeScope HW due; Practice HW 6.2-6.6
week 6 Mar 2 Quiz 5 (Ch 6), Mar 3-5
Mar 4 Midterm review Week 5 GradeScope HW due; Midterm covers material from chapters 1-6; Sample midterm
week 7 Mar 9 Midterm open Mar 5-10
Mar 11 Language Basics; Regular Languages, Chapter 7 + Sections 8.1-8.4 Practice HW 7.4, 7.5, 7.12, 7.15, 8.2, 8.3, 8.6
week 8 Mar 16 Quiz 6 (Langs), Mar 17-19
Mar 18 Regular Expressions; Regular Grammars, Sections 8.4, 8.6, 8.7 Week 7 GradeScope HW due; Practice HW 8.8, 8.9, 8.11, 8.12
week 9 Mar 23 Quiz 7 (REs/RGs), Mar 24-26
Mar 25 Regular Grammar Conversions, Sections 8.8,8.9 Week 8 GradeScope HW due; Practice HW 8.14, 8.15
week 10 Mar 30 Quiz 8 (RGs), Mar 31-Apr 2
Apr 1 Finite Automata, Sections 9.1-9.4,9.8 Week 9 GradeScope HW due; Practice HW 9.4, 9.8, 9.16a, 9.17
week 11 Apr 6 Quiz 9 (DFAs), Apr 7-9
Apr 8 Nondeterministic Finite Automata; Properties of Regular Languages, Sections 9.5-9.7 Week 10 GradeScope HW due; Practice HW 9.5, 9.6, 9.25
week 12 Apr 13 Quiz 10 (NFAs), Apr 14-16
Apr 15 Context-Free Grammars, Sections 10.1-10.4 Week 11 GradeScope HW due; Practice HW 10.1, 10.2, 10.7
week 13 Apr 20 Quiz 11 (Ch 10), Apr 21-23
Apr 22 Pushdown Automata; Turing Machines, Sections 11.1,11.2, 12.2 Week 12 GradeScope HW due; Practice HW 11.1, 11.4, 11.6, 11.9a (NPDA are allowed)
week 14 Apr 27 Quiz 12 (Ch 11), Apr 28-30
Apr 29 Final review Week 13 GradeScope HW due; Final covers material from chapters 7-12; Sample final
exam week May 3-10 Final exam open May 1-6