Subject: Programs Verification	Code: MI018	

Semester	 Hours: C+S+L	Type	 Section	
6	2+1+0	optional	Computer Science	
6	2+1+0	optional	Mathematics-Computer Science	

Teaching Staff in Charge	Prof. FRENTIU Militon, Ph.D., mfrentiu@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 vverification 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.

9. Consequences on programming activity. Programming rules	
Selective 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. MANNA, Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974.
9. M.Frentiu, H.F.Pop, Fundamentals of Programming, Babes-Bolyai Press, 200	
Assessment	Each student must read a published research paper and present it at a seminary. He will obtain a mark for the presentation given to the seminary, for the way he expressed the ideas, and for his activityy in the seminaries (mark R). The activity ends with a written examination (mark E).  The final mark is the average of R and E, i.e. F=(R+E)/