|
Course unit
SOFTWARE VERIFICATION
SCP6076339, A.A. 2019/20
Information concerning the students who enrolled in A.Y. 2019/20
ECTS: details
Type |
Scientific-Disciplinary Sector |
Credits allocated |
Core courses |
INF/01 |
Computer Science |
6.0 |
Course unit organization
Period |
Annual |
Year |
1st Year |
Teaching method |
frontal |
Type of hours |
Credits |
Teaching hours |
Hours of Individual study |
Shifts |
Lecture |
6.0 |
48 |
102.0 |
No turn |
Examination board
Board |
From |
To |
Members of the board |
3 a.a. 2018/2019 |
01/10/2018 |
28/02/2020 |
RANZATO
FRANCESCO
(Presidente)
FILE'
GILBERTO
(Membro Effettivo)
CRAFA
SILVIA
(Supplente)
GAGGI
OMBRETTA
(Supplente)
SPERDUTI
ALESSANDRO
(Supplente)
|
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 formal semantics of programming languages and formal methods for static program analysis and verification. |
Examination methods:
|
Oral examination and/or software project, possibly split into distinct parts. |
Assessment criteria:
|
The oral examination focuses on a variety of exercises that the student must solve independently as a take-home exam. The software project focuses on some program verification tools. |
Course unit contents:
|
- Program semantics: This is a model of the dynamic behaviour of programs (in particular the input/output behaviour) by means of order and fixed point theory. (cf. https://en.wikipedia.org/wiki/Semantics_(computer_science) )
- Static program analysis and verification by abstract interpretation: Abstract interpretation is a well-known technique for approximating the semantics of programs that allows to specify how to statically deduce program properties and to prove their correctness. (cf. https://en.wikipedia.org/wiki/Abstract_interpretation )
- 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 (such as gcc and javac) when optimizing a program. (cf. https://en.wikipedia.org/wiki/Data-flow_analysis )
- Software verification tools: e.g., Clousot (Microsoft, USA), Interproc (INRIA, France), Jandom (Univ. Pescara, Italy) (cf. https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis ) |
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 and/or a lab project of software verification. The course will include invited lectures by guest researchers on advanced topics in software verification. |
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
-
Antoine Minè, Tutorial on static inference of numeric invariants by abstract interpretation. --: Now, The Essence of Knowledge, 2017. Journal: Foundations and Trends in Programming Languages
|
Innovative teaching methods: Teaching and learning strategies
- Lecturing
- Laboratory
- Problem based learning
- Problem solving
- Loading of files and pages (web pages, Moodle, ...)
Innovative teaching methods: Software or applications used
- Static program analysis tools
Sustainable Development Goals (SDGs)
|
|