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

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
N0
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

Calendar
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
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)

Syllabus
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)
Quality Education Industry, Innovation and Infrastructure