CIS-5130 (Analysis of Artifacts) Home Page

This is the home page for Peter Chapin's CIS-5130 course notes for the Fall 2024 semester. Here you will find class handouts, slides used during the lectures, homework assignments, and links to other references of interest.

The course syllabus gives an overview of the course and its content, lists course resources, and describes the grading policy and related issues.
The homework submission area and grade book are on Canvas but all other course resources are here.
Here is a list of the analysis projects chosen by the class members.

Topics

2024-08-26. Course introduction and overview.
2024-08-28. Introduced SPARK. Had a conversation comparing Rust and SPARK.
2024-09-02. No class (vacation).
2024-09-04. Discussed the BinarySearch example. Illustrated loop variants.
2024-09-09. Discussed Homework #1. Discussed the SelectionSort example that uses ghost functions.
2024-09-11. Introduced Frama-C and ACSL.
2024-09-16. ?
2024-09-18. ?
2024-09-23. ?
2024-09-25. ?
2024-09-30. Short discussion of how SPARK deals with memory safety (more discussion pending?) and other topics.
2024-10-02. No class
2024-10-07. No class (Vacation).
2024-10-09. No class (Vacation).
2024-10-14. Henry presented on Rust. Discussed on Rust's memory safety versus SPARK's.
2024-10-16. Discussed the Splint paper with a demonstration of Splint.

Slides

Papers

A detailed bibliography in BibTeX format.

Static Detection of Dynamic Memory Errors by David Evans
Improving Security Using Extensible Lightweight Static Analysis by David Evans and David Larochelle
An Introduction to Memory Safety Concepts and Challenges by Forough Goudarzi (on the AdaCore Blog).
Memory Safety in Ada/SPARK Through Language Features and Tool Support by Forough Goudarzi (on the AdaCore Blog)
Memory Safety in Rust by Ben Brosgol (on the AdaCore Blog)

Samples

An example of a SPARK buffers package. This package provides a fixed length array type to hold characters and a collection of subprograms to manipulate such arrays. Two versions are provided: a version without postconditions and a version with postconditions.

Homework

Homework #1. SPARK. This assignment gives you an opportunity to experiment with SPARK.
Set up Frama-C on Lemuria or on your own system. This entails installing OPAM and then using OPAM to install Frama-C and all its dependencies (which OPAM will figure out for you).
Read the first Splint paper (Static Detection of...).
OPTIONAL. Read the second Splint paper (Improved Security Using...).

Resources

The following are links to relevant resources for this class.

The SPARK Reference Manual.
The SPARK Users Guide.
The opam tool is used to manage OCaml packages, including the OCaml compiler itself.
Objective Caml is a programming language favored by those doing research in formal verification. It is also a good, general purpose functional/imperative/OOP language.
Frama-C is a framework for the analysis of C programs.
ACSL by Example demonstrates ACSL on various "simple" C library-like functions. It can be used as a vehicle for learning ACSL.