George Mason University 

DEPARTMENT OF COMPUTER SCIENCE

CS330 - Formal Methods and Models - Fall 2024


1:30–2:45, Enterprise 178


Prerequisites | Description | Readings | Syllabus | Grading | Late | TA | Dates


This page last updated on 5/12/2024


Professor Dana Richards 

703-993-1545 

richards@gmu.edu

(Please prefix the subject of your email with CS330.) 


Course office hours: Tuesday 3:00-5:00 or by appt.

Engineering Building - Room 5320 


PREREQUISITES : 

CS211 and Math 125 (C or better in both).


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 :

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.


READINGS: 

  1. Logic and Languages Models for Computer Science: Fourth edition. 


SYLLABUS:


The pace is approximate. Later chapters will not be covered as completely. 


  Topic                                 Week        Part/Chapters


  Introduction                           1          1

  Propositional Logic and Proofs         1-2        2-3

  Predicate Logic and Proofs             3-4        4-5

  Program Verification     5-6        6

  Exam #1                                7

  Regular Languages and Finite Automata  7-10       7-9

  Context-Free Languages and PDAs        11-12      10-11

  Turing Machines & Computability        13-14      12

 

GRADING : 


Quizzes -- 30%

Exams --   70%


The two exams, including the final, each cover about a half of the semester; the final is not cumulative. 

Of these exams the highest score will count 40%, and the lowest 30%.  Exam1 is Oct 10 and Exam 2 is Dec 17.


Homework is ungraded.

Quizzes will test homework, typically every other class.

The lowest quiz grade will be dropped.

No a priori mapping between scores and grades; the final histogram is used to apportion grades.


All testing is closed book, but limited notes are permitted, as follows for exams (but not for quizzes). One sheet of notes (8.5 by 11 inches, 1 side only). NO COPYING is allowed. That means no photocopying of anything, even the textbook, though you may write out material from it verbatim. It also means no copying of anyone else's notes, even by hand. You may use a computer for editing your own notes. The sheet must be turned in with your exam. Violations of these rules for creating the notes is considered a violation of the Honor Code. 


NO assistance with graded work is allowed, human or otherwise. Receiving direct contributions to submitted work is considered a violation of the Honor Code. (See cs.gmu.edu/wiki/pmwiki.php/HonorCode for the GMU and Computer Science guidelines.)  The common policies of all courses is at https://stearnscenter.gmu.edu/home/gmu-common-course-policies/.

It is a departmental requirement that students in CS330 must see their advisor and discuss their degree progress.  Students not fulfilling this requirement will receive an Incomplete grade. (Non-majors and graduate students are not included.)  The visit must be documented by a signed form (https://cs.gmu.edu/media/uploads/programs/undergraduate/files/advisingcs330.pdf) or email from your advisor.

LATENESS: 

Programs will be marked down 25% each day they are late; in particular, it is marked down 25% after the due date.


TA:    Chuan Yan, cyan3@gmu.edu


NO LAPTOPS, PHONES, ETC. (If you NEED a laptop for note-taking then speak to me.)