CS 4950: Precise Software Analysis (Seminar)
Fall 2020

This course introduces a field of computer science that uses strict mathematical, logical and algorithmic techniques to analyze software behavior, mostly in the interest of finding critical functionality, security, or performance errors. (Think of airplanes with a buggy flight controller.) This course is not about software testing.

This is a relatively low-load, low-credit (1h) course. The material part of the course is most valuable for those with interest in software and its semantics, and algorithmic techniques to analyze it. The methodological part of the course is most valuable for those contemplating a graduate-student career, and perhaps an area for grad-level research.
Precise Software Analysis



... = CS 3950, which is a generic introduction to computer-science research. The present course, 4950, is a follow-up for people interested in a sneak preview of research in a particular sub-area of computing. There are different sections with different sub-areas. This website talks about Section 1, where the sub-area is a field that we here call "Precise Software Analysis".

We do not assume any prior knowledge from the field of precise software analysis. While many things that we encounter in papers we read will be unclear at first sight, this does not suggest that you went to the dentist when this was covered in one of your UG classes; it most likely was not. Instead, in research we often have to practice "abstract reading", or "reading with holes". The discussions we will have on the papers will try to fill these holes. Be brave, and be flexible.

Course Staff

Instructor: Thomas Wahl Thomas Wahl

Course Topics

This course is shaped by the papers we read, discuss, and evaluate. While the selection of papers depends on your preferences, I roughly have the following topics in mind (and do not worry if these keywords don't mean much to you at this point). You can see the full list of papers currently under consideration here. The references below refer to that full list of papers.
  1. Basic motivation for precise, automated software analysis [1,2]
  2. Semantic foundations [3,4,15]
  3. Abstraction in program analysis [5,6,7]
  4. Infinite-state models [8]
  5. Bounded-path model checking [9]
  6. Software-specific techniques [10,11]
  7. Program Synthesis [12]
  8. Termination Analysis [13]
  9. (Old) News for Software Engineers [14]
(This list is not designed such that each item represents one class session. It is just a topics list.)

The following list contains papers that we have not discussed in class and that are therefore candidates for student presentations. As time goes on, this list may grow, but never shrink, so picking a paper from it is safe: [3,4,5,7,10,14].

Course Components and Course Credit

The course grade will consist of three components:
  1. Paper discussions (first half of the course): The week prior to each class session, the instructor will assign 1-2 papers to study. Before class, each student will turn in a 1-2 page summary and evaluation of the paper, in the style of a mini-review. (We will discuss how to write such evaluations; a template is provided here. The template comes in the LaTeX type-setting language, which is the standard in computer science research for document preparation. So, as a by-product, you will learn how to type-set simple documents in LaTeX. Here is the pdf rendering of the latex template.)

    During class, we will discuss the paper. The instructor will give an intro into the topic of the paper, provide background, guide the discussion, etc.

    Credit: 50% of your course grade.

  2. Paper presentations (second half of the course): We will continue to study, discuss and evaluate papers, with the following differences: (i) each class session will have a designated discussion leader (that will be a student, not the instructor), (ii) the lead gives a 30min-or-so slide presentation on the paper, (iii) the lead and the instructor together guide the discussion. The paper to be discussed will not be assigned by the instructor, but agreed upon between the lead and the instructor. Slides must be sent to the instructor 3 days before the presentation for review. All students, with the exception of the discussion lead, continue to turn in their short paper evaluations.

    Credit: 30% of your course grade (determined both by the slide set and by the presentation).

  3. Class participation (the entire course): the usual. This is a course where non-participation makes no sense. It is not a lecture course. You want to find out whether research is for you, so find out, actively. Research is not about sitting and listening, but about investigating, sharing, debating, engaging, claiming, proving, refuting, measuring, presenting, defending, getting excited and, sometimes, being disappointed. We will practice most of these activities in the course (not the last one). Almost all of them require participation.

    Credit: 20% of your course grade.


I knew there was something I was about to forget ...

The University is planning to partially reopen in the Fall and offer a hybrid learning model, involving both on-the-ground instruction, and remote learning. (See here for the latest.) Our class is expected to be small, so we hope that, most of the time, we can physically meet, with distance, and have lively discussions. We will decide this together as we go, and depending on your circumstances. Synchronous virtual attendance will be supported; nobody will be forced to be around in person.