Skip to main content
SpringerLink
Log in
Book cover

Tests and Proofs

First International Conference, TAP 2007 Zurich, Switzerland, February 12-13, 2007 Revised Papers

  • Conference proceedings
  • © 2007

Overview

Editors:
  1. Yuri Gurevich
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Bertrand Meyer
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 4454)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: TAP 2007.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (12 papers)

  1. Front Matter

    Download chapter 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

    Download chapter PDF
Back to top

Other volumes

  1. Tests and Proofs

Keywords

About this book

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.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation