Map2Check – An Approach to Verifying Programs with Loops Using Program Slicing.

Oriented by Professor Dr. Herbert Rocha

Versão Pt-Br!

All the data collected here is available in more details in

• the Master Thesis of Marek Chalupa: Click here to see it!.
• The user-manual from Frama-c platform: Frama-c general User Manual(EN)!
• the slicing manual: Frama-c SLICING Manual(FR)
• you can also check the oficial website of the platform: Here!
• the ESBMC website is: here!
• https://link.springer.com/chapter/10.1007/978-3-030-17502-3_15

Objective of the project

• Acquire knowledge of program slicing, verification and validation of software through the various tools available in the market;
• test the various tools available in different scenarios;
• verify if Map2Check and others tools are capable of generating readable code results around the boundaries arrays and loop functions;
• contribute to science with this research project;

TO DO's of the project

Click here to see them.

PROGRAM VERIFICATION AND PROGRAM SLICING DEFINITIONS

Click here to see its documentation

PROGRAM VERIFICATION TOOLS:

• FRAMA-C Tool

  • Click here to see its documentation

• ESBMC Tool

  • Click here to see its documentation

• MAP2CHECK Tool

  • Click here to see its documentation

TESTS

We are going to use the tests in the folder: Tests

Tests with loops: Click me!

Complex frama-c tests: Click me!