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