Course Schedule

The table below gives the planned schedule for this course. The schedule lists the topics in order, and gives access to each lecture's meeting outlines and readings.

This schedule 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).

, Ch 2.2, 2.3,
Date Topic(s) Reading(s) Optional Reading(s)
Jan. 9 Introduction to the class and the need for approximation in program analysis, Grading Policy Forward, Preface [XText18], [Hedin-etal09] (Concept Overview)
Jan. 11 Overview of Analysis Techniques (Dataflow Analysis, Abstract Interpretation, Type and Effect Systems) Forward, Preface; Ch 1, 1.1-1.3, 1.5-1.6 Ch 1.4
Jan. 16 Overview of Analysis Techniques (Dataflow Analysis, Abstract Interpretation, Type and Effect Systems), continued Forward, Preface; Ch 1, 1.1-1.3, 1.5-1.6 Ch 1.4
Jan. 18 Overview of Analysis Techniques (Dataflow Analysis, Abstract Interpretation, Type and Effect Systems), continued Forward, Preface; Ch 1, 1.1-1.3, 1.5-1.6 Ch 1.4
Jan. 23 Overview of Analysis Techniques (Dataflow Analysis, Abstract Interpretation, Type and Effect Systems), continued Forward, Preface; Ch 1, 1.1-1.3, 1.5-1.6 Ch 1.4
Jan. 25 Intraprocedural Data Flow Analysis (Blocks and Labels, Notation, Available Expressions, AE Analysis, Very Busy Expressions, Live Variables, ud and du chains Ch 2.1  
Jan. 25 ASTs and CFGs in Xtext (Attributes, Rewrites) Ch 1.6 Ch 2.1, [XText18], [Hedin-etal09] (Abstract Syntax, Attributes)
Jan. 30 Theory of intraprocedural Data Flow Analysis (modeling programs, control flow graphs, etc.) Ch 2.1  
Feb. 1 Theory of intraprocedural Data Flow Analysis (modeling programs, control flow graphs, etc., Available Expressions Analysis) Ch 2.1  
Feb. 6 Intraprocedural Data Flow Analysis (Reaching Definitions, Very Busy Expressions, Solving Dataflow Equations using Chaotic Iteration) Ch 2.1, 1.7  
Feb. 8 Intraprocedural Data Flow Analysis (Examples with solutions using Chaotic Iteration: Live Variables, ud and du chains, Monotone Frameworks) Ch 1.7, Ch 2.1, Ch 2.3  
Feb. 13 Calculational Proofs and Semantics Overview, Structural Operational Semantics [Gries91], [Dijisktra-Scholten90], Ch. 2 (esp. 2.2) [Back-vonWright98]
Feb. 15 Review for Midterm Exam Ch 1, 2.1  
Feb. 20 Midterm Exam Ch 1, 2.1  
Feb. 22 Midterm recap, Semantics Overview, Structural Operational Semantics Ch 2 (esp. 2.2)  
Feb. 27 Correctness of LV Analysis Ch 2 (esp. 2.2 and 2.3)  
Feb. 29 Interprocedural Dataflow Analysis Ch 2.5  
Mar. 5 Work on projects, no class    
Mar. 7 Work on projects, no class    
Mar. 12 Shape Analysis Ch 2.6 [Manevich-etal05]
Mar. 14 Shape Analysis and Type Checking Ch 2.6 and 1.6 [Manevich-etal05]
Mar. 19 Spring Break, no class    
Mar. 21 Spring Break, no class    
Mar. 26 Type Checking Ch 1.6  
Mar. 28 Type Checking and Type Checking as Abstract Interpretation Ch 1.6 [Cousot97]
Apr. 2 Type Checking as Abstract Interpretation Ch 1.5-1.6 [Cousot97]
Apr. 4 Type Checking as Abstract Interpretation and Abstract Interpretation: Overview and Basics Ch 1.5 and 4.1 [Cousot97] [Cousot-Cousot95]
Apr. 6 Abstract Interpretation: Overview and Basics Ch 4.1 [Cousot-Cousot95]
Apr. 9 Abstract Interpretation: Approximation of Fixed Points Ch 4.2 [Cousot-Cousot95]
Apr. 11 Abstract Interpretation: Approximation of Fixed Points Ch 4.2 [Cousot-Cousot95]
Apr. 16 Project presentations    
Apr. 18 Project presentations    

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.
[Cousot97]
Patrick Cousot. Types as abstract interpretations. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '97). Association for Computing Machinery, New York, NY, USA, pp. 316-331, 1997. https://doi.org/10.1145/263699.263744
[Cousot-Cousot95]
Patrick Cousot and Radhia Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proceedings of the seventh international conference on Functional programming languages and computer architecture (FPCA '95). Association for Computing Machinery, New York, NY, USA, pp. 170-181, 1995. https://doi.org/10.1145/224164.224199
[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 8, 2024.
[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 8, 2024.

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

Last modified Thursday, April 4, 2024.

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