HECS-1

Analysis and verification of sequential programs

Lecturers

Contents

The objective of this course is to expose students to the major issues and solutions for the validation of sequential programs. The focus is on the formalization of expected properties and on their verification by deductive and algorithmic methods.

This course is divided into two complementary parts. Part 2 is also offered to M2 students of the ORCO master in Grenoble.

Part 1: Verification of sequential programs (course ref. WMM9MO45)

Program verification consists in proving properties that are true of all executions of the program, regardless of the input. For instance, one may wish to prove that the program may never encounter undefined behaviors or assertion violations, or that its output always satisfies some relationship with its input.

In general, one proves that no program execution encounters some undesirable configuration by exhibiting some property, known as inductive invariant, that holds by induction over the number of steps of the execution and that excludes the undesirable configuration. The difficulty is to find such an inductive invariant. This is the hard problem at the heart of program verification.

Topics discussed in the course include:

  • Reasoning by induction – Inductive invariants
  • Abstract interpretation
  • Program proof methods
  • Termination arguments
  • Verification for real languages: C, Java, etc.

Part 2: SAT/SMT solving (course ref. WMM9MO46)

The SAT problem (checking whether a formula built from AND, OR, and Boolean variables has a solution) is the canonical NP-complete problem. It is of high industrial importance in itself in hardware verification

Its combination with arithmetic and other form of reasoning, known as Satisfiability Modulo Theory, applies to many areas: a problem is specified as a formula involving AND, OR, arithmetic operations and comparisons over reals, integers, Boolean variables etc. and the solver says whether it has a solution and if so gives a solution.

Optimization Modulo Theory extends this paradigm to finding a solution that is optimal with respect to some criterion; e.g. if the formula defines scheduling constraints, one may compute an optimal schedule.

Topics discussed in the course include:

  • Boolean satisfiability checking: DPLL, CDCL
  • Satisfiability modulo theories: DPLL(T)
  • Optimization

Credits

3 ECTS for each part –  6 ECTS for the whole HECS “core” course, which comprises both parts.

Comments are closed.