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:
- Bulwahn, Lukas
- Year:
- 2013
- Document type:
- Dissertation
- Faculty/School:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=1115870
- Date of submission:
- 08.10.2012
- Oral examination:
- 26.03.2013
- File size:
- 666381 bytes
- Pages:
- 117
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130326-1115870-0-3
- Last change:
- 27.11.2013
BibTeX