研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	英語
発行・発表の年月	2004/12
形態種別	学術雑誌
査読	査読あり
標題	Verifying Haskell Programs by Combining, Model Checking and Interactive Theorem Proving
執筆形態	共著
掲載誌名	Information and Softwave Technology, Vol 46, No15
掲載区分	国外
巻・号・頁	46(15),pp.1011-1025
著者・共著者	Peter Dybjer, Qiao Haiyan, Makoto Takeyama
概要	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 ...