Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Gross, Jason, Zimmermann, Théo, Poddar-Agrawal, Miraya, Chlipala, Adam · arXiv (Cornell University) · 2000
A program fails. Under which circumstances does this failure occur? One single algorithm, the delta debugging algorithm, suffices to determine these failure-inducing circumstances. Delta debugging tests a program systematically and automatically to isolate failure-inducing circumstances such as the program input, changes to the program code, or executed statements.