One of the greatest challenges facing designers of equipment to be used in a nuclear arms control treaty is how to convince the other party in the treaty to trust its results and functionality. Whether the host provides equipment meant to prove treaty obligations and the inspector needs to gain that trust (commonly referred to as authentication), or the inspector provides this equipment and the host needs to gain this trust (commonly considered to be included in certification), one party generally has higher confidence in the equipment at the start of a treaty regime and the other party needs to gain that confidence prior to use. While we focus on authentication in this document—that is, the inspector gaining confidence in host-provided equipment—our conclusions will likely apply to host certification of inspector-provided equipment.

98 NUCLEAR DISARMAMENT, SAFEGUARDS, AND PHYSICAL P↗

DOE OSTI2014

Survey of Existing Tools for Formal Verification

Formal methods have come into wide use because of their effectiveness in verifying "safety and security" requirements of digital systems; a set of requirements for which testing is mostly ineffective. Formal methods are routinely used in the design and verification of high-consequence digital systems in industry. This report outlines our work in assessing the capabilities of commercial and open source formal tools and the ways in which they can be leveraged in digital design workflows.

Armstrong, Robert C.↗

DOE OSTI2014

Digital Design Verification using Formal and Complexity Analysis.

Abstract not provided.

Armstrong, Robert C.↗