Skip to content

Latest commit

 

History

History
119 lines (82 loc) · 3.42 KB

TODO.md

File metadata and controls

119 lines (82 loc) · 3.42 KB
Raw

TO DO's:

27/03~10/04:

  • Install Frama-C

    • Installation tutorial of the program completed!

  • Create a tutorial on how to use https://frama-c.com/fc-plugins/slicing.html

    • Learn how to use the tool
    • Perform tests

  • Read Chapter 2 of the Thesis on program slicing

    • 1/3
    • 2/3
    • 3/3

10/04~17/04:

  • Present an example with slides of what program slicing is and how to execute it using Frama-C via command line.

    • (EXTRA!) present an example of program slicing with frama-c GUI

  • Present an example with slides of what program slicing is and how to execute it WITHOUT USING SOFTWARE, for function and instruction as a cutting criterion.

  • (EXTRA!) add pt-br support to the repository.

03/05~10/05:

  • complete the documentation for -slice-assert, -slice-pragma

    • (EXTRA!) enhance the documentation for types of slices in frama-c
    • (EXTRA!) enhance the documentation for the definition of slices

  • study more about -slice-assert, -slice-pragma, -slice-return, -slice-calls

    • 1/2 slice-assert
    • 2/2 slice-pragma
    • 3/4 slice-return
    • 4/4 slice-calls019980

  • 1 example with various criterions focusing in a assert(0) <- this is expected to be an error

  • test the output of frama-c combined with esbmc.org

    • 1/5
    • 2/5
    • 3/5
    • 4/5
    • 5/5

  • Refactor all the repository, adding the new tools to the README

    • Refactor documentation of frama-c

    • Create documentation for esbmc

      • 1/4 what is it?
      • 2/4 installation
      • 3/4 what it can do?
      • 4/4 Examples of use

22/05~29/05

  • Selecionar 5 programas de https://sv-comp.sosy-lab.org/2023/benchmarks.php com LOOPs

  • Testar com várias opções do FRAMA-C

    • 1/15 [loop_array1-1.c]
    • 2/15 [loop_array1-2.c]
    • 3/15 [loop_array2-2.c]
    • 4/15 [loop_array3.c]
    • 5/15 [loop_diamond1-1.c]
    • 6/15 [loop_diamond2-2.c]
    • 7/15 [loop_functions1-1.c]
    • 8/15 [loop_functions1-2.c]
    • 9/15 [loop_multivar1-1.c]
    • 10/15 [loop_multivar1-2.c]
    • 11/15 [loop_underapprox1-1.c]
    • 12/15 [loop_underapprox1-2.c]
    • 13/15 [loop_underapprox2-1.c]
    • 14/15 [loop_nested1-1.c]
    • 15/15 [loop_overflow1-1.c]

  • Slice por localização no código

  • Um exemplo de uso com ESBMC

  • (EXTRA!) complete the udemy course:Functional Verification - a holistic view

  • (EXTRA!) complete the udemy course: ROS for Beginners II

  • (EXTRA!) study all the 3 slide presentations in ESBMC documentation website:

    • 1/3
    • 2/3
    • 3/3

31/05/23 ~ 31/07/23

  • Definir as opções do FRAMA-C para efetuar o slice nos arquivos em C focando __VERIFIER_ERROR() OU REACH_ERROR()

    • Verificar para cada programa se ele é um código funcional, i.e., aceito pelo ESBMC (é sim)
    • Passar cada código pelo ESBMC, e tabelar os resultados incluindo o tempo
    • Análise comparativa usando o ESBMC sem efetuar o slice com o Frama-C, i.e., os códigos originais

  • Testar a ferramenta map2check

  • (EXTRA!) Realizar testes no cruise_control

  • opção do ESBMC para usar k-induction em paralelo

  • Escrever uma página sobre o FRAMA-C

  • [/] Escrever o relatório final, deadline 15 agosto.

to go back to the previous page: Click me!