Automated Software Validation

This an old offering, for the latest offering click here

Variants of the following course were offered at the CS Department of National University of Singapore for 3 years from 2003-05.



Lecture  Summary 



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



 Reading:  Trends in Software Verification by Gerard Holzmann


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.



1. Chapter 3 and 4.1 of the book Model Checking by Clarke, Grumberg and Peled. This material has been placed under E-reserves.

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 fixed-point characterizations of CTL properties.

3. Section 4 of the following survey article Section 5 of this article also contains discussion on fixed-point 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


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.


Week 4 Lesson 4:  Recovering slack from past lectures (The material on temporal logic, fixed-point 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 well-established 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.



The Model Checker SPIN, Gerard Holzmann, IEEE Transactions on Software Engineering 97, see

Basic SPIN manual at

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 The second section of these lecture notes is particularly relevant to the course material.


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 user-guided simulation. The Linear-time 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

Additional Reading: If you get time, you can also take a look at the article "Polymorphic Predicate Abstraction" by the same authors at


Week 9 Lesson 9:  Abstraction Refinement



Reading:  Generating Abstract Explanations of Spurious Counterexamples in C Programs by Ball and Rajamani at


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 E-reserves (please download the file named Program Verification).

Additional Readings: The first 4-5 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


Week 11 Lesson 11: PVS theorem prover



Reading:  See the documentation at  To use the prover, see the Prover Guide at the PVS web-site (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 well-known theorem provers PVS and HOL by Mike Gordon. See



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).



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


Week 13 Lesson 13: Project Presentations by Students