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
- Autor:
- Bulwahn, Lukas
- Jahr:
- 2013
- Dokumenttyp:
- Dissertation
- Fakultät/School:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=1115870
- Eingereicht am:
- 08.10.2012
- Mündliche Prüfung:
- 26.03.2013
- Dateigröße:
- 666381 bytes
- Seiten:
- 117
- Urn (Zitierfähige URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130326-1115870-0-3
- Letzte Änderung:
- 27.11.2013
BibTeX