Verification is experimentation!

Research output: Contribution to journalArticleAcademicpeer-review

7 Citations (Scopus)

Abstract

The formal verification of concurrent systems is usually seen as an example par excellence of the application of mathematical methods to computer science. Although the practical application of such verification methods will always be limited by the underlying forms of combinatorial explosion, recent years have shown remarkable progress in computer-aided formal verification. This makes formal verification a practical proposition for a growing class of real-life applications, and has put formal methods on the agenda of industry, in particular in the areas where correctness is critical in one sense or another. Paradoxically, the results of this progress provide evidence that successful applications of formal verification have significant elements that do not fit the paradigm of pure mathematical reasoning. In this essay we argue that verification is part of an experimental paradigmin at least two senses. Wesubmit that this observation has consequences for the ways in which we should research and apply formal methods.
Original languageUndefined
Article number10.1007/s100090100050
Pages (from-to)107-217
Number of pages111
JournalInternational journal on software tools for technology transfer
Volume3
Issue number2
DOIs
Publication statusPublished - 2001

Keywords

  • FMT-TOOLS
  • FMT-CBD: CORRECTNESS BY DESIGN
  • FMT-TESTING
  • IR-63259
  • FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS
  • EWI-6380

Cite this

@article{1b36d07f9b5a430ca10af6a8aaa810d1,
title = "Verification is experimentation!",
abstract = "The formal verification of concurrent systems is usually seen as an example par excellence of the application of mathematical methods to computer science. Although the practical application of such verification methods will always be limited by the underlying forms of combinatorial explosion, recent years have shown remarkable progress in computer-aided formal verification. This makes formal verification a practical proposition for a growing class of real-life applications, and has put formal methods on the agenda of industry, in particular in the areas where correctness is critical in one sense or another. Paradoxically, the results of this progress provide evidence that successful applications of formal verification have significant elements that do not fit the paradigm of pure mathematical reasoning. In this essay we argue that verification is part of an experimental paradigmin at least two senses. Wesubmit that this observation has consequences for the ways in which we should research and apply formal methods.",
keywords = "FMT-TOOLS, FMT-CBD: CORRECTNESS BY DESIGN, FMT-TESTING, IR-63259, FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS, EWI-6380",
author = "Hendrik Brinksma",
year = "2001",
doi = "10.1007/s100090100050",
language = "Undefined",
volume = "3",
pages = "107--217",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer",
number = "2",

}

Verification is experimentation! / Brinksma, Hendrik.

In: International journal on software tools for technology transfer, Vol. 3, No. 2, 10.1007/s100090100050, 2001, p. 107-217.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Verification is experimentation!

AU - Brinksma, Hendrik

PY - 2001

Y1 - 2001

N2 - The formal verification of concurrent systems is usually seen as an example par excellence of the application of mathematical methods to computer science. Although the practical application of such verification methods will always be limited by the underlying forms of combinatorial explosion, recent years have shown remarkable progress in computer-aided formal verification. This makes formal verification a practical proposition for a growing class of real-life applications, and has put formal methods on the agenda of industry, in particular in the areas where correctness is critical in one sense or another. Paradoxically, the results of this progress provide evidence that successful applications of formal verification have significant elements that do not fit the paradigm of pure mathematical reasoning. In this essay we argue that verification is part of an experimental paradigmin at least two senses. Wesubmit that this observation has consequences for the ways in which we should research and apply formal methods.

AB - The formal verification of concurrent systems is usually seen as an example par excellence of the application of mathematical methods to computer science. Although the practical application of such verification methods will always be limited by the underlying forms of combinatorial explosion, recent years have shown remarkable progress in computer-aided formal verification. This makes formal verification a practical proposition for a growing class of real-life applications, and has put formal methods on the agenda of industry, in particular in the areas where correctness is critical in one sense or another. Paradoxically, the results of this progress provide evidence that successful applications of formal verification have significant elements that do not fit the paradigm of pure mathematical reasoning. In this essay we argue that verification is part of an experimental paradigmin at least two senses. Wesubmit that this observation has consequences for the ways in which we should research and apply formal methods.

KW - FMT-TOOLS

KW - FMT-CBD: CORRECTNESS BY DESIGN

KW - FMT-TESTING

KW - IR-63259

KW - FMT-IA: INDUSTRIAL APPLICATION OF FORMAL METHODS

KW - EWI-6380

U2 - 10.1007/s100090100050

DO - 10.1007/s100090100050

M3 - Article

VL - 3

SP - 107

EP - 217

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 2

M1 - 10.1007/s100090100050

ER -