CS 6535: Engineering Reliable Software
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.
- Course number: CS 6535
- Class times: Thursdays 6-9pm
- Class location: West Village H 164
- Instructor: Thomas
- Office hours: Wednesdays 12 noon - 2pm
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.
- 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.
- 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
- classified by test case selection: based on various
coverage metrics; manual vs. automatic test case generation
- classified by test organization: unit, integration, and
system testing; stress testing; regression testing; test
- 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.
- 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.
- Other techniques: (if time permits) code monitoring and
runtime analysis; theorem proving
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.
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:
- 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.
- 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.
- 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
You should also not be afraid of basic (e.g. propositional) logic,
and of basic algorithmic concepts such as graph search.
- programming: reasonable proficiency in at least one
main-stream functional or imperative programming language, such
as from the LISP family, Haskell, Java, or C++. This course is
not about programming techniques. It is about techniques for
finding bugs, assuming you have at least a basic understanding
of programming constructs, and of programming.
- program reading: ability to read and understand
programs written in main-stream functional or imperative
programming languages, such as those above, even if you have not
programmed in them. Much of the instruction will be done using
one of these languages (different languages in different phases
of the course).
Course components and
final grade will depend on the following contributions to the class:
- 10%: class participation.
This can take many forms: correct answers, incorrect answers,
good questions, volunteer presentations, suggestions for
improving the class, …
- 20%: homeworks.
Depending on class size, we may decide to do homeworks in
- 30%: midterm exam.
This will happen during class time, on a date we will determine
during the first session, so it is most desirable for you to be
present on the first day. It is also most desirable for you to
be present on the exam day and take the exam, as I will not
allow make-ups under any but earth-shattering circumstances.
- 40%: course projects. (either several medium-size
projects, or one comprehensive course project)
Depending on class size, we may decide to do projects in groups.
Completing projects may require a moderate write-up, and
will require a presentation, depending on the nature of
Note: do not buy
any of these books just yet (unless you really want to); we will
discuss on the first day of class.
- Introduction to Software Testing, by Paul Amman and
Jeff Offutt. Cambridge University Press. ISBN: 978-0-521-88038-1
- The Art of Software Testing, by Glenford J. Myers,
Corey Sandler, Tom Badgett. Wiley Publishers. ISBN-13:
- Logic in Computer Science, by Michael Huth and Mark
Ryan. Cambridge University Press. ISBN:
978-0-521-54310-1 (2nd edition, paperback)
These books are available used for little money, and as e-books.