---
_id: '478'
abstract:
- lang: eng
  text: 'Software systems are playing an increasing role in our everyday life, and
    as the amount of software applications grows, so does their complexity and the
    relevance of their computations. Software components can be found in many systems
    that are charged with safety-critical tasks, such as control systems for aviation
    or power plants. Hence, software verification techniques that are capable of proving
    the absence of critical errors are becoming more and more important in the field
    software engineering. A well-established approach to software verification is
    model checking. Applying this technique involves an exhaustive exploration of
    a state space model corresponding to the system under consideration. The major
    challenge in model checking is the so-called state explosion problem: The state
    space of a software system grows exponentially with its size. Thus, the straightforward
    modelling of real-life systems practically impossible. A common approach to this
    problem is the application of abstraction techniques, which reduce the original
    state space by mapping it on a significantly smaller abstract one. Abstraction
    inherently involves a loss of information, and thus, the resulting abstract model
    may be too imprecise for a definite result in verification. Therefore, abstraction
    is typically combined with abstraction refinement: An initially very coarse abstract
    model is iteratively refined, i.e. enriched with new details about the original
    system, until a level of abstraction is reached that is precise enough for a definite
    outcome. Abstraction refinement-based model checking is fully automatable and
    it is considered as one of the most promising approaches to the state explosion
    problem in verification. However, it is still faced with a number of challenges.
    There exist several types of abstraction techniques and not every type is equally
    well-suited for all kinds of systems and verification tasks. Moreover, the selection
    of adequate refinement steps is nontrivial and typically the most crucial part
    of the overall approach: Unfavourable refinement decisions can compromise the
    state space-reducing effect of abstraction, and as a consequence, can easily lead
    to the failure of verification. It is, however, hard to predict which refinement
    steps will eventually be expedient for verification – and which not.'
author:
- first_name: Nils
  full_name: Timm, Nils
  last_name: Timm
citation:
  ama: Timm N. <i>Three-Valued Abstraction and Heuristic-Guided Refinement for Verifying
    Concurrent Systems</i>. Universität Paderborn; 2013.
  apa: Timm, N. (2013). <i>Three-Valued Abstraction and Heuristic-Guided Refinement
    for Verifying Concurrent Systems</i>. Universität Paderborn.
  bibtex: '@book{Timm_2013, title={Three-Valued Abstraction and Heuristic-Guided Refinement
    for Verifying Concurrent Systems}, publisher={Universität Paderborn}, author={Timm,
    Nils}, year={2013} }'
  chicago: Timm, Nils. <i>Three-Valued Abstraction and Heuristic-Guided Refinement
    for Verifying Concurrent Systems</i>. Universität Paderborn, 2013.
  ieee: N. Timm, <i>Three-Valued Abstraction and Heuristic-Guided Refinement for Verifying
    Concurrent Systems</i>. Universität Paderborn, 2013.
  mla: Timm, Nils. <i>Three-Valued Abstraction and Heuristic-Guided Refinement for
    Verifying Concurrent Systems</i>. Universität Paderborn, 2013.
  short: N. Timm, Three-Valued Abstraction and Heuristic-Guided Refinement for Verifying
    Concurrent Systems, Universität Paderborn, 2013.
date_created: 2017-10-17T12:42:25Z
date_updated: 2022-01-06T07:01:22Z
ddc:
- '040'
department:
- _id: '77'
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T14:06:05Z
  date_updated: 2018-03-15T14:06:05Z
  file_id: '1324'
  file_name: 478-Dissertation-Timm.pdf
  file_size: 931458
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T14:06:05Z
has_accepted_license: '1'
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
title: Three-Valued Abstraction and Heuristic-Guided Refinement for Verifying Concurrent
  Systems
type: dissertation
user_id: '477'
year: '2013'
...