COP 5021 - Program Analysis Spring 2010

Resources

This page provides information on some of the resources available for students in COP 5021. The page is organized as follows:

1. Miscellaneous Resources: about the course, program analysis, semantics in general, and programming languages.

Miscellaneous Resources

The following are some links to various resources you may find useful about this course, program analysis, semantics in general, and programming languages.

Course Resources

• Web page for the book Principles of Program Analysis, by Flemming Nielson, Hanne Riis Nielson, and Chris Hankin (Springer-Verlag, 1999). ISBN 3-540-65410-0.
• The course LaTeX macros directory, which contains files that you can use to do calculational-style proofs and to use the notations from the Nielsen, Nielsen and Hankin book.
• Old homeworks for this course. (Current students should get the homeworks from Webcourses, since this directory is not necessarily kept up to date during the semester.)
• Meeting outlines directory, containing outline files for the "lectures".
• Lecture notes directory, containing strangely formatted notes for the "lectures". We recommend that students use the meeting outlines (above) instead.
• The sources for the WHILE language built with JastAdd are available for anonymous checkout via subversion (SVN) with the command: svn checkout http://refine.eecs.ucf.edu/svn/proganalysis/WHILE/trunk If you use Eclipse, use

  http://refine.eecs.ucf.edu/svn/proganalysis

  as the repository location.

Program Analysis Resources

Most of the links in this section were found by students in the class. Please contribute, and thanks!

General Resources about Program Analysis

• Wikipedia definitions for data flow analysis, abstract interpretation, and type system.
• Wikipedia's list of tools for static code analysis.
• The Program Analysis for Software Tools and Engineering (PASTE) 2007 workshop, which has links to previous PASTE workshops.
• Semantics-Based Program Analysis and Manipulation.
• Summer School on Program Analysis and Transformation from 2005.
• Patrick Cousot's page of research on abstract interpretation, which includes the paper Abstract Interpretation from ACM Computing Surveys, 28(2):324--328, June 1996. See also his MIT course on abstract interpretation.
• Abstract Interpretation in a Nutshell by Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jerome Feret, Laurent Mauborgne, Antoine Mine, David Monniaux, Xavier Rival.
• David Schmidt's notes on abstract interpretation.
• Michael Schwarzbach's lecture notes on static analysis.
• MIT's Program Analysis Group, which has several projects including Daikon.
• IBM's Program Analysis, Transformation, and Visualization group, and page on Program Analysis and Transformation.
• Microsoft's Program Analysis research group.
• Inexpensive Program Analysis group at the University of Virginia.
• Bill Pugh's 2002 University of Maryland class on Program analysis and Understanding.
• Tao Xie's Software Engineering Research Links.
• Set theory page by Wolfram Research.

Tools for Implementing Program Analyses

• PAG/WWW program analyzer generator.
• TVLA, the three-valued logic analysis engine.
• JastAdd a attribute grammar system with extensions that make it suitable for dataflow analysis.
• Crystal Static Analysis Framework for Java programs that can be built as Eclipse plugins.
• Beaver, an LALR(1) parser generator that is used in the JastAdd Java compiler.
• Banshee a tool for building constraint-based analyses. This is a successor to Alex Aiken's BANE system.
• Indus, a "collection of program analyses and transformations implemented in Java to customize and adapt Java programs."
• Soot a Java Optimization Framework.

Applications of Program Analysis

• Findbugs, a tool for finding bugs in Java code.
• Bandera a model checker and model checking framework for Java programs.
• Bogor "an extensible software model checking framework".
• Static source code analysis tools for C (a listing).
• C Global Surveyor, a tool that finds bugs in C programs using abstract interpretation.
• Java PathFinder, and explicit state model checker.
• Superwomble, a "lightweight tool for extracting object models from Java bytecode".

General Semantics Resources

• An Introduction to the Literature on Semantics.
• Gary Leavens's favorite formal method links.

Programming Language Resources

• Lambda the Ultimate programming languages weblog.
• Gary Leavens's programming languages page with various links
• The Types mailing list.
• Other programming language related links.
• Google's directory of programming languages.
• Alligator Eggs! which, believe it or not, teaches you about lambda calculus.
• To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction, another, but more thorough, graphical introduction to lambda calculus.

Return to top

Last modified Monday, January 25, 2010.

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