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

SYLLABUS

General data
Code	Subject	
MID0010	Software Systems Verification and Validation	

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

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
FRENTIU Militon	Ph.D.	Prof.	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 vverification 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 program correctness. 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.	 Comparing the verification methods (2 lectures) 
- correctness-inspection-testing-symbolic execution 
- Cleanroom. Program Quality 
- 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. MANNA, Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974.

VI. Tematica activităţilor didactice pe săptămâni
C1 (+S1) Program Specification. The concept of program correctness. Examples.
C2 (+S2) Floyd method for prooving correctness 
C3 (+S3)  Hoare axiomatisation method 
C4 (+S4) The Evolution of the concept of program correctness. The Contribution of Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan.
C5 (+S5)  Dijkstra: the weakest precondition.  Stepwise refinement from specifications 
C6 (+S6) Verification and validation: concepts, methods, relations
C7 (+S7) Program inspection
C8 (+S8) Program documentation
C9 (+S9) Symbolic execution
C10 (+S10). Program testing:  concepts, types of testing, testing criteria.
C11 (+S11) Unit testing: blackbox and whitebox testing
C12 (+S12)  Integration testing, system testing, regression testing, acceptance testing 
 C13 (+S13) Model checking
C14 (+S14). Comparing the verification methods:  correctness-inspection-testing-symbolic execution. Cleanroom. Program Quality. The consequences of the theory of program correctness on programming. Programming style. 

VII. Didactic methods used
Expositions: class lectures, introductive lectures, dialog-based lectures, lectures with demonstrations, descriptions and explanations.
   Conversations: dialog, debate, introductive conversations,   conversations to systematize and synthesize knowledge.
   Discovery: inductive and deductive discovery, directed and independent rediscovery, creative discovery, experimental discovery.
   Use of problems: use of problem questions, problems and problem situations.
   Other methods: exercises,  individual and homework study, case study, brainstorming.

VIII. Assessment
The activity in the seminaries is appreciated with a mark S and at laboratories with L. The activity ends with a written examination (mark E). The final mark is the average of R and E, i.e. F=(S+L+2E)/4

IX. Additional references
Papers from Internet	

	Dean 							Head of chair,

	Data,							Titular curs,
	24.04.2007						Prof. Dr. FRENTIU Militon