CIS 890
Advanced Topics in Programming Languages
and Software Foundations
Fall 2021


This course will explore some techniques and tools to verify the reliability of software.

Course Content

There will be two strands:

Program Analysis
using the textbook Principles of Program Analysis by Nielson, Nielson and Hankin,
covering topics such as type systems, abstract interpretation, constraint-based analysis
the Coq proof assistant
as introduced by the online textbook(s) Software Foundations.
The exact content of the course will depend on the interests of the participants
(we may even narrow down to only one strand).


While some material may be uploaded on Canvas, this course is based on in-person class participation.

We will study and learn the concepts through a number of exercises, to be discussed during our weekly meeting.

There will also be presentations by students and instructor, leading to class discussions.

Larger projects could arise from this class.


Torben Amtoft, tamtoft hat ksu dot edu


Thursdays, 1-3pm, in Engineering 2183.


The instructor will respond to emails when he reads them, but he will usually do that only twice or thrice a day (to decrease disruption of productivity).

For questions or comments of general interest, we strongly encourage that you post in the Canvas discussion forum so that also other students will benefit from, and contribute to, the conversation.

The instructor expects to be in his campus office most of the work week;
he will usually have his door shut (as there is a lot of traffic in the corridor) but feel free to knock!


August 26
September 2
September 9
September 16
September 23
September 30
October 7
Class canceled
October 14
October 21
We finish Chapter 4 from Principles of Program Analysis (with selected exercises):
October 28
November 4
November 11
November 18
December 2
December 9
We wrap up the course:

Mandatory Statements