– Syntax and operational semantics of deterministic programs.

– Hoare Logic system for correctness of deterministic programs.

– Formal verification of classical sequential algorithms. Partial correctness and termination.

– Completeness of Hoare Logic systems.

– Syntax and operational semantics of disjoint parallel programs.

– Disjoint parallelism and sequentiality.

– Verification of correctness of disjoint parallel programs.

– Verification of parallel programs with shared variables: partial correctness.

– Strong correctness of proof outline. Rule for parallelism and its incompleteness. Rule for auxiliary variables.

– Total correctness of parallel programs with shared variables.

– Parallel programs with shared variables. Non-compositional behaviour of components.

– Parallel programs with synchronisation: syntax and operational semantics.

– Verification of correctness of parallel programs with synchronisation: partial correctness, termination, deadlock absence.

– Verification of correctness of paradigmatic examples of parallel programs with synchronisation: producer and consumer, readers and writers, implementation and use of semaphores, etc.

– Non-deterministic programs: syntax, operational semantics, rules for verification of correctness.

– Usefulness of non-deterministic programs. Translation of parallel programs into non-deterministic programs.

– Introduction to distribute computing. Distribute programs: syntax, operational semantics.

– Paradigmatic examples: the transmission problem and its variants (with or without filtering of data, with or without acknowledgement messages, etc.),

– Translation of distributed programs into non-deterministic programs and relationships between the semantics.

– Verification: partial correctness, termination, deadlock absence.

– Fairness: study of correctness of parallel programs under hypothesis of fair scheduling. The presented methodology is based on the implementation of a fair scheduling inside the program itself. Such implementation is defined in a language extended with random assignment. The proof of termination requires the use of termination function defined on well-founded structures generalising natural numbers.