User: Guest  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 
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. 
Oral examination:
26.03.2013 
File size:
666381 bytes 
Pages:
117 
Last change:
27.11.2013