Open AccessExpert Assessment of Verification Tool Results
Author(s) -
Владимир Анатольевич Гратинский,
Евгений Михайлович Новиков,
Илья Сергеевич Захаров
Publication year - 2020
Publication title -
trudy instituta sistemnogo programmirovaniâ ran/trudy instituta sistemnogo programmirovaniâ
Language(s) - English
Resource type - Journals
eISSN - 2220-6426
pISSN - 2079-8156
DOI - 10.15514/ispras-2020-32(5)-1
Subject(s) - verification , computer science , software verification , functional verification , intelligent verification , completeness (order theory) , software engineering , runtime verification , verification and validation , high level verification , formal verification , verification and validation of computer simulation models , semantics (computer science) , programming language , model checking , software , software construction , software system , engineering , mathematical analysis , operations management , statistics , mathematics
Verification tools can produce various kinds of results while checking programs against requirement specifications. Experts, who seek for errors and estimate completeness of verification, mostly appreciate verdicts, violation witnesses and code coverage reports. They need convenient tools for automating the assessment of verification results to apply verification tools in practice when many program configurations and versions are checked against various requirements. In this paper, we propose new methods for expert evaluation of verification results, covering all those problems that are most significant in accordance with our experience in verifying large programs for compliance with a large number of requirements specifications. Some ideas are borrowed from the areas of testing and static analysis. However, specific methods and technical solutions are unique, since the verification results provided by verification tools are either not found in other areas or have special semantics. The paper presents our approaches and their implementation in the Klever software verification framework.