CS 5100/6100, Theory of Computation, Spring 2019, 1:25-2:45 pm, WEB L122

Course material maintained on the CS 6100 Canvas site (5100 students are added there)

Instructor Hours: Mon and Wed, 11am - 12pm, 3428 MEB - or by email appt.

All class emails via Canvas

IMPORTANT: Everyone MUST read the Course Goals and Policies listed  HERE .

Part of this course requires you to run Jupyter notebooks and run the “Jove” automata package I’ve developed and provided at https://github.com/ganeshutah/Jove.git 

Here is how to run Jove under Jupyter notebooks and have fun learning:

You may wish to review background material from CS 3100 here:

Textbook and Reference Material (all on Canvas):

Syllabus (topics, readings, assigned work)

Date of lecture

Topics Covered

Read these before NEXT class

 Work assigned, Resources

Due date shown as [on ...]

Due by class time

1: 1/7

  • Course Intro, background questionnaire
  • Handed out in class
  • Lecture slides
  • Demonstration of Jove
  • ACPP, CEAATL: material that matches the lec of  1/9
  • Slides on RE derivatives covered on 1/9 are here in pptx
  • Same slides in pdf
  • Finish background questionnaire
  • Please do your best and send me by 1/8/19, 9am (camera phone photos OK) of your work
  • This is to give me some quick feedback
  • You may submit fuller version on 1/9 during class

2: 1/9

  • Finite Automata, Derivatives
  • Buchi Automata, NBA (non-deterministic Buchi automata) and inequivalence with DBA
  • Clarke et.al. book chapters on Buchi and Kripke (on Canvas)
  • Typo (swapped a and b) likely in key proof
  • Chapter 21 of CEAAT and SMC as needed to grok the syntax of Promela -  1/14
  • Quiz-1 on canvas
  • [on 1/14]
  • Asg-1 Part A  covering basic exercises using Jove. See Asg-1 Part A  on Canvas.
  • [on 1/16]

3: 1/14

  • LTL, SPIN Model Checker
  • Verify/fix  a broken bubble-sort and binary search
  • Reading : continue with these slides and then read the right sections of CEAATL.

  • Asg-1 Part B (on Canvas) covering, NBA, readings
  • [on 1/23]

4: 1/16

  • LTL, SPIN Model Checker
  • Additional L4 slides
  • Reading : In slides so far suggest reading from CEAATL + when asgs and quizzes are posted, read the necessary material (ask on canvas  if unclear)

  • Quiz2 and Asg2 will be posted 1/18 evening
  • Quiz-2 on canvas
  • [Due on 1/25]
  • Asg-1b covering LTL and SPIN. Solving the MWGC problem plus others
  • [Due on 1/30]

Date of lecture

Topics Covered

Read these before class

 Work assigned, Resources

Due date shown as [on ...]

5: 1/21

  • MLK holiday

6:1/23

  • Introduce the Man,Wolf,Goat,Cabbage problem. Solve their crossing via counterexample to an LTL claim

  • Finish up LTL, SPIN Model Checking

7:1/28

  • BDDs and Minimal DFA

8:1/30

  • PDA, Relationship to Boolean Programs, CFLs, showing completeness
  • Putting it all together: Read Bebop paper of Ball/Rajamani

Date of lecture

Topics Covered

Read these before class

 Work assigned, Resources

Due date shown as [on ...]

9: 2/4

TMs, Decidability, Reduction proofs

10: 2/6

NP-Completeness, Cook-Levin Reduction

11:2/11

SAT

12:2/13

Lambda Calculus, Fixpoint Theory

Date of lecture

Topics Covered

Read these before class

 Work assigned, Resources

Due date shown as [on ...]

13: 2/18

  • President’s day holiday

14: 2/20

CTL model checking

15: 2/25

CTL model checker - deep-dive into source

16: 2/27

First-order Logic

Date of lecture

Topics Covered

Read these before class

 Work assigned, Resources

Due date shown as [on ...]

17: 3/4

SMT, Decision Procedures

18: 3/6

Survey of Papers to Read for Spring Break

3/10 to 3/17

Spring Break

Class in project mode from now on (one lecture per week; the other lecture slot for project 1-1s)

Last lecture is on 4/22 (project presentations before this)

The course will deep-dive into Racket and Formal Synthesis using SMT Methods. Watch out for those topics to be our focus for the rest of the semester.