Introduction to program verification

Teacher
Francesco ranzato
Department of Mathematics
ranzato[at]math.unipd.it
INF/01

Aim
Computer programs may contain bugs, namely errors and flaws in programs that cause incorrect output or unintended behavior. This course aims to be a gentle introduction to methodologies and tools used for automatically and formally proving that computer programs do not contain bugs, a discipline known as program verification.

Syllabus
- Meaning of programs: Program semantics
- Program verification by sound static analysis
- Tools for program verification

Introductory reading
Wikipedia entry on formal software verification:
https://en.wikipedia.org/wiki/Formal_verification

Course material, enrollment and last minute notifications
Made available by the teacher at this Moodle address

Course requirements
None

Schedule
Canceled

Location
to be defined

<< Courses in 2019-2020