Program Verification for Optimized Byte Copy

Abstract

We present a program to copy bytes, together with a formal specification and a proof that the code satisfies the specification. The program, which is in the critical path for a network implementation, has been tuned carefully over a period of time; the proof covers the entire program, and is easily updated if the program is modified. The program is written in the Standard ML programming language and was produced as part of the Fox Project implementation of the TCP/IP protocol suite.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1994
Accession Number
ADA283915

Entities

People

  • Edoardo S. Biagioni

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Compilers
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Language
  • Megabytes
  • Network Protocols
  • Operating Systems
  • Optimization
  • Programming Languages
  • Side Effects
  • Specifications

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computer Networking
  • Software Engineering