### Skapa referens, olika format (klipp och klistra)

**Harvard**

Dybjer, P., Haiyan, Q. och Takeyama, M. (2004) *Verifying Haskell programs by combining testing, model checking and interactive theorem proving*.

** BibTeX **

@conference{

Dybjer2004,

author={Dybjer, Peter and Haiyan, Qiao and Takeyama, Makoto},

title={Verifying Haskell programs by combining testing, model checking and interactive theorem proving},

booktitle={Information and Software Technology, special issue, edited by Huimin Lin, Hans-Dieter Ehrich, and T.H. Tse},

pages={1011 - 1025},

abstract={We propose a program verification method that combines random testing, model checking and interactive theorem proving. Testing and model checking are used for debugging programs and specifications before a costly interactive proof attempt. During proof development, testing and model checking quickly eliminate false conjectures and generate counterexamples which help to correct them. With an interactive theorem prover we also ensure the correctness of the reduction of a top level problem to subproblems that can be tested or proved. We demonstrate the method using our random testing tool and binary decision diagrams-based (BDDs) tautology checker, which are added to the Agda/Alfa interactive proof assistant for dependent type theory. In particular we apply our techniques to the verification of Haskell programs. The first example verifies the BDD checker itself by testing its components. The second uses the tautology checker to verify bitonic sort together with a proof that the reduction of the problem to the checked form is correct.},

year={2004},

keywords={Program verification, Random testing, Proof-assistants, Type theory, Binary decision diagrams, Haskell},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 2256

A1 Dybjer, Peter

A1 Haiyan, Qiao

A1 Takeyama, Makoto

T1 Verifying Haskell programs by combining testing, model checking and interactive theorem proving

YR 2004

T2 Information and Software Technology, special issue, edited by Huimin Lin, Hans-Dieter Ehrich, and T.H. Tse

SP 1011

OP 1025

AB We propose a program verification method that combines random testing, model checking and interactive theorem proving. Testing and model checking are used for debugging programs and specifications before a costly interactive proof attempt. During proof development, testing and model checking quickly eliminate false conjectures and generate counterexamples which help to correct them. With an interactive theorem prover we also ensure the correctness of the reduction of a top level problem to subproblems that can be tested or proved. We demonstrate the method using our random testing tool and binary decision diagrams-based (BDDs) tautology checker, which are added to the Agda/Alfa interactive proof assistant for dependent type theory. In particular we apply our techniques to the verification of Haskell programs. The first example verifies the BDD checker itself by testing its components. The second uses the tautology checker to verify bitonic sort together with a proof that the reduction of the problem to the checked form is correct.

LA eng

DO 10.1016/j.infsof.2004.07.002

LK http://dx.doi.org/10.1016/j.infsof.2004.07.002

OL 30