| First cycle degree courses | Second cycle degree courses | Single cycle degree courses |
| School of Science | ||
| COMPUTER SCIENCE | ||
Course unit
SOFTWARE VERIFICATION
SCP6076339, A.A. 2019/20
Information concerning the students who enrolled in A.Y. 2019/20
SOFTWARE VERIFICATION
SCP6076339, A.A. 2019/20
Information concerning the students who enrolled in A.Y. 2019/20
Information on the course unit
| Degree course |
Second cycle degree in COMPUTER SCIENCE SC1176, Degree course structure A.Y. 2014/15, A.Y. 2019/20 |
 bring this page with you |
|---|---|---|
| Number of ECTS credits allocated | 6.0 | |
| Type of assessment | Mark | |
| Course unit English denomination | SOFTWARE VERIFICATION | |
| Website of the academic structure | http://informatica.scienze.unipd.it/2019/laurea_magistrale | |
| Department of reference | Department of Mathematics | |
| Mandatory attendance | No | |
| Language of instruction | Italian | |
| Branch | PADOVA | |
| 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 |
Lecturers
| Teacher in charge | FRANCESCO RANZATO | INF/01 |
|---|
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 |
| Start of activities | 30/09/2019 |
|---|---|
| End of activities | 20/06/2020 |
| Show course schedule | 2019/20 Reg.2014 course timetable |
Examination board
| Board | From | To | Members of the board |
|---|---|---|---|
| 4 a.a. 2019/2020 | 01/10/2019 | 28/02/2021 |
RANZATO
FRANCESCO
(Presidente)
BALDAN PAOLO (Membro Effettivo) CRAFA SILVIA (Supplente) FILE' GILBERTO (Supplente) GAGGI OMBRETTA (Supplente) SPERDUTI ALESSANDRO (Supplente) |
| 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) |
|
- Lecturing
- Laboratory
- Problem based learning
- Problem solving
- Loading of files and pages (web pages, Moodle, ...)
