.. Copyright (c) 2020 ISP RAS (http://www.ispras.ru)
   Ivannikov Institute for System Programming of the Russian Academy of Sciences
   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at
       http://www.apache.org/licenses/LICENSE-2.0
   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

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 <https://forge.ispras.ru/projects/klever>`__.

Contents
========

.. toctree::
   :maxdepth: 2

   deploy
   tutorial
   cli
   dev_decomposition_conf
   dev_common_api_models
   dev_req_specs
   dev_env_model_specs
   dev_verifier_profiles
   verifying_new_program
   dev
   glossary

..
   Indices and tables
   ==================

   * :ref:`genindex`
   * :ref:`modindex`
   * :ref:`search`