Babes-Bolyai University of Cluj-Napoca
Faculty of Mathematics and Computer Science
Study Cycle: Graduate

SUBJECT

Code
Subject
MID0010 Software Systems Verification and Validation
Section
Semester
Hours: C+S+L
Category
Type
Computer Science
6
2+1+1
speciality
compulsory
Information engineering
6
2+1+1
speciality
compulsory
Teaching Staff in Charge
Prof. FRENTIU Militon, Ph.D.,  mfrentiucs.ubbcluj.ro
Asist. VESCAN Andreea,  avescancs.ubbcluj.ro
Lect. SIMON Karoly, Ph.D.,  ksimoncs.ubbcluj.ro
Aims
To understand what a correct algorithm is. To gain knowledge of designing correct algorithms and proving their correctness hand- in-hand. To learn the methods of program verification and validation. To become used with building correct programs from specifications.
To acquire a modern programming style.
Content
I. The theory of program correctness (4 lectures)
- Program Specification
- Floyd method for prooving correctness
- Hoare axiomatisation method
- Dijkstra: the weakest precondition.
- Stepwise refinement from specifications
- The Evolution of the concept of programcorrectness. The Contribution of Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan

II. Verification and validation: (3 lectures)
- the concepts verification and validation;
- the verification methods;
- program inspection;
- symbolic execution;
- testing and debugging;
- documentation.
III. Program testing: (3 cursuri)
- the concept of Program testing;
- unit testing: testing criteria, blackbox and whitebox testing;
- types of testing: integration T., system T., regression T., acceptance T.
- testing automatizing
IV. Model checking (2 lectures)
V. Consequences of V&V on programming methodology (2 lectures)
- Cleanroom. SPI.
- The consequences of the theory of program correctness on programming. Programming style.

References
1. BALANESCU T., Corectitudinea programelor, Editura tehnica, Bucuresti 1995.
2. DIJKSTRA, E., A constructive approach to the problem of program correctness, BIT, 8(1968), pg.174-186.
3. DIJKSTRA, E., Guarded commands, nondeterminacy and formal derivation of programs, CACM, 18(1975), 8, pg.453-457.
4. DROMEY G., Program Derivation. The Development of Programs From Specifications, Addison Wesley Publishing Company, 1989.
5. FRENTIU, M., Verificarea corectitudinii programelor, Ed.Univ.$Petru-Maior$, 2001.
6. GRIES, D., The Science of Programming, Springer-Verlag, Berlin, 1981.
7. HOARE, C.A.R., An axiomatic basis for computer programming, CACM, 12(1969), pg.576-580, 583.
8. Morgan, C., Programing from Specifications, Prentice Hall, NewYork, 1990.
B. Internet
Assessment
The activity at seminaries, consisting from participation in solving the exercises and discussions, will be appreciatewd by a mark S. A second mark L will be given for the laboratories work. At the end a written examination will give a mark E. The final mark F is given by:
F=(A+L+2E)/4.
Details at: www.cs.ubbcluj.ro/~mfrentiu/Lectures/
Links: Syllabus for all subjects
Romanian version for this subject
Rtf format for this subject