"Babes-Bolyai" University of Cluj-Napoca
Faculty of Mathematics and Computer Science

Program verification
Code
Semes-
ter
Hours: C+S+L
Credits
Type
Section
MI018
6
2+1+0
5
optional
Informatică
MI018
6
2+1+0
4
optional
Matematică-Informatică
Teaching Staff in Charge
Prof. FRENTIU Militon, Ph.D.,  mfrentiucs.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.
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.
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 and for the way he expressed the ideas (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)/2