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?
• CLI
  • Credentials
  • Starting Solution of Verification Jobs
  • Waiting for Solution of Verification Job
  • Obtaining Verification Results
• Development of Requirement Specifications
  • Analysis and Description of Checked Requirements
  • Development of Requirements Specification
  • Testing of Requirements Specification
  • Using Argument Signatures to Distinguish Objects
• Developer Documentation
  • How to Write This Documentation
  • Using Git Repository
  • Releases
  • Updating List of Required Python Packages
  • 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