Klever

Klever is a software verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of requirements using software model checkers. You can learn more about Klever at the project site.

Contents

• Deployment
  • Hardware Requirements
  • Software Requirements
  • Klever Addons
  • Klever Build Bases
  • Deployment Configuration File
  • Structure of Klever Git Repository
  • Deployment Variants
• Tutorial
  • Preparing Build Bases
  • Signing in
  • Starting Verification
  • Decision Progress
  • Analyzing Verification Results
  • Analyzing Error Traces
  • Creating Marks
  • What’s Next?
• Developer Documentation
  • How to Write This Documentation
  • Using Git Repository
  • Releases
  • Updating List of Required Python Packages
  • Deployment for Development Purposes
  • How to generate build bases for testing Klever
  • Generating Bare CPAchecker Benchmarks
  • Using PyCharm IDE
  • Extended Violation Witness Format
  • Error Trace Format
  • Code Coverage Format
• Glossary