Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Adobe portable document format (pdf)
Copyright noticeThis material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This paper describes the main results of the V3F project (which stands for “Validation and verification of software handling float- ing-point numbersâ€). The goal of this project was to provide tools to support the verification and validation process of programs with floating- point numbers. We did investigate two directions: structural testing of a program with floating-point numbers and verification of the confor- mity of a program handling floating-point numbers, with its specification. Practically, a constraint solver over the floats was developed for the gen- eration of test sets in structural testing framework. Different techniques have been developed to evaluate the distance between the semantics of a program over the real numbers and its semantics over the floating-point numbers.
Bertrand Jeannet
Bertrand.Jeannet@irisa.fr
Thierry Jéron
Thierry.Jeron@irisa.fr
@InProceedings{V3F_CSTVA06,
Author = {Blanc, B. and Bouquet, F. and Gotlieb, A. and Jeannet, B. and Jéron, T. and Legeard, B. and Marre, B. and Michel, C. and Rueher, M.},
Title = {The {V3F} Project},
BookTitle = {Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA06), Nantes},
editor = {Blanc, B. and Gotlieb, A. and Michel, C.},
Year = {2006}
}
Get EndNote Reference (.ref)