Formal approaches

About this repository

This reposirtory contains an end-of-semester project in formal approach.
The aim is to prove mathematically the correct functioning of a bubble sorting system.

Prerequisite

• Install GNU compiler collection
  
• Install frama-c
  

Installation

• First clone this project

git clone https://github.com/PierreVerbe/Formal-Approaches

• Verify the installation of frama-c

frama-c -help

Launching the analysis

• Launch frama-c

frama-c -wp src/sort_1.c

• Launch frama-c graphical user interface

frama-c-gui -wp src/sort_1.c