Black, P.
and Walia, K.
(2020),
SATE VI Ockham Sound Analysis Criteria, NIST Interagency/Internal Report (NISTIR), National Institute of Standards and Technology, Gaithersburg, MD, [online], https://doi.org/10.6028/NIST.IR.8304
(Accessed April 19, 2024)
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
Secure .gov websites use HTTPS
A lock (
) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.
SATE VI Ockham Sound Analysis Criteria
Published
Author(s)
, Kanwardeep S. Walia
Abstract
Static analyzers examine the source or executable code of programs to find problems. Many static analyzers use heuristics or approximations to examine programs with millions of lines of code for hundreds of classes of problems. The Ockham Sound Analysis Criteria recognizes static analyzers that are precise. In brief the criteria are (1) the analyzer's findings are claimed to always be correct, (2) it produces findings for most of a program, and (3) even one incorrect finding disqualifies an analyzer. This document begins by explaining the background and requirements of the Ockham Criteria and how we determine if a tool satisfies it. As part of Static Analysis Tool Exposition (SATE) VI, we examined two tools: Astree and Frama-C with the Evolved Value Analysis (Eva) plug-in. Examining the tool outputs led us to find several systematic mistakes in the Juliet 1.3 test suite and thousands of mistakes in its manifest of known errors. Our conclusion is that Astree and Frama-C with Eva satisfied the SATE VI Ockham Sound Analysis Criteria.Citation
NIST Interagency/Internal Report (NISTIR) - 8304
Report Number
8304
NIST Pub Series
Pub Type
NIST Pubs
Download Paper
Keywords
Ockham Criteria, software assurance, software measurement, software testing, sound analysis, static analysis
Citation
Created May 19, 2020, Updated May 4, 2021