Testing processes usually aim at high coverage, but loops severely limit coverage ambitions since the number of iterations is generally not predictable. The most common solution is extreme: it limits its aims to achieving branch coverage, which only considers loop executions that iterate the body either once or not at all. This approach misses bugs that only arise after two or more iterations. To achieve more meaningful coverage, testing strategies may unroll loops, iterating them up to n times for some n greater than one, chosen pragmatically in consideration of the available computational power. While loop unrolling is a standard part of compiler optimization techniques, its use in testing is less common. Part of the reason is that the concept, while seemingly intuitive, lacks a generally accepted and precise specification. The present article provides a formal definition and a set of formal properties of unrolling. All the properties have mechanically been proved correct (through the Isabelle proof assistant). Using this definition, we have applied an unrolling strategy to an automated testing framework. The results indicate how many bugs the usual approach misses by limiting itself to branch coverage, analyzing the benefits (in number of detected bugs) and costs of successive unrolling levels. They provide important factual information on the merits of including unrolling in testing strategies and coverage measurement.

Techniques of Automatic Program Repair (APR) have the potential of thoroughly facilitating the task of producing quality software. After a promising start, however, progress in making APR practical has been hindered by the lack of a common framework to support the multiplicity of APR ideas and tools, and of target programming languages and environments. In this position paper we outline a general framework to enable the APR community to benefit from each other's advances, in particular through a standard language for describing bugs and their fixes. Such a common framework - which is also applicable to work on fault seeding - could be a tremendous benefit to researchers and developers of Interactive Development Environments (IDEs) who are working to make APR an effective part of the software developer's practical experience.

Automatic program repair usually relies heavily on test cases for both bug identification and fix validation. The issue is that writing test cases is tedious, running them takes much time, and validating a fix through tests does not guarantee its correctness. The novel idea in the Proof2Fix methodology and tool presented here is to rely instead on a program prover, without the need to run tests or to run the program at all. Results show that Proof2Fix automatically finds and fixes significant historical bugs.

MCDC, for "Modified Condition/Decision Coverage", is a test coverage criterion recommended in several important industrial software safety standards. The intuition behind MCDC is that it should be more effective than industry's default coverage criterion, branch coverage, since it uses a finer-grain decomposition of program conditions. Manually generating MCDC-compliant test suites is, however, tedious and error-prone; there is, as a result, little empirical evidence of whether that intuition holds up in practice. Does MCDC really provide enough of an advantage over branch coverage to justify the extra work and longer test runs? To help answer this question, the present work takes advantage of verification technology that combines tests and proofs, based on the Auto-Proof program verifier. For each decision point in the program, the approach proceeds in four steps. First, compute a set of conditions that satisfy MCDC. Then, inject into the program, for each combination, an incorrect instruction (a "seeded contradiction" in the terminology of previous work). Next, apply the prover to verify the instrumented program; the prover naturally fails, but in the process it produces a set of counterexamples covering all the combinations. Finally, turn this result into a directly usable test suite-guaranteed by construction to satisfy the MCDC criterion. The results, on a significant set of example programs, yield insights on how MCDC coverage compares to branch coverage and adaptive random testing when trying to detect faults.

A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. Unlike a failed test, which provides concrete evidence of an actual bug in the program, a failed proof leaves the programmer in the dark. Can we instead learn something useful from it? The work reported here takes advantage of the rich information that some automatic provers internally collect about the program when attempting a proof. If the proof fails, the Proof2Test tool presented in this article uses the counterexample generated by the prover (specifically, the SMT solver underlying the Boogie tool used in the AutoProof system to perform correctness proofs of contract‐equipped Eiffel programs) to produce a failed test, which provides the programmer with immediately exploitable information to correct the program. The discussion presents Proof2Test and the application of the ideas and tool to a collection of representative examples.

The regression test suite, a key resource for managing program evolution, needs to achieve 100% coverage, or very close, to be useful. Devising a test suite manually is unacceptably tedious, but existing automated methods are often inefficient. The method described in this article, “Seeding Contradiction”, inserts incorrect instructions into every basic block of the program, enabling an SMT-based Hoare-style prover to generate a counterexample for every branch of the program and, from the collection of all such counterexamples, a test suite. The method is static, works fast, and achieves excellent coverage.

In software verification, a successful automated program proof is the ultimate triumph. The road to such success is, however, paved with many failed proof attempts. The message produced by the prover when a proof fails is often obscure, making it very hard to know how to proceed further. The work reported here attempts to help in such cases by providing immediately understandable counterexamples. To this end, it introduces an approach called Counterexample Extraction and Minimization (CEAM). When a proof fails, CEAM turns the counterexample model generated by the prover into a a clearly understandable version; it can in addition simplify the counterex-amples further by minimizing the integer values they contain. We have implemented the CEAM approach as an extension to the AutoProof verifier and demonstrate its application to a collection of examples.