Optimization of test cases generated by Proof2Test for simple test cases in Eiffel

Abstract

The Proof2Test system, designed for the AutoProof environment, uses the underlying SMT Solving Technology to generate test cases for proof failures. These test cases can be simplified by reducing the magnitude of the values of the variables present in them. The present work describes a simplification strategy to generate test cases that use small values and are easily understandable by programmers.

Attachments
Masters' Thesis (738.74 KB)
Publication Type
Publication Year
Subject
Computer Science