guilhermebn198/program-slicing_pic

exploring program slicing and documenting my discoveries

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!

program-slicing_pic's Issues

creating a tutorial for frama-c CLI of slicing code

Creating a tutorial guide on how to use basic instructions on frama-c

Study ESBMC

Figure a way of presenting slicing code WITHOUT tools in a way it may be good to see in github

translation of all the documentos to pt-br

More tests

What did you saw that you'd like to change?
MORE TESTS