COP 5021 - Program Analysis Spring 2016

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.
• 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.
• The Astrée Static Analyzer.
• 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.
• 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.
• 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.
• Implementing a JIT Compiled Language with Haskell and LLVM, by Stephen Diehl.
• 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.

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.
• 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 Saturday, March 29, 2014.

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