Counterexample Generation for Higher-Order Logic Using Functional and Logic Programming ; Generierung von Gegenbeispielen für höherstufige Logik unter Verwendung von funktionalen und logischen Programmen
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Doctoral Thesis;
Electronic Thesis;
E-Book
Title:
Counterexample Generation for Higher-Order Logic Using Functional and Logic Programming ; Generierung von Gegenbeispielen für höherstufige Logik unter Verwendung von funktionalen und logischen Programmen
Contributor:
Bulwahn, Lukas
[Author]
Published:
Technical University of Munich; Technische Universität München, 2013-11-27
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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. ; 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.