Description

Most of the course is devoted to high-level semantic design and code-level properties. The emphasis is put on executable specifications and verification tools based on the following methods:

• Static analysis and type checking


• Design-by-contract and property-based testing

Static and dynamic verification in particular are compared in this course, with a focus on tools and prototype development:

• Preliminaries
  
  
  
  
  • Imperative programming and unit testing
  
  
  • Functional programming and logic
  
  
  
  


• Part I: static analysis
  
  
  
  • Specification: typing rules (deductive system)
  
  
  • Implementation: mode-based extraction of functional code
  
  
  
  


• Part II: dynamic verification
  
  
  
  • Specification: design-by-contract
  
  
  • Implementation: self-testing and property-based testing
  
  
  
  

Finalité

Students who take this course will gain an understanding of the concepts and theories of computer-aided formal specification and verification, and learn how to use and write formal verification tools.

Description des modalités d'évaluation

Attendance and participation in lessons (50%) and written final exam (50%).

Public

Computer Science or Computer/Electrical Engineering Bachelor.