Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges

Abstract

This paper reviews some common knowledge about establishing correctness of programs and the current status of program specification and verification. While doing so, it identifies several challenges related to the grand challenge of building a verifying compiler. The paper argues that invariants are central to establishing correctness of programs and that thus, a major part of an automatic program verifier must be automated support for verifying invariants, a significant problem in itself. The paper discusses where the invariants come from, what can be involved in establishing that they hold, and the extent to which the process of finding and proving invariants can be automated. The paper also discusses several of the related challenges identified, argues that addressing them would make the significance to global program behavior of feedback from a verifying compiler clearer, and recommends that many of them should be included within the scope of the grand challenge.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2005
Accession Number
ADA462162

Entities

People

  • Myla M. Archer

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Addressing
  • Automatic
  • Availability
  • Classification
  • Compilers
  • Contracts
  • Feedback
  • Information Operations
  • Instructions
  • Military Research
  • Monitoring
  • Security
  • Specifications
  • Standards
  • Switzerland

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computer Vision.
  • Strategic Security Studies