Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Informatică
Programul de studii: Informatică - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MID0010	Software Systems Verification and Validation	

Semester	Hours: C+S+L+P	Category	Status	
6	2+1+1+0	speciality	compulsory	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
VESCAN Andreea		Asist.	Programming  Languages and Methods	*			

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
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.	

IV. Course contents
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. 

V. Bibliography
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 	

VI. Thematic of didactic activities per weeks

VII. Didactic methods used

VIII. 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/	

IX. Additional references

	Dean,							Chair head,

	Date,							Course responsible,
								Asist. VESCAN Andreea,