First cycle
degree courses
Second cycle
degree courses
Single cycle
degree courses
School of Science
Course unit
SCM0015974, A.A. 2015/16

Information concerning the students who enrolled in A.Y. 2015/16

Information on the course unit
Degree course Second cycle degree in
SC1176, Degree course structure A.Y. 2014/15, A.Y. 2015/16
bring this page
with you
Number of ECTS credits allocated 8.0
Type of assessment Mark
Website of the academic structure
Department of reference Department of Mathematics
Mandatory attendance No
Language of instruction English
Single Course unit The Course unit can be attended under the option Single Course unit attendance
Optional Course unit The Course unit can be chosen as Optional Course unit

Teacher in charge FRANCESCO RANZATO INF/01

ECTS: details
Type Scientific-Disciplinary Sector Credits allocated
Core courses INF/01 Computer Science 8.0

Course unit organization
Period First semester
Year 1st Year
Teaching method frontal

Type of hours Credits Teaching
Hours of
Individual study
Lecture 8.0 64 136.0 No turn

Start of activities 01/10/2015
End of activities 28/01/2016
Show course schedule 2019/20 Reg.2014 course timetable

Examination board
Board From To Members of the board
5 a.a. 2017/2018 01/10/2017 28/02/2019 RANZATO FRANCESCO (Presidente)
BALDAN PAOLO (Membro Effettivo)
FILE' GILBERTO (Membro Effettivo)

Prerequisites: Basic knowledge of programming languages. Formally prerequisite courses are not required.
Target skills and knowledge: This course aims to be an introduction to methodologies and tools used for designing the semantics, static analysis and automatic verification of the behavior of programs and, more generally, of software systems. In particular, the main topics will be operational and denotational semantics of programming languages and formal methods for static program analysis and verification.
Examination methods: Oral examination, typically divided into three distinct parts.
Assessment criteria: The oral examination focuses on a variety of exercises that the student must solve independently as a take-home exam.
Course unit contents: - Operational program semantics: This is a model of the operational behaviour of programs on an abstract execution machines by means of proof derivation systems.

- Denotational program semantics: This is a model of the input/output behaviour of programs by means of partial order and fixed point theory.

- Static program analysis by abstract interpretation: Abstract interpretation is a well-known technique for approximating the denotational semantics of programs that allows to specify how to statically deduce program properties and to prove their correctness.

- Dataflow program analysis: This is a technique for gathering information about the possible set of values calculated at various program points. A program's control flow graph is used to determine those parts of a program to which a particular value assigned to a variable might propagate. The information gathered is often used by compilers when optimizing a program.

- System verification by model checking: Model checking is a technique for automatically verifying some correctness properties of software systems, where correctness is specified by using temporal logics. The inventors of model checking were the recipients of prestigious 2007 Turing Award (widely recognized as the "Nobel Prize" of computer science).
Planned learning activities and teaching methods: The course consists of lectures and requires that the student solves independently as a take-home exam a number of exercises.
Additional notes about suggested reading: Slides used during lectures will be available.
Textbooks (and optional supplementary readings)
  • H. Riis Nielson, F. Nielson, Semantics with Applications: A Formal Introduction. --: Wiley, 1992. Electronic version freely available