Formal Software Verification

Who is the material made for?

This course is aimed at software developers, software architects, technology/innovation officers with development experience, and students with some programming experience.

The practical parts of this module assume a basic familiarity with (imperative) programming and with discrete mathematics (a working understanding of sets and first order logic).

Introduction

Formal Software Verification are a host of methodologies and tools that can help in the design, development, and maintenance of correct and robust computer programs.

This approach relies on automatic procedures for verifying that software behaves as expected.

7

These procedures are rooted in mathematics and techniques that support rigorous reasoning about properties of complex software.

There are several techniques that fall under the umbrella of formal software verificationproviding a spectrum with different levels of strength, precision, learning curve, and costs.

While the more powerful techniques require extensive training and a solid background in mathematics and computer science, there are many industry–level tools that require basic familiarity with software development and that can be readily adopted into existing processes: experience reports from across industry show that software engineers at all levels can learn verification from scratch and get useful results in few weeks.

This module aims to provide a high–level introduction to formal software specification and verification, including case studies and experience reports from industry. The fundamentals of this approach are illustrated through a series of examples and exercises using industry–level tools for formal software specification like TLA+ and its toolbox for model–checking and machine–checked proofs.