George Mason University 


CS330 - Formal Methods and Models - Spring 2015

Monday, Wednesday 1:30 – 2:45pm,  Innovation Hall 136



This page last updated on 1/20/2015


Prof. Alexander Brodsky


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


Office hours:  Thursday 3:30 – 5:00 pm

Engineering Bldg 4418 



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



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. 



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.



  1. Logic and Languages Models for Computer Science: second edition, by Richards and Hamburger.

                  (available as a packet at the bookstore) (soon)



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

  Applications: Relational Calculus

        and Datalog                            5-6        Lecture Notes

  Exam #1                                7

  Finite Automata, Regular Expressios    7-9        7-9

  AWK: Regular Expression Application    10         B

  Context-Free Grammars & PDAs           11-12      10-11

  Turing Machines & Computability        13-14      12



Quizzes -- 20%

Programming Assignments -- 20%

Exams -- 60%


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 35%, and the lowest 25%.  


Homework is ungraded.

Quizzes will test homework, typically every other class class.

The lowest quiz grades will be dropped.

There will be small programming assignments in Relational Calculus/ Datalog and AWK. 


All testing is closed book.


There is to be NO group work on the programs. Receiving direct contributions to the code that is submitted is considered a violation of the Honor Code. (See for the GMU and Computer Science guidelines.)


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 note or email from your advisor.



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


TA:   Ivan Avromovic,, hours TBA



NO LAPTOP USAGE during class (If you NEED a laptop for note-taking then speak to me.)