---
_id: '2289'
abstract:
- lang: eng
  text: Formal verification aims to improve the quality of software by detecting errors
    before they do harm. At the basis of formal verification is the logical notion
    of correctness, which purports to capture whether or not a program behaves as
    desired. We suggest that the boolean partition of software into correct and incorrect
    programs falls short of the practical need to assess the behavior of software
    in a more nuanced fashion against multiple criteria. We therefore propose to introduce
    quantitative fitness measures for programs, specifically for measuring the function,
    performance, and robustness of reactive programs such as concurrent processes.
    This article describes the goals of the ERC Advanced Investigator Project QUAREM.
    The project aims to build and evaluate a theory of quantitative fitness measures
    for reactive models. Such a theory must strive to obtain quantitative generalizations
    of the paradigms that have been success stories in qualitative reactive modeling,
    such as compositionality, property-preserving abstraction and abstraction refinement,
    model checking, and synthesis. The theory will be evaluated not only in the context
    of software and hardware engineering, but also in the context of systems biology.
    In particular, we will use the quantitative reactive models and fitness measures
    developed in this project for testing hypotheses about the mechanisms behind data
    from biological experiments.
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Henzinger TA. Quantitative reactive modeling and verification. <i>Computer
    Science Research and Development</i>. 2013;28(4):331-344. doi:<a href="https://doi.org/10.1007/s00450-013-0251-7">10.1007/s00450-013-0251-7</a>
  apa: Henzinger, T. A. (2013). Quantitative reactive modeling and verification. <i>Computer
    Science Research and Development</i>. Springer. <a href="https://doi.org/10.1007/s00450-013-0251-7">https://doi.org/10.1007/s00450-013-0251-7</a>
  chicago: Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.”
    <i>Computer Science Research and Development</i>. Springer, 2013. <a href="https://doi.org/10.1007/s00450-013-0251-7">https://doi.org/10.1007/s00450-013-0251-7</a>.
  ieee: T. A. Henzinger, “Quantitative reactive modeling and verification,” <i>Computer
    Science Research and Development</i>, vol. 28, no. 4. Springer, pp. 331–344, 2013.
  ista: Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer
    Science Research and Development. 28(4), 331–344.
  mla: Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” <i>Computer
    Science Research and Development</i>, vol. 28, no. 4, Springer, 2013, pp. 331–44,
    doi:<a href="https://doi.org/10.1007/s00450-013-0251-7">10.1007/s00450-013-0251-7</a>.
  short: T.A. Henzinger, Computer Science Research and Development 28 (2013) 331–344.
corr_author: '1'
date_created: 2018-12-11T11:56:47Z
date_published: 2013-10-05T00:00:00Z
date_updated: 2024-10-09T20:55:17Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00450-013-0251-7
ec_funded: 1
file:
- access_level: open_access
  checksum: f117a00f9f046165bfa95595681e08a0
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:17:51Z
  date_updated: 2020-07-14T12:45:37Z
  file_id: '5308'
  file_name: IST-2016-626-v1+1_s00450-013-0251-7.pdf
  file_size: 570361
  relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: '        28'
issue: '4'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 331 - 344
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: Computer Science Research and Development
publication_status: published
publisher: Springer
publist_id: '4642'
pubrep_id: '626'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative reactive modeling and verification
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 28
year: '2013'
...