Random testing in Isabelle/HOL
- 8 November 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
When developing non-trivial formalizations in a theorem prover, a considerable amount of time is devoted to "debugging" specifications and conjectures by failed proof attempts. To detect such problems early in the proof and save development time, we have extended the Isabelle theorem prover with a tool for testing specifications by evaluating propositions under an assignment of random values to free variables. Distribution of the test data is optimized via mutation testing. The technical contributions are an extension of earlier work with inductive definitions and a generic method for randomly generating elements of recursive datatypes.Keywords
This publication has 12 references indexed in Scilit:
- Bounded Model Generation for Isabelle/HOLElectronic Notes in Theoretical Computer Science, 2005
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Science and Business Media LLC ,2005
- Applications of Polytypism in Theorem ProvingLecture Notes in Computer Science, 2003
- Combining Testing and Proving in Dependent Type TheoryLecture Notes in Computer Science, 2003
- Executing Higher Order LogicLecture Notes in Computer Science, 2002
- Automating first-order relational logicPublished by Association for Computing Machinery (ACM) ,2000
- QuickCheckACM SIGPLAN Notices, 2000
- Mutation operators for specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2000
- The integration of functions into logic programming: From theory to practiceThe Journal of Logic Programming, 1994
- FINDER: Finite domain enumerator system descriptionLecture Notes in Computer Science, 1994