cod. 1000741

Academic year 2015/16
3° year of course - Second semester
Academic discipline
Informatica (INF/01)
Discipline informatiche
Type of training activity
56 hours
of face-to-face activities
6 credits
hub: PARMA
course unit
in - - -

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.


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.


The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. Matthew Hennessy, Wiley, 1990. []

La Semantica Formale dei Linguaggi di Programmazione. Glynn Winskel. MIT Press, 1993.

Teaching methods

Lectures and exercise sessions, practical projects.

Assessment methods and criteria

Written and oral examination.

Other information

- - -