Variants of the following course were offered at the CS Department of National University of Singapore for 3 years from 2003-05.
|
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 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 http://www.cs.technion.ac.il/users/orna/tools.ps 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 http://www-2.cs.cmu.edu/~modelcheck/ed-papers/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, 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.
|
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 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
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=MSR-TR-2001-10
|
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=MSR-TR-2002-09
|
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 E-reserves (please download the file named
Program Verification).
Additional Readings: http://www.cl.cam.ac.uk/Teaching/mjcg/Lectures/SpecVer1/Notes03/Notes.pdf 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 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 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 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/renieris-ase2003.pdf
|
ResearchTrends.pdf | |
| Week 13 | Lesson 13: Project
Presentations by Students
|
|||