Login
Original title:
Counterexample Generation for Higher-Order Logic Using Functional and Logic Programming
Translated title:
Generierung von Gegenbeispielen für höherstufige Logik unter Verwendung von funktionalen und logischen Programmen
Author:
Year:
2013
Document type:
Dissertation
Institution:
Fakultät für Informatik
Advisor:
Nipkow, Tobias (Prof., Ph.D.)
Referee:
Nipkow, Tobias (Prof., Ph.D.); Runciman, Colin (Prof.)
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
testing, theorem proving, formal methods
Translated keywords:
Testen, Theorembeweisen, Formale Methoden
Controlled terms:
Gegenbeispiel; Isabelle Programm; HOL
TUM classification:
DAT 706d
Abstract:
This thesis presents a counterexample generator for the interactive theorem prover Isabelle/HOL that uncovers faulty specifications and invalid conjectures using testing methods. Its contributions are two testing strategies: exhaustive testing
with concrete values; and symbolic testing, evaluating conjectures with a narrowing strategy. We present techniques to deal with conditional conjectures, including an approach to synthesize test data generators derived from the premise's definition.
Translated abstract:
Diese Dissertation beschreibt einen Gegenbeispielgenerator für den interaktiven Theorembeweiser Isabelle/HOL, der fehlerhafte Spezifikationen und ungültige Hypothesen durch Testmethoden aufdeckt. Ein Beitrag dieser Arbeit sind zwei neue Teststrategien: erschöpfendes Testen und symbolisches Testen mit einer Narrowing-Strategie. Die Arbeit beschreibt Techniken um mit bedingten Hypothesen umzugehen und die Synthese von Testdatengeneratoren, die aus der Definition der Bedingung erzeugt werden.
Date of submission:
08.10.2012
Oral examination:
26.03.2013
File size:
666381 bytes
Pages:
117
Last change:
27.11.2013
BibTeX