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	
Mathematics-Computer Science - in Romanian	6	2+1+1	speciality	optional	
Information engineering	6	2+0+2		compulsory	

Teaching Staff in Charge	Prof. FRENTIU Militon, Ph.D., mfrentiu@cs.ubbcluj.ro
Lect. SIMON Karoly, Ph.D., ksimon@cs.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. 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. 

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.
B. Articole Internet	
Assessment	The activity at seminaries, consisting from participation in solving the exercises and a talk about a given paper will be appreciated by a mark, let denote it by A. At the end a wrutten examination will give a second mark, denoted by E. The final mark F is given by:
                                  F=(A+E)/2.
Detalii la: www.cs.ubbcluj.ro/~mfrentiu/Lectures/