University of Illinois Urbana-Champaign

Automatic and Precise Dimensional Analysis

d'Amorim, Marcelo; Hills, Mark; Chen, Feng; Rosu, Grigore

Content Files
Automatic and Precise Dimensional Analysis.pdf

Permalink

https://hdl.handle.net/2142/11131

Description

Title
Automatic and Precise Dimensional Analysis
Author(s)
  • d'Amorim, Marcelo
  • Hills, Mark
  • Chen, Feng
  • Rosu, Grigore
Issue Date
2005-12
Keyword(s)
computer science
Date of Ingest
2009-04-20T18:48:50Z
Abstract
The loss of NASA's Mars climate orbiter is evidence of the importance of units of measurement as a safety policy for software in general and for scientific applications in particular. In this paper we present a static analysis technique that detects violations of the unit policy. The technique relies on domain-specific unit annotations inserted in the code, either manually or automatically with the support of a tool, which are verified conservatively, i.e., all runtime unit errors are detected statically using an automatic theorem prover. This paper informally compares our approach with others, describes the technique in detail, and evaluates a benchmark built of standard programs for unit analysis and important fragments of NASA's SCRover project code.
Type of Resource
text
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11131
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections

Research and Tech Reports - Computer Science PRIMARY