Formal Software Verification

Assessment Method

Note test will take place on Monday June 20, at 15:00, in room 0.02

• Presentation on a theme to be assigned
• Individual test (last year's test here)

Slides

• Introductory Slides
• Slides on Operational Semantics
• Hoare Logic
• Verification Conditions
• Safety Verification with Frama-C
• Functional Verification with Frama-C
• Formal Logic and Deduction Systems
• Propositional Logic
• First-order Logic
• Beyond First-order Logic

Text Book

• Rigorous Software Development: an Introduction to Program Verification

Reading Material

• Paper Archive (for student presentations)
• Pitts A. M. Lecture Notes on Semantics of Programming Languages. Univ Cambridge, 1997-2002 (available online aqui)
• Verification Conditions for Source-level Imperative Programs (paper)

Code

• partition_init.c
• isort_init.c

Student Presentations

• Separation Logic
• Software Model Checking
• Static Analysis
• Testing
• Symbolic Execution

-- JorgeSousaPinto - 17 Mar 2011