CS510 Software Engineering

Mathias Payer -- Spring semester 2015, 3 credit course


Course overview

Software engineering applies well-defined processes and principles to the design, development, and maintenance of software. Software engineering relies both on engineering and computer science components to build software systems. In this course students will study systematic and automatic techniques towards building software systems. Through this course, students are expected to deeply understand the discussed principles, be familiar with software development tools, and acquire experience in applying the discussed techniques.

Topics: program analysis, debugging, testing, model checking, verification


  1. Introduction (01/13/15)
  2. Program representations (01/15/15) [1]
  3. Dynamic program analysis
  1. Program Tracing (01/20/15) [2]
  2. Program Profiling (01/26/15) [3] [4]
  3. Slicing (02/03/15) [5]
  4. Delta debugging and statistical debugging (02/10/15) [6]
  1. Static program analysis [7]
  1. Data-Flow analysis (2/17/15)
  2. Propositional logic (2/24/15, 3/3/15) [8] (only chapter 1)
  3. SAT solving (3/12/15)
  4. Model checking C programs: CBMC-1, CBMC-2 (3/24/15, 3/26/15) [9]
  5. Model checking Java programs and predicate abstraction (3/31/15, 4/02/15) [10] [11]
  1. Symbolic execution (4/7/15) [12]
  2. Testing
  1. Testing basics (4/9/15)
  2. CUTE: concolic testing (4/14/15) [13]
  3. CHESS: concurrent testing (4/16/15, 4/21/15) [14]
  4. Protocol mining (4/23/15, 4/28/15) [15]
  5. Protocol checking


  1. Basic data structures (hw1 solution), due Feb-03.
  2. Dynamic and static analysis techniques (hw2 solution), due Feb-26.
  3. Propositional logic and SAT solving (hw3 solution), due Mar-26.
  4. Symbolic and concolic execution (hw4 solution), due Apr-28.


  1. Small project: using ASan to find memory errors in existing programs (slides, P1 description, due Feb-03 before class).
  2. Small project: using LLVM to construct call graph and memory allocation sites (P2 description, due Feb-26 before class).
  3. Small project: using Klee to find vulnerabilities (P3 description, due Mar-26 before class).
  4. Term project: data flow tracking as LLVM pass (P4 description, due Apr-30 before class).

Student presentations

The presentations count as one extra (bonus) homework, should take 15 minutes and will be held at the end of class. These presentations are an opportunity to cover up some missed points from any of the exercises or exams.

  1. 03/26 Java Path Finder: Nathan Burrow
  2. 03/31 Deviation Analysis through Model Checking: Santiago Velez Saffon
  3. 04/02 BLITZ: David Perry
  4. 04/07 Automatic Predicate Abstraction: Xuankang Lin
  5. 04/09 KLEE: Yunxiao Zou
  6. 04/14 HI-CFG: Kexin Pei
  7. 04/16 Concolic Testing: Joe Klemen
  8. 04/21 Concurrent Testing: David Wiszowaty
  9. 04/21 Automatic Generation and Clustering of Efficient Random Unit Tests: Daren Khaled Fadolalkarim
  10. 04/23 Automatic Test Factoring: Alejandro Guayaquil Sosa
  11. 04/23 Feedback-directed random test generation: Huyue Gu
  12. 04/28 Test Suite Reduction for Model Based Tests: Edgardo A. Barsallo Yi
  13. 04/28 Asserting and checking determinism for multithreaded programs: Victor O. Santos Uceta
  14. 04/30 BITA: Coverage-Guided, Automatic Testing of Actor Programs: Augustin Bazzani
  15. 04/30 Run-time efficient probabilistic model checking: Miguel Rivera Mediavilla


  1. for academic honesty refer to the Purdue integrity/code of conduct;
  2. except as by prior arrangement or notification by the professor of an extension before the deadline, missing or late work will be counted as a zero/fail.
  3. code, documentation, and reports must be submitted into GitHub and you must give the instructors access to the code (user ids 'gannimo' and 'scottcarr').

Course policies

This course will be run under the "reasonable person" policy wherein it is assumed that all students are reasonable adults that want to benefit the most of the course by attending the course regularly, completing the homework assignments and projects on time, asking questions during the course and if they run into problems, and checking back with the instructor and the TA regularly to ensure good progress.

A more verbose version of the policy is available on Spaf's page. CS-510 follows the policies listed on that page. If you have any question about the course policy, don't hesitate to ask the instructor or the TA.

As a short summary: (i) you are expected to attend all classes (modulo good reasons), (ii) you are supposed to hand in all work before the deadlines (there's a 10% point reduction per day for late hand-ins), (iii) if you need special treatment or have special circumstances, talk to the instructor or TA.

References and Reading Assignments

[1]Jeanne Ferrante and Karl J. Ottenstein and Joe D. Warren, The program dependence graph and its use in optimization, TOPLAS'87
[2]Xiangyu Zhang and Rajiv Gupta, Whole Execution Traces and Their Applications, MICRO'04 (focus on Section 4)
[3]Thomas Ball and James R. Larus, Efficient Path Profiling, MICRO'96
[4]Darko Marinov and Robert O'Callahan, Object Equality Profiling, OOPSLA'03
[5]Ben Xin and Xiangyu Zhang, Efficient online detection of dynamic control dependence
[6]Andreas Zeller and Ralf Hildebrandt, Simplifying and Isolating Failure-Inducing Input
[7]Al Bessey and Ken Block and Ben Chelf and Andy Chou and Bryan Fulton and Seth Hallem and Charles Henri-Gros and Asya Kamsky and Scott McPeak and Dawson Engler, A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World, CACM'10
[8]Michael Huth and Mark Ryan, Logic in Computer Science: modeling and reasoning about systems, Cambridge University Press, 2004 (available online).
[9]Edmund Clarke and Daniel Kroening and Karen Yorav, Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking, DAC'03
[10]Willem Visser and Klaus Havelund and Guillaume Brat and Seung Joon Park, Model Checking Programs, ASE'02
[11]Thomas Ball and Rupak Majumdar and Todd Millstein and Sriram K. Rajamani, Automatic Predicate Abstraction of C Programs, PLDI'01
[12]Cristian Cadar and Daniel Dunbar and Dawson Engler, KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, OSDI'08
[13]Koushik Sen and Darko Marinov and Gul Agha, CUTE: a concolic unit testing engine for C, FSE'05
[14]Madanlal Musuvathi and Shaz Qadeer and Thomas Ball and Gerard Basler and Piramanayagam Arumuga Nainar and Iulian Neamtiu, Finding and Reproducing Heisenbugs in Concurrent Programs, OSDI'08
[15]Michael Pradel and Thomas R. Gross, Automatic Generation of Object Usage Specifications from Large Method Traces, ASE'09