loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Third International Conference On Quality Software
Verifying Haskell Programs by Combining Testing and Proving
Dallas, Texas
November 06-November 07
ISBN: 0-7695-2015-4
ASCII Text
x 
 
Peter Dybjer, Qiao Haiyan, Makoto Takeyama, "Verifying Haskell Programs by Combining Testing and Proving," Quality Software, International Conference on, pp. 272, Third International Conference On Quality Software, 2003.
 
 
BibTex
x
 
@article{ 10.1109/QSIC.2003.1319111,
author = {Peter Dybjer and Qiao Haiyan and Makoto Takeyama},
title = {Verifying Haskell Programs by Combining Testing and Proving},
journal ={Quality Software, International Conference on},
volume = {0},
year = {2003},
isbn = {0-7695-2015-4},
pages = {272},
doi = {http://doi.ieeecomputersociety.org/10.1109/QSIC.2003.1319111},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Quality Software, International Conference on
TI - Verifying Haskell Programs by Combining Testing and Proving
SN - 0-7695-2015-4
SP
EP
A1 - Peter Dybjer,
A1 - Qiao Haiyan,
A1 - Makoto Takeyama,
PY - 2003
KW - program verification
KW - random testing
KW - proof-assistants
KW - type theory
KW - BDDs and Haskell
VL - 0
JA - Quality Software, International Conference on
ER -
 
Peter Dybjer, Chalmers University of Technology, Sweden
Qiao Haiyan, Chalmers University of Technology, Sweden
Makoto Takeyama, Chalmers University of Technology, Sweden
We propose a method for improving confidence in the correctness of Haskell programs by combining testing and proving. Testing is used for debugging programs and specification before a costly proof attempt. During a proof development, testing also quickly eliminates wrong conjectures. Proving helps us to decompose a testing task in a way that is guaranteed to be correct. To demonstrate the method we have extended the Agda/Alfa proof assistant for dependent type theory with a tool for random testing. As an example we show how the correctness of a BDD-algorithm written in Haskell is verified by testing properties of component functions. We also discuss faithful translations from Haskell to type theory.
Index Terms:
program verification, random testing, proof-assistants, type theory, BDDs and Haskell
Citation:
Peter Dybjer, Qiao Haiyan, Makoto Takeyama, "Verifying Haskell Programs by Combining Testing and Proving," qsic, pp.272, Third International Conference On Quality Software, 2003
Usage of this product signifies your acceptance of the Terms of Use.