Variants of the following course were offered at the CS Department of National University of Singapore for 3 years from 200305.
DATES 
Lecture Summary 
Readings 
Resources 

Week1  Lesson 1: Introduction,
Discussion of Course Outline and Term Projects


Intro.pdf  
Week 2  Lesson 2: Temporal
Logics This lesson will discuss specification languages for
describing properties of our transition system like models. The properties
capture ordering of events as the transition system evolves in its
execution.

Readings: 1. Chapter 3 and 4.1 of the book Model Checking by Clarke, Grumberg and Peled. This material has been placed under Ereserves. 2. Chapter 3 of Logic in Computer Science by Huth and Ryan, RBR in Science Library. In particular, see chapter 3.9 for discussion on fixedpoint characterizations of CTL properties. 3. Section 4 of the following survey article http://www.cs.technion.ac.il/users/orna/tools.ps Section 5 of this article also contains discussion on fixedpoint characterization of CTL properties. So, if you cannot access Chapter 3.9 of the Huth and Ryan book, you can read this portion as well. Additional Reading: You may be interested to read the original paper on Model Checking (appeared in 1986), see http://www2.cs.cmu.edu/~modelcheck/edpapers/AVoFSCSU.pdf

TL.pdf  
Week3  Lesson 3: Model Checking We will discuss a simple search algorithm to prove properties of transition system like models. The property specification language considered is Computation Tree Logic (CTL).  Readings: Same as last week.

MC.pdf  
Week 4  Lesson 4: Recovering slack from past lectures (The material on temporal logic, fixedpoint characterizations and model checking spills into three lectures instead of two).      
Week 5  Lesson 5: SPIN as a
modeling tool This lecture will try to get you familiar with a very
wellestablished verification tool called SPIN. It has its own modeling
language (called PROMELA) which captures some of the features of a
programming language; actually PROMELA is suitable for directly modeling
protocols. We will discuss PROMELA in this lecture.

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 (Call number TK 5105.5 Hol, RBR in Science Library) 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  
Week 6  Lesson 6: SPIN as a
validation tool We will continue with our discussion of the verification
tool SPIN. We will discuss its capabilities for model checking, random
simulation and userguided simulation. The Lineartime temporal logic (LTL)
model checking algorithm implemented in SPIN is discussed.

Readings: Last Week's
Readings. In addition, if you are interested to learn more about the LTL verification algorithm used by SPIN, you can refer to Chapter 8 of the following book. "The SPIN Model Checker: primer and reference manual" by G.J. Holzmann, Addison Wesley 2004, Call Number TA168 Hol 2004 , RBR in Science Library.

Same as Week 5  
Mid Semester Break  
Week 7  Midterm
Examination


Week 8  Lesson 8: 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 9  Lesson 9: Abstraction
Refinement

Reading: Generating Abstract
Explanations of Spurious Counterexamples in C Programs by Ball and Rajamani
at
http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSRTR200209

AbstRefine.pdf  
Week 10  Lesson 10: Hoare style
deductive verification

Reading: Chapter 4 of the book
Logic in Computer Science by Michael Huth and Mark Ryan. This
material has been placed in Ereserves (please download the file named
Program Verification).
Additional Readings: http://www.cl.cam.ac.uk/Teaching/mjcg/Lectures/SpecVer1/Notes03/Notes.pdf The first 45 chapters of this lecture notes can help boost our understanding of the topic. The original article by C.A.R. Hoare on this topic was called An axiomatic basis for computer programming. It appeared in Communications of the ACM, see http://portal.acm.org/citation.cfm?doid=363235.363259

Hoare.pdf  
Week 11  Lesson 11: PVS theorem
prover

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: Future Trends in
software validation In this lesson, I will give an summary of some
upcoming problems and trends in the field of software verification. We
will discuss whether you faced the manifestation of (some) of these problems
in your term projects. I will also discuss in some details some emerging
research on dynamic checking techniques for software debugging (detecting
presence of bugs) and fault localization (tracking down the bugs).

Readings 1. Dynamic Program Slicing , Agrawal and Horgan, PLDI 1990, Available from ACM Digital Library 2. Fault Localization With Nearest Neighbor Queries, ASE 2003, Reiss and Renieris, see http://www.cs.brown.edu/people/er/papers/renierisase2003.pdf

ResearchTrends.pdf  
Week 13  Lesson 13: Project
Presentations by Students
