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.

This syllabus is subject to change. If it is necessary to revise the schedule, then this page will be updated to reflect the changes.

Material describing the course and its objectives and grading policies is available elsewhere.

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 the following Friday Readings Optional Readings
Jan. 9 Introduction, Grading Policy, Overview of Analysis Techniques (Syntax and Semantics of WHILE, Parsing and ASTs for WHILE) Handouts, HW0 Forward, Preface; Ch 1, 1.1-1.2 [XText18], [Hedin-etal09] (Concept Overview)
Jan. 16 Overview of Analysis Techniques (Dataflow Analysis, Abstract Interpretation, Type and Effect Systems)   Ch 1.3, 1.5-1.6 Ch 1.4
Jan. 23 ASTs and CFGs in XText (Attributes, Rewrites) Homework 1 (due Jan. 22 and 24) Ch 1.6, Ch 2.1, [XText18], [Hedin-etal09] (Abstract Syntax, Attributes)
Jan. 30 Intraprocedural Data Flow Analysis (Blocks and Labels, Notation, Available Expressions, AE Analysis, Very Busy Expressions, Live Variables, ud and du chains, monotone frameworks)   Ch 2.1, 2.3  
Feb. 6 Theory of AE and LV in XText, Theory of Data Flow Analysis (Monotone frameworks, Equation Solving), Midterm Exam Review HW 2, problems 1-3 Ch 2.1.2-4 [XText18]
Feb. 13 Calculational Proofs, Semantics Overview, Structural Operational Semantics, Correctness of LV analysis HW 2, problem 4 [Gries91], [Dijisktra-Scholten90], Ch. 2 (esp. 2.2) [Back-vonWright98]
Feb. 20 Midterm Exam   Ch 1, 2.1  
Feb. 27 Correctness of LV analysis, Type Checking HW 3, problem 1 Chapter 2 (esp. 2.2 and 2.3)  
Mar. 6 Type Checking in XText HW 3, problems 2-5   [XText18]
Mar. 13 Spring Break, no class      
Mar. 20 Interprocedural Dataflow Analysis   Ch 2.5  
Mar. 27 Very Busy Expressions Analysis in XText HW 3, problems 6-7 Ch 2.1.3  
Apr. 3 Shape Analysis   Ch 2.6 [Manevich-etal05]
Apr. 10 Shape Analysis   Ch 2.6 [Manevich-etal05]
Apr. 17 Project presentations HW 4    

Return to top

Bibliography

[Back-vonWright98]
Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction, section 4.2, Graduate Texts in Computer Science. Springer-Verlag, Berlin, 1998.
[Dijkstra-Scholten90]
Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and program semantics, chapter 4, Springer-Verlag, NY, 1990.
[Gries91]
David Gries. "Teaching calculation and discrimination: A more effective curriculum." Communications of the ACM, 34(3):44-55, March 1991. http://dx.doi.org/10.1145/102868.102870
[Hedin-etal09]
Görel Hedin and others. "JastAdd Manual". http://jastadd.org/web/documentation/reference-manual.php Checked January 4, 2016.
[Manevich-etal05]
Roman Manevich and E. Yahav and G. Ramalingam and Mooly Sagiv. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In Verification, Model Checking, and Abstract Interpretation, Springer-Verlag, Lecture Notes in Computer Science, Vol. 3385, pages 181-198. http://dx.doi.org/10.1007/b105073
[XText18]
Xtext authors. XText Documentation. https://www.eclipse.org/Xtext/documentation/index.html, checked January 4, 2018.

Previous syllabi from earlier offerings of the class are also available. See the courses's about page.

Last modified Tuesday, April 24, 2018.

This web page is for the Spring 2018 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@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.