Tests and Proofs

1. Front Matter

   PDF

2. Combining Static and Dynamic Reasoning for Bug Detection

   • Yannis Smaragdakis, Christoph Csallner

   Pages 1-16

3. Testable Requirements and Specifications

   • Jonathan S. Ostroff, Faraz Ahmadi Torshizi

   Pages 17-40

4. Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic

   • Philipp Rümmer, Muhammad Ali Shah

   Pages 41-60

5. Testing and Verifying Invariant Based Programs in the SOCOS Environment

   • Ralph-Johan Back, Johannes Eriksson, Magnus Myreen

   Pages 61-78

6. Testing and Proving Distributed Algorithms in Constructive Type Theory

   • Qiao Haiyan

   Pages 79-94

7. Automatic Testing from Formal Specifications

   • Manoranjan Satpathy, Michael Butler, Michael Leuschel, S. Ramesh

   Pages 95-113

8. Using Contracts and Boolean Queries to Improve the Quality of Automatic Test Generation

   • Lisa (Ling) Liu, Bertrand Meyer, Bernd Schoeller

   Pages 114-130

9. Symbolic Execution Techniques for Refinement Testing

   • Pascale Le Gall, Nicolas Rapin, Assia Touil

   Pages 131-148

10. Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing

    • Achim D. Brucker, Burkhart Wolff

    Pages 149-168

11. Generating Unit Tests from Formal Proofs

    • Christian Engel, Reiner Hähnle

    Pages 169-188

12. Using Model Checking to Generate Fault Detecting Tests

    • Angelo Gargantini

    Pages 189-206

13. White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing

    • Bernhard Beckert, Christoph Gladisch

    Pages 207-216

14. Back Matter

    PDF

To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs. To test a program is to run it with the expectation of discovering bugs. These two paths to software reliability seem to diverge from the very start: if you have proved your program correct, it is fruitless to comb it for bugs; and if you are testing it, that surely must be a sign that you have given up on any hope to prove its correctness. Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using different kinds of techniques and tools. Dijkstra’s famous pronouncement that tests can only show the presence of errors — in retrospect, perhaps one of the best advertisements one can imagine for testing, as if “only” finding bugs were not already a momentous achievement! — didn’t help make testing popular with provers, or proofs attractive to testers. And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking was one of the first signs that apparent contradiction may yield to complementarity; in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer.

• Automat
• Oracle
• logic
• model checking
• programming
• theorem proving
• tools
• verification

Policies and ethics