Verified Algorithms

The aim of this course is to learn how to write algorithms that satisfy precise specification and verify them using the computer

S2 3 ECTS 24h OPT EN Site web

Description

Verified algorithms are algorithms that come with a computer-checked guarantee that they perform what is specified. This course teaches how to obtain such algorithms using a proof assistant named Coq.

Verified algorithms are crucial for domains where the presence of bugs are inacceptable for society: computer security, financial transactions, transportation embedded software, computer infrastructure.

Outline

  • Programming with simple types and recursive data-types
  • Expressing requirements with logical formulas and advanced types
  • Tactic-based formal verification
  • Reasoning by induction on programs
  • Verified algorithms in data processing
  • Verified algorithms in number processing
  • Verified compilation

The various techniques used in this course will be illustrated during lab sessions using the Coq system (ACM software system award 2014). A downgraded version can be used for experimenting at this address.

References