CS 330: Formal Methods and Models
George Mason University Department of Computer Science
Section 003: Fall 2023 - 1:30pm-2:45pm Mon/Wed - 2014 Horizon Hall
Section 005: Fall 2023 - 10:30am-1:10pm Friday - 178 Enterprise Hall

Professor: Ivan Avramovic
Email NetID: iavramo2
Hours: 10:00-11:00am Monday; 12:00-1:00pm Wednesday
Phone: (703) 993-5426
Office: D215K Buchanan Hall

Assistants: (see Piazza for hours)

GTA: John Atwood (jatwood4)
GTA: Petar Duric (pduric)
GTA: Yong Li (yli69)
UTA: Qasim Shahid

Prerequisites: CS211 and MATH125 (C or better in both)
Textbook: Hamburger and Richards, Logic and Language Models for Computer Science, Fourth Edition
Other requirements:
A scanner, camera, or digital drawing tool to use to prepare digital uploads of homework

Lectures: Lectures will be held in-person; Supporting videos will be available via Blackboard.
Course resources:
Piazza for questions and discussion. Please note that while Piazza requests donations, it is due to Piazza's business model independent from any input from the university; students should not feel any obligation to provide donations.
Blackboard to view grades and course materials.
GradeScope for exam feedback, quizzes, and homework assignment turn-in/feedback.

Schedule: see below for schedule; subject to change.

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

Grading Scale

Grade A+AA- B+BB- C+CC- DF
max 9791 898781 797771 6959
min 989290 888280 787270 60

Advising Requirement

It is a departmental requirement that all undergraduate Computer Science students taking CS330 must speak with their faculty advisor during the semester and submit an advising form (found here) documenting their visit.

Honor Code

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

The use of AI tools (including but not limited to ChatGPT) to aid in the completion of graded assignments/quizzes/exam, and the use of solutions which are derived directly or indirectly from AI prompts, is considered unauthorized assistance and is prohibited under the honor code.

Some kinds of participation in third-party online study sites violate the GMU Honor code: these include accessing questions for this class which have been uploaded by others; accessing exam 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. It is your resposibility to protect your work, including protecting your computer with a password and avoiding sites which make your work publicly visible. Always consult with the professor before using these sites.

Please respect the importance of upholding the Honor Code, since it affects the meaningfulness of your degree and the degrees of other students. As a practical matter, an understanding of the material presented in this course has a potential to positively impact your ability to acquire computing skills and perform computing skill which will be used in your future careers; you put yourself in the best position to gain that understanding when you rely on your own work.

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. In the event that any class meetings need to be held synchronously online, those classes 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," I am 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 in person during the current semester. For information regarding the virus and current university policy regarding the virus, consult the Safe Return to Campus page.

Schedule

.
Week Date Topic Assignments/Notes
Week 1 Aug 20-26 Introduction; Mathematical Preliminaries, Sections 1.1-1.6. Propositional Logic, Sections 2.1-2.7.
  Aug 21 Introduction; Mathematical Preliminaries (003)
 
  Aug 23 Propositional Logic (003) Practice HW 2.4, 2.7a, 2.8, 2.9, 2.11
 
  Aug 25 Introduction; Mathematical Preliminaries; Propositional Logic (005) Practice HW 2.4, 2.7a, 2.8, 2.9, 2.11
Week 2 Aug 27-Sep 2 Proofs by Deduction, Sections 3.1-3.9.
  Aug 28 Propositional Logic review (003)
Aug 29 Turn-in HW 1 (Prop Logic) assigned
Aug 30 Proof by Deduction (003) Practice HW 3.7, 3.8, 3.10 (1st-4th)
 
Sep 1 Propositional Logic review; Proof by Deduction (005) Practice HW 3.7, 3.8, 3.10 (1st-4th)
Week 3 Sep 3-9 Predicate Logic, Sections 4.1-4.5.
Sep 4 No Class Labor Day
Sep 5 Turn-in HW 1 (Prop Logic) due; Quiz 1 closes (Intro/Prop Logic; opened Saturday)
Sep 6 Proof by Deduction review (003)
  Sep 7 Turn-in HW 2 (Deduction) assigned
Sep 8 Proof by Deduction review; Predicate Logic (005) Practice HW 4.1, 4.3, 4.7, 4.10a,b
Week 4 Sep 10-16 Mathematical Induction, Sections 5.1-5.5.
Sep 11 Predicate Logic (003) Practice HW 4.1, 4.3, 4.7, 4.10a,b; Turn-in HW 2 (Deduction) due
Sep 12 Quiz 2 closes (Deduction; opened Saturday)
Sep 13 Predicate Logic review (003)
Sep 14 Turn-in HW 3 (Pred Logic) assigned
Sep 15 Predicate Logic review; Mathematical Induction (005) Practice HW 5.2-5.4, 5.9
Week 5 Sep 17-23 Program Verification, Sections 6.1-6.4.
Sep 18 Mathematical Induction (003) Practice HW 5.2-5.4, 5.9; Turn-in HW 3 (Pred Logic) due
Sep 19 Quiz 3 closes (Pred Logic; opened Saturday)
Sep 20 Mathematical Induction review (003)
Sep 21 Turn-in HW 4 (Induction) assigned
Sep 22 Mathematical Induction review; Program Verification (005) Practice HW 6.2-6.4, 6.6, 6.7
Week 6 Sep 24-30 Midterm warm-up.
Sep 25 Program Verification (003) Practice HW 6.2-6.4, 6.6, 6.7; Turn-in HW 4 (Induction) due
Sep 26 Quiz 4 closes (Induction; opened Saturday)
Sep 27 Program Verification review (003)
Sep 28 Turn-in HW 5 (Prog Verif) assigned
Sep 29 Program Verification review; Midterm warm-up (005) Midterm covers material from chapters 1-6
Week 7 Oct 1-7 Language Basics; Regular Languages, Chapter 7 + Sections 8.1-8.2
Oct 2 Midterm warm-up (003) Turn-in HW 5 (Prog Verif) due
Oct 3 Quiz 5 closes (Prog Verif; opened Saturday)
Oct 4 Midterm Exam Section 003
 
Oct 6 Midterm Exam Section 005; Language Basics/Regular Languages Practice HW 7.4, 7.5, 7.12, 7.15, 8.2, 8.3, 8.6
Week 8 Oct 8-14 Regular Expressions/Regular Grammars, Sections 8.2-8.5
Oct 9 No Class Fall Break
Oct 10 Language Basics/Regular Languages Monday classes meet; Practice HW 7.4, 7.5, 7.12, 7.15, 8.2, 8.3, 8.6
Oct 11 Language Basics/Regular Languages review (003)
  Oct 12 Turn-in HW 6 (Langs/RLs) assigned
Oct 13 Language Basics/Regular Languages review; Regular Expressions/Regular Grammars (005) Practice HW 8.8, 8.9, 8.11, 8.12
Week 9 Oct 15-21 Regular Grammar Conversions, Sections 8.5,8.6
Oct 16 Regular Expressions/Regular Grammars (003) Practice HW 8.8, 8.9, 8.11, 8.12; Turn-in HW 6 (Langs/RLs) due
Oct 17 Quiz 6 closes (Langs/RLs; opened Saturday)
Oct 18 Regular Expressions/Regular Grammars review (003)
Oct 19 Turn-in HW 7 (REs/RGs) assigned
Oct 20 Regular Expressions/Regular Grammars review; Regular Grammar Conversions (005) Practice HW 8.14, 8.15
Week 10 Oct 22-28 Finite Automata, Sections 9.1-9.4,9.8
Oct 23 Regular Grammar Conversion (003) Practice HW 8.14, 8.15; Turn-in HW 7 (REs/RGs) due
Oct 24 Quiz 7 closes (REs/RGs; opened Saturday)
Oct 25 Regular Grammar Conversion review (003)
Oct 26 Turn-in HW 8 (RG Conv) assigned
Oct 27 Regular Grammar Conversion review; Finite Automata (005) Practice HW 9.7, 9.5, 9.16a, 9.17
Week 11 Oct 29-Nov 4 Nondeterministic Finite Automata/Properties of Regular Languages, Sections 9.5-9.7
Oct 30 Finite Automata (003) Practice HW 9.7, 9.5, 9.16a, 9.17; Turn-in HW 8 (RG Conv) due
Oct 31 Quiz 8 closes (RG Conv; opened Saturday)
Nov 1 Finite Automata review (003)
Nov 2 Turn-in HW 9 (FA) assigned
Nov 3 Finite Automata review; Nondeterministic Finite Automata/Properties of Regular Languages (005) Practice HW 9.8, 9.9, 9.25
Week 12 Nov 5-11 Context-Free Grammars, Sections 10.1-10.4
Nov 6 Nondeterministic Finite Automata/Properties of Regular Languages (003) Practice HW 9.8, 9.9, 9.25; Turn-in HW 9 (FA) due
Nov 7 Quiz 9 closes (FA; opened Saturday)
Nov 8 Nondeterministic Finite Automata/Properties of Regular Languages review (003)
Nov 9 Turn-in HW 10 (NFA/Prop RLs) assigned
Nov 10 Nondeterministic Finite Automata/Properties of Regular Languages review; Context-Free Grammars (005) Practice HW 10.1, 10.2, 10.8
Week 13 Nov 12-18 Pushdown Automata/Turing Machines, Sections 11.1,11.2, 12.2
Nov 13 Context-Free Grammars (003) Practice HW 10.1, 10.2, 10.8; Turn-in HW 10 (NFA/Prop RLs) due
Nov 14 Quiz 10 closes (NFA/Prop RLs; opened Saturday)
Nov 15 Context-Free Grammars review (003)
Nov 16 Turn-in HW 11 (CFGs) assigned
Nov 17 Context-Free Grammars review; Pushdown Automata/Turing Machines (005) Practice HW 11.1, 11.4, 11.6, 11.9a (NPDA are allowed)
Week 14 Nov 19-25
Nov 20 Pushdown Automata/Turing Machines (003) Practice HW 11.1, 11.4, 11.6, 11.9a (NPDA are allowed); Turn-in HW 11 (CFGs) due
Nov 21 Quiz 11 closes (CFGs; opened Saturday)
Nov 22 No class Thanksgiving
Nov 23 No class Thanksgiving
Nov 24 No class Thanksgiving
Week 15 Nov 26-Dec 2 Final Exam warm-up Quiz 11 (PDA/TMs; opened Saturday) closes Sunday Dec 3
Nov 27 Pushdown Automata/Turing Machines review (003)
Nov 28
Nov 29 Final Exam warm-up (003) Final covers material from chapters 7-12
Nov 30
Dec 1 Pushdown Automata/Turing Machines review; Final Exam warm-up (005) Final covers material from chapters 7-12
exam week Dec 6-13 Reading Days Dec 4-5
Dec 6 (Wed) Final Exam Section 003 1:30-4:15pm Sec 003
 
Dec 8 (Fri) Final Exam Section 005 10:30am-1:15pm Sec 005