The Course Bibliography

All the material used in this course has been taken from a number of books and papers, which are listed in this webpage. Each group of slides cites, on its first page, the sources that have been used in its conception. By clicking on the image of the book, or paper, you will be redirected to a webpage providing further information about that material.

Books

The "Dragon Book" is perhaps the most well-known book about compilers. It covers the many different aspects of the design and implementation of a compiler, from the parser to the code generator. We have used Chapter 9 of this book heavily in our discussions about dataflow analysis.
Principles of Program Analysis is a very nice compilation of many different techniques used in the static analysis of code. This book is rigorously formal, and contains some very nice proofs. Our class on contraint based analysis was taken from the third chapter of this book. Many examples that we use througout the course have also been taken from it.
Data Flow Analysis - Theory and Practice offers one of the most complete descriptions about the data-flow framework that I know. The book is particularly deep in regards to interprocedural analyses. This is a bit in contrast to other books, that focus mostly on the intra-procedural aspects of data-flow techniques.
Modern Compiler Implementation in Java is a book that also covers the many aspects of a compiler design and implementation. The last chapters, about code analysis and optimization, are particularly nice. Most of our discussion about SSA form have been taken from this book, as well as the material about loop optimizations.
Lecture Notes in Static Analysis is probably the best collection of lecture notes about static program analyses. In this book (which is publically available!) Michael Schwartzbach covers, in a very concise way, everything that we teach in DCC888, from dataflow to pointer analyses.

Papers

wave propagation and deep propagation for pointer analysis: this paper discuss the wave propagation algorithm that we use in the lecture about pointer analysis. It also contains a brief, yet illustrative, discussion about pointer analysis in general.
Parameterized Construction of Program Representations for Sparse Dataflow Analyses: this paper describes a general way to build program representations for sparse data-flow analyses. Each of these program representations ensures that the information associated with a variable is unique along this variable's entire live range.
A Survey on Register Allocation: This paper provides an overview of some of the most well-known register allocation techiniques, including linear scan, graph coloring, integer linear programming and partitioned boolean programming. We also look into SSA-based register allocation, including SSA-elimination and spilling.
A Framework for End-to-End Verification and Evaluation of Register Allocators: This paper validates a register assignment (plus spilling) using a type system. This proof has been mecanized in Twelf, and it is available on-line. This paper also compares different register allocators; hence, it is a good source of references to several well-known implementations.
Twelf's soundness proofs: These are the scripts used ot prove the soundness of the type system used in the paper "A Framework for End-to-End Verification and Evaluation of Register Allocators". The proof comes in a number of files, but you can grab all of them in this zip.

Última atualização: 07 de Julho de 2007.

Last update: July 7^th, 2007.

	The "Dragon Book" is perhaps the most well-known book about compilers. It covers the many different aspects of the design and implementation of a compiler, from the parser to the code generator. We have used Chapter 9 of this book heavily in our discussions about dataflow analysis.
	Principles of Program Analysis is a very nice compilation of many different techniques used in the static analysis of code. This book is rigorously formal, and contains some very nice proofs. Our class on contraint based analysis was taken from the third chapter of this book. Many examples that we use througout the course have also been taken from it.
	Data Flow Analysis - Theory and Practice offers one of the most complete descriptions about the data-flow framework that I know. The book is particularly deep in regards to interprocedural analyses. This is a bit in contrast to other books, that focus mostly on the intra-procedural aspects of data-flow techniques.
	Modern Compiler Implementation in Java is a book that also covers the many aspects of a compiler design and implementation. The last chapters, about code analysis and optimization, are particularly nice. Most of our discussion about SSA form have been taken from this book, as well as the material about loop optimizations.
	Lecture Notes in Static Analysis is probably the best collection of lecture notes about static program analyses. In this book (which is publically available!) Michael Schwartzbach covers, in a very concise way, everything that we teach in DCC888, from dataflow to pointer analyses.

	wave propagation and deep propagation for pointer analysis: this paper discuss the wave propagation algorithm that we use in the lecture about pointer analysis. It also contains a brief, yet illustrative, discussion about pointer analysis in general.
	Parameterized Construction of Program Representations for Sparse Dataflow Analyses: this paper describes a general way to build program representations for sparse data-flow analyses. Each of these program representations ensures that the information associated with a variable is unique along this variable's entire live range.
	A Survey on Register Allocation: This paper provides an overview of some of the most well-known register allocation techiniques, including linear scan, graph coloring, integer linear programming and partitioned boolean programming. We also look into SSA-based register allocation, including SSA-elimination and spilling.
	A Framework for End-to-End Verification and Evaluation of Register Allocators: This paper validates a register assignment (plus spilling) using a type system. This proof has been mecanized in Twelf, and it is available on-line. This paper also compares different register allocators; hence, it is a good source of references to several well-known implementations.
	Twelf's soundness proofs: These are the scripts used ot prove the soundness of the type system used in the paper "A Framework for End-to-End Verification and Evaluation of Register Allocators". The proof comes in a number of files, but you can grab all of them in this zip.