/Verif

Abstract Interpretation Tool

Primary LanguageOCaml

Verification Tool

Implement a program verification tool.

Language description

The input language is a subset of C/C++. Supported types are int, float, and bool. Supported instructions are:

  • while loops
  • conditionals
  • variable assignments
  • break / continue statements.

Analysis

Implemented verification methods:

  • Basic analysis with invariant induction through widening and narrowing.