Learning objectives
Introduce students to: the use of formal methods for the specification of the semantics of programming languages; the use of formal techniques for the verification of the behavior of a program with respect to a partial specification.
Prerequisites
Foundations of computer science.
Course unit content
Definition of operational and denotational semantics of simple imperative programming languages; formal reasoning about the behavior of simple programs; notion of behavioral equivalence of computer programs.
Full programme
Program syntax and semantics. Structural operational semantics, big-step and small-step. Induction principles and inductive definitions. Denotational semantics. Orderings, domains and fixed points. Axiomatic semantics. Verification of program correctness. Introduction to the static analysis of programs.
Bibliography
The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. Matthew Hennessy, Wiley, 1990. [http://www.cogs.susx.ac.uk/users/matthewh/semnotes.ps.gz]
La Semantica Formale dei Linguaggi di Programmazione. Glynn Winskel. MIT Press, 1993.
Teaching methods
Lectures and exercise sessions.
Assessment methods and criteria
Students will be evaluated by means of: home assignments to be handed in in one week time; realization of a final project; concluding oral examination.
Other information
- - -
