Logo
1.0

About

  • An introduction to Formal Verification
  • What is FVM?

Getting started

  • Installation
  • Your first example

Concepts

  • Assert/assume/cover
  • Sequences and properties
  • Coverage metrics in formal verification
  • How to do specific things with PSL and the FVM

Examples

  • Repository of Examples

Public API

  • FvmFramework
  • Command-line options
  • drom2psl

Internal API

  • fvm
    • fvm package

Advanced

  • Techniques to reduce proof complexity
  • Future work: Guidelines on writing formal test plans
  • Future work: Guidelines on writing formal-friendly designs

Appendix

  • License
  • Acknowledgement
  • Publications
  • ChangeLog
fvm
  • fvm
  • View page source

fvm

Warning

Callables that are not documented in the Public API are not intented to be directly used and thus may change between minor versions.

  • fvm package
    • Subpackages
      • fvm.drom2psl package
        • Submodules
        • Module contents
      • fvm.toolchains package
        • Subpackages
        • Submodules
        • Module contents
    • Submodules
      • fvm.argument_parser module
        • create_parser()
      • fvm.framework module
        • FvmFramework
        • getlogformattool()
      • fvm.generate_test_cases module
        • generate_test_case()
        • html_to_oneline()
      • fvm.helpers module
        • get_fvm_shortversion()
        • get_fvm_version()
        • getscriptname()
        • insert_line_after_target()
        • insert_line_before_target()
        • is_inside_venv()
        • is_interactive()
        • readable_time()
      • fvm.logcounter module
        • LogCounter
      • fvm.manage_allure module
        • change_logo()
        • create_parser()
        • download_allure()
        • ensure_allure()
        • extract_allure()
        • get_allure_bin_path()
        • get_allure_dir()
        • get_allure_zip_path()
        • install_allure()
        • main()
        • make_allure_executable()
      • fvm.reports module
        • copy_results_to_allure_results()
        • generate_allure()
        • generate_html_report()
        • generate_text_report()
        • generate_xml_report()
        • get_all_steps()
        • pretty_summary()
        • rich_table_to_markdown()
        • show_allure()
      • fvm.steps module
        • Steps
      • fvm.tables module
        • show_coverage_summary()
        • show_friendliness_score()
        • show_prove_summary()
        • show_step_summary()
    • Module contents
Previous Next

© Copyright 2024-2026, Universidad de Sevilla.

Built with Sphinx using a theme provided by Read the Docs.
Other Versions v: main
Tags
1.0.0rc1
1.0.0rc2
1.0.0rc3
Branches
main