– 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.