CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Peter Dybjer (Institutionen för datavetenskap, Programmeringslogik) ; Qiao Haiyan ; Makoto Takeyama
Information and Software Technology, special issue, edited by Huimin Lin, Hans-Dieter Ehrich, and T.H. Tse Vol. 46 (2004), 15, p. 1011 - 1025.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Program verification, Random testing, Proof-assistants, Type theory, Binary decision diagrams, Haskell



Denna post skapades 2006-08-25. Senast ändrad 2013-08-12.
CPL Pubid: 2256

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap, Programmeringslogik (2002-2004)

Ämnesområden

Information Technology

Chalmers infrastruktur