Course Syllabus
The table below gives the planned syllabus for the course. The syllabus lists the topics in order, and gives access to each lecture's meeting outlines, and homeworks and readings.
Material describing the course and its objectives and grading policies is available elsewhere.
This syllabus is subject to change. If it is necessary to revise the schedule, then this page will be updated to reflect the changes.
The readings are from Principles of Programming Analysis (second corrected printing) by Flemming Nielson, Hanne Riis Nielson, and Chris Hankin (Springer-Verlag, 2005).
Dates | Topics | Homework Due | Readings | Optional Readings |
---|---|---|---|---|
Jan. 7 | Introduction | Handouts, Grading Policy | Forward, Preface | |
Jan. 9 | Overview of Analysis Techniques | Ch 1, 1.1-1.2 | ||
Jan. 14 | Overview of Analysis Techniques | Ch 1.3-1.4 | ||
Jan. 16 | Overview of Analysis Techniques | HW1 | Ch 1.5 | |
Jan. 21 | MLK day, no class | |||
Jan. 23 | Overview of Analysis Techniques | Ch 1.6 | ||
Jan. 28 | Intraprocedural Data Flow Analysis | Ch 2.1 | ||
Jan. 30 | Intraprocedural Data Flow Analysis | HW2, p 1-7 | Ch 2.1 | |
Feb. 4 | Intraprocedural Data Flow Analysis | Ch 2.1 | ||
Feb. 6 | Intraprocedural Data Flow Analysis | Ch 2.1 | ||
Feb. 11 | Intraprocedural Data Flow Analysis | HW2, rest | Ch 2.1 | |
Feb. 13 | Theory of Data Flow Analysis | Ch 2.2 | ||
Feb. 18 | Discussion related to homework 2 | HW 3, p 1-9 | Ch 2.2 | |
Feb. 20 | Theory of Data Flow Analysis | Ch 2.2 | ||
Feb. 25 | Theory of Data Flow Analysis | Ch 2.2 | ||
Feb. 27 | Theory of Data Flow Analysis | Ch 2.2 | ||
Mar. 3 | Theory of Data Flow Analysis | Ch 2.2 | ||
Mar. 5 | Theory of Data Flow Analysis | Ch 2.2 | ||
Mar. 10 | Spring Break, no class | |||
Mar. 12 | Spring Break, no class | |||
Mar. 17 | Monotone Frameworks in Data Flow Analysis | HW 3, p 10-15 | Ch 2.3 | |
Mar. 19 | Monotone Frameworks in Data Flow Analysis | Ch 2.3 | ||
Mar. 24 | Interprocedural Data Flow Analysis | Ch 2.5 | ||
Mar. 26 | Interprocedural Data Flow Analysis | Ch 2.5 | ||
Mar. 31 | Interprocedural Data Flow Analysis | Ch 2.5 | ||
Apr. 2 | Interprocedural Data Flow Analysis | Ch 2.5 | ||
Apr. 7 | Data Flow Analysis: Shape Analysis | Ch 2.6 | ||
Apr. 9 | Data Flow Analysis: Shape Analysis | Ch 2.6 | ||
Apr. 14 | Data Flow Analysis: Shape Analysis | Ch 2.6 | ||
Apr. 16 | Data Flow Analysis: Shape Analysis | Ch 2.6 | [Manevich-etal05] | |
Apr. 21 | Course Summary and Evaluations | |||
April 22-25 | Final Oral Exams |
Bibliography
- [Manevich-etal05]
- Roman Manevich, E. Yahav, G. Ramalingam, and Mooly Sagiv. "Predicate abstraction and canonical abstraction for singly-linked lists." In Verification, Model Checking, and Abstract Interpretation, volume 3385 of Lecture Notes in Computer Science, pages 181--198, Berlin, 2005. Springer-Verlag.
Previous syllabi from earlier offerings of the class are also available. See the courses's about page.
Last modified Thursday, April 17, 2008.
This web page is for the Spring 2008 offering of COP 5021 at the University of Central Florida. The details of this course are subject to change as experience dictates. You will be informed of any changes. Please direct any comments or questions to Gary T. Leavens at leavens@eecs.ucf.edu. Some of the policies and web pages for this course are quoted or adapted from other courses I have taught, in particular, COP 4020 and Com S 641.