Benutzer: Gast  Login
Originaltitel:
Counterexample Generation for Higher-Order Logic Using Functional and Logic Programming 
Übersetzter Titel:
Generierung von Gegenbeispielen für höherstufige Logik unter Verwendung von funktionalen und logischen Programmen 
Jahr:
2013 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Runciman, Colin (Prof.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
testing, theorem proving, formal methods 
Übersetzte Stichworte:
Testen, Theorembeweisen, Formale Methoden 
Schlagworte (SWD):
Gegenbeispiel; Isabelle Programm; HOL 
TU-Systematik:
DAT 706d 
Kurzfassung:
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. 
Übersetzte Kurzfassung:
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. 
Mündliche Prüfung:
26.03.2013 
Dateigröße:
666381 bytes 
Seiten:
117 
Letzte Änderung:
27.11.2013