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. Static program analysis.
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, practical projects.
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
- - -
