CS 330: Formal Methods and Models
George Mason University Department of Computer Science
Section DL1: Fall 2021 - 9:00-10:15am Tue/Thu - Online
Professor: Ivan Avramovic
Email: iavramo2-at-gmu.edu
Hours: Monday/Thursday 10:30-11:30 (see Piazza for the link)
Phone/Office: (703) 993-5426 / 4609 Engineering (note: I am unlikely to be in the office or check the phone frequently this semester)

Assistants: (see Piazza for hours)

Petar Duric, pduric-at-gmu.edu (GTA)
Gabriel Thomsen, gthomsen-at-gmu.edu (GTA)
Ha Phuong Le, hle36-at-gmu.edu (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 homework 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 and course materials.
GradeScope to for quizzes, tests, and turn-in homework assignments.

Webpage: course webpage can be found at https://cs.gmu.edu/~iavramo2/classes/cs330f21.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 third-party online study sites violate the GMU Honor code: these include accessing exam or quiz questions for this class which have been uploaded by others; 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 very reliant on student integrity 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 Aug 24 Introduction; Mathematical Preliminaries, Sections 1.1-1.6
Aug 26 Propositional Logic, Sections 2.1-2.6 Practice HW 2.4, 2.6, 2.7, 2.10a, 2.11
week 2 Aug 31 Quiz 1 (Ch 1 and 2), Sep 1-3
Sep 2 Proofs by Deduction, Sections 3.1-3.7 GradeScope HW 1 due; Practice HW 3.8, 3.9, 3.11 (2nd-6th)
week 3 Sep 7 Quiz 2 (Ch 3), Sep 8-10
Sep 9 Predicate Logic, Sections 4.1-4.5 GradeScope HW 2 due; Practice HW 4.1, 4.3, 4.7, 4.8a,b
week 4 Sep 14 Quiz 3 (Ch 4), Sep 15-17
Sep 16 Mathematical Induction, Sections 5.1,5.2,5.4,5.5 GradeScope HW 3 due; Practice HW 5.2-5.4, 5.6
week 5 Sep 21 Quiz 4 (Ch 5), Sep 22-24
Sep 23 Program Verification, Sections 6.1-6.4 GradeScope HW 4 due; Practice HW 6.2-6.6
week 6 Sep 28 Quiz 5 (Ch 6), Sep 29-Oct 1
Sep 30 Midterm review GradeScope HW 5 due; Midterm covers material from chapters 1-6; Sample midterm
week 7 Oct 5 Midterm open Oct 4-6
Oct 7 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 Oct 12 No class Fall Break
Oct 14 Quiz 6 (Langs), Oct 15-17
week 9 Oct 19 Regular Expressions; Regular Grammars, Sections 8.4, 8.6, 8.7 GradeScope HW 6 due; Practice HW 8.8, 8.9, 8.11, 8.12
Oct 21 Quiz 7 (REs/RGs), Oct 22-24
week 10 Oct 26 Regular Grammar Conversions, Sections 8.8,8.9 GradeScope HW 7 due; Practice HW 8.14, 8.15
Oct 28 Quiz 8 (RGs), Oct 29-31
week 11 Nov 2 Finite Automata, Sections 9.1-9.4,9.8 GradeScope HW 8 due; Practice HW 9.4, 9.8, 9.16a, 9.17
Nov 4 Quiz 9 (DFAs), Nov 5-7
week 12 Nov 9 Nondeterministic Finite Automata; Properties of Regular Languages, Sections 9.5-9.7 GradeScope HW 9 due; Practice HW 9.5, 9.6, 9.25
Nov 11 Quiz 10 (NFAs), Nov 12-14
week 13 Nov 16 Context-Free Grammars, Sections 10.1-10.4 GradeScope HW 10 due; Practice HW 10.1, 10.2, 10.7
Nov 18 Quiz 11 (Ch 10), Nov 19-21
week 14 Nov 23 Pushdown Automata; Turing Machines, Sections 11.1,11.2, 12.2 GradeScope HW 11 due; Practice HW 11.1, 11.4, 11.6, 11.9a (NPDA are allowed)
Nov 25 No class Thanksgiving Recess
week 15 Nov 30 Quiz 12 (Ch 11), Dec 1-3
Dec 2 Final review GradeScope HW 12 due; Final covers material from chapters 7-12; Sample final
exam week Dec 8-15 Final exam open Dec 7-9