CS 6535: Engineering Reliable Software

Spring 2014



The story. Software bugs have been compared to death and taxes: they seem unavoidable. While some people contest that statement, much of the software development cycle today is spent on finding (and getting rid of) bugs in programs in large projects sometimes more than 50% of the time. Research and industry have come up with a wild variety of techniques to help engineers identify flaws in their software. Every programmer in industry must be aware of, and be able to use, at least some of these techniques in his or her career.

The course. In this course you will learn about a broad set of software reliability methods used in industry, ranging from human-centered code analysis methods, to systematic program testing, and high-precision formal software analysis approaches. As a side effect, you will also become a better programmer: chances are that programming bugs you discover in exercises in this course result from mistakes you will never make in the future to begin with.

Software bug

Synopsis


Course topics

  1. Formal property specification: how to state precisely what your program is (not) supposed to do, using property specification languages. Formal property specifications serve two purposes: (i) they force you to be precise about the intended purpose and properties of the program, and (ii) they allow automated techniques to test or otherwise analyze your program as to whether it meets those properties.

  2. Trial-and-error approaches to software reliability: Program testing is the most widely used form of vetting a program's reliability. Historically ad-hoc, large-scale program testing today is a very systematic activity. We will study it

  3. Symbolic code analysis: treating programs as logical formulas. This powerful paradigm encodes a program's execution as a set of constraints over the program variables at any point in time. Such an encoding gives you access to efficient constraint solver technology and is extremely instrumental in various software reliability techniques, from test case generation to formal program verification.

  4. Formal approaches to software reliability: such approaches emphasize the fact that program source code has (mostly) well-defined semantics and can thus be treated as a mathematical object, i.e., it can be analyzed with mathematical and logical techniques. We will study one such technique in greater detail: model checking, a method to systematically search programs for bugs, in a way that can either expose them, or in fact guarantee their absence.

  5. Other techniques: (if time permits) code monitoring and runtime analysis; theorem proving
We will study these topics hands-on, using tools and languages that you have already seen in your prior CS education, and will likely see in your professional career as a software programmer. Examples include ScalaTest, the Java Pathfinder, the KLEE symbolic execution engine, the Dracula/ACL2s programming environment, the CBMC model checker, and many more.

Methodology

Class time will be spent on highly-interactive lectures, discussions, practical exercises, and presentations by students. Outside class, there will be practical homework exercises to bring across the techniques, and a few slightly larger projects that go deeper into each particular technique. Projects can be done in groups of some non-zero size to be determined. Alternatively, I will give each student the option to conduct one comprehensive course project that encompasses several aspects of the course. Comprehensive projects are subject to approval by the instructor.

Prerequisites

I. Formal prerequisites: The course is intended mainly for Master-level students, but will be useful also for some undergraduate students, and for some Ph.D. students. Details:
  1. If you are an MS student, CS 5010 "Programming Design Principles" (aka "Bootcamp") with a minimum grade of C- is a requirement; if you lack it, come and talk to the instructor.
    CS 6535 is not about program design, but about program analysis (in the broadest sense of the word); we anticipate minor overlap with the Bootcamp course.

  2. If you are an undergraduate student, you should be a Junior or Senior, with a GPA of at least 3.25. You will be able to benefit from this course if you have had exposure to diverse programming courses in different flavors of languages; this will generally be the case only for junior/senior undergraduates. Examples of supporting courses you might have taken include the Fundies courses (CS25XX), Programming Languages (CS4400), and Software Development (CS4500). As listed below, the course assumes reasonable proficiency in programming techniques. If you feel you have that, this course is for you.

  3. If you are a Ph.D. student, you can benefit from this course by getting a soft introduction to program reliability. I invite you to talk to me to see whether the course is for you.

II. Content prerequisites: (listed roughly in order of decreasing significance) You should also not be afraid of basic (e.g. propositional) logic, and of basic algorithmic concepts such as graph search.

Course components and grading

Your final grade will depend on the following contributions to the class:

Textbooks (tentative)

Note: do not buy any of these books just yet (unless you really want to); we will discuss on the first day of class.


These books are available used for little money, and as e-books.