Academic Year 2022-2023



Marina Lenisa
Unit Credits
Teaching Period
Second Period
Course Type
Prerequisites. Programming Languages, Logics
Teaching Methods. Lectures on theory ed exercises; assignment of individual exercises.
Verification of Learning. Written exam; optional oral exam.
In the course on Formal Methods mathematical techniques for the formal verification of programs are presented. In particular, the Hoare logic, based on invariants is illustrated for the formal verification of correctness and termination of various classical sequential algorithms. Issues such as absence of deadlock and fairness are formally discussed for a number of paradigmatic problems in concurrency theory, like producer-consumer and data transmission.
– Introduction to the formal verification of program correctness.

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

Apt K., de Boer F., Olderog E-R., “Verification of Sequential and Concurrent Programs”, Springer, 3rd edition, 2009.