The latest offering of the module was in the Academic Year 201011.
Assessment: Final 50%, Midterm 20%, Project 30% (Effort 10%, Innovation: 8%, Report writing: 7%, Presentation: 5%).
DATES 
Lecture Summary 
Readings 
Resources 
Week1 
Introduction to the
module and discussion on Software testing will take place. Software
testing is the mostly widely used validation method and we will start our
discussions with testing. 
For a recent work on symbolic execution based testing, see  Intro.pdf 
Week 2  This lecture will focus on software debugging. Lightweight methods like program slicing and fault localization will be discussed briefly. Symbolic execution based methods for debugging will be discussed towards the later parts of the lecture.

Relevant chapters of "Why Programs Fail" by Andreas Zeller. In addition: You may read Dynamic Slicing & Relevant Slicing http://www.comp.nus.edu.sg/~abhik/pdf/toplas07.pdf Hierarchical Dynamic Slicing http://www.comp.nus.edu.sg/~abhik/pdf/issta07.pdf Software Fault Localization http://www.comp.nus.edu.sg/~abhik/pdf/cc06.pdf 
Debug1.pdf 
Week3 
We will finish the discussion on fault
localization (remaining from previous lecture on debugging) Continuation of the lecture on symbolic execution based software debugging. 
Yesterday my program worked. Today it does not. Why? Andreas Zeller, [ESEC‐FSE 1999].http://www.infosun.fim.uni‐passau.de/st/papers/tr‐99‐01/esec99‐talk.pdf DARWIN: An Approach for Debugging Evolving Programs Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, Kapil Vaswani, ESEC‐FSE 2009. http://www.comp.nus.edu.sg/~abhik/pdf/fse09.pdf 
Debug2.pdf 
Week 4 
Discussion on
compulsory term project (1 hour) We will discuss program properties and temporal logics. Both linear and branching time logics will be discussed. We will also try to make time for discussing their fixed point characterizations. (1 hour) 
This is the challenge problem we will tackle as the term project in this
module. Every student group will solve the same problem. http://sqrl.mcmaster.ca/pacemaker.htm
The weblink for the
challenge problem we tackle as the course project appears in the module
outline. The project will involve modeling the problem in SPIN model checker
and performing verification. Every group will have to do this (no
other techniques/ tools can be used)  so that the outputs from
the different groups can be compared in an objective fashion for fair
assessment. This is only the first step and everyone must complete this step
to get any credit in the project. A better project will also use the SPIN
model a guidance to generate C code. SPIN's language is quite close to C 
so this should be possible. You will also then be able to argue how/why you
could use the SPIN model as guidance and the links between requirements,
model and code. Finally, an excellent project will also have one group
member writing the code without going through modeling and the two codes
will be compared to clarify coding errors or errors in understanding the
requirements. 

Week 5 
Finish discussion on program properties
and temporal logics. Both linear and branching time logics will be
discussed. We also discussed their recursive characterizations.

"Model Checking" by Clarke, Grumberg and Peled, Chapter 3 provides introduction to linear and branching time logics. "Logic in Computer Science" by Huth and Ryan, Chapter 3.9 provides treatment of fixed point characaterizations of CTL properties. 
Temporal Logics 
Week 6 
SPIN as a
modeling and validation tool will be discussed in this lecture. This will
also expose the students to the model checking procedure inside SPIN. The
model checker in SPIN checks linear time temporal logics (LTL). A generic
verification method for LTL will be discussed

Readings: The Model Checker SPIN, Gerard Holzmann, IEEE Transactions on Software Engineering 97, see http://spinroot.com/gerard/pdf/ieee97.pdf Basic SPIN manual at http://spinroot.com/spin/Man/Manual.html Addtional Readings: You may also want to browse through the book "Design and Validation of Computer Protocols" by Gerard Holzmann. Some details about the verification algorithm of SPIN are available at http://spinroot.com/gerard/pdf/marktoberdorf.pdf The second section of these lecture notes is particularly relevant to the course material.

SPIN.pdf 
Mid Semester Break  
Week 7  Midterm
Examination (first hour), followed
by discussion on modeling/validation issues in the term project on pacemaker
controller.

   
Week 8  Lesson 8:
CTL model checking algorithm Initiate discussion on software abstractions (in particular predicate abstraction) to be completed in the next lecture.

"Model Checking" by Clarke, Grumberg and Peled, Chapter 4. 
CTLMC.pdf 
Week 9  Lesson 9:
Predicate Abstraction  Generating Finite state Models This lesson will
focus on generating a transition system like model from a program written in
a realistic programming language like C. The transition system like model is
amenable for verification.

Reading: Automatic Predicate
Abstraction of C Programs, Thomas Ball, Rupak Majumder, Todd Millstein and
Sriram Rajamani, PLDI 2001, see
http://www.cs.ucla.edu/~rupak/Papers/automatic_abstraction_of_c_programs.ps Additional Reading: If you get time, you can also take a look at the article "Polymorphic Predicate Abstraction" by the same authors at http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSRTR200110

ModelGen.pdf 
Week 10  Lesson 11: Abstraction
Refinement: We discuss how to iteratively arrive at the "right" software
abstraction.


AbstRefine.pdf 
Week 11  Lesson 11: PVS theorem
prover: This class will give the students a feel about the issues in
using a proof assistant for program verification.

Reading: See the documentation
at
http://pvs.csl.sri.com/documentation.shtml To use the prover, see the
Prover Guide at the PVS website (appears under Instructional
Resources). Sections 4 and 5 of the guide (on proof rules and strategies)
are particularly relevant. The System Guide contains some instructions about
getting started. Additional Reading: (optional) Here is an interesting comparison of two wellknown theorem provers PVS and HOL by Mike Gordon. See http://www.cl.cam.ac.uk/users/mjcg/PVS.html


Week 12 
Lesson 12: Review of lecture material. Many sample
questions will be discussed as an online session in this lecture.

All material covered in the module. 
Past final  1 
Week 13 
Lesson 13: Project
Presentations by Students.

   