---
_id: '469'
abstract:
- lang: eng
  text: Runtime monitoring aims at ensuring program safety by monitoring the program's
    behaviour during execution and taking appropriate action before a program violates
    some property.Runtime monitoring is in particular important when an exhaustive
    formal verification fails. While the approach allows for a safe execution of programs,
    it may impose a significant runtime overhead.In this paper, we propose a novel
    technique combining verification and monitoring which incurs no overhead during
    runtime at all. The technique proceeds by using the inconclusive result of a verification
    run as the basis for transforming the program into one where all potential points
    of failure are replaced by HALT statements. The new program is safe by construction,
    behaviourally equivalent to the original program (except for unsafe behaviour),and
    has the same performance characteristics.
author:
- first_name: Daniel
  full_name: Wonisch, Daniel
  last_name: Wonisch
- first_name: Alexander
  full_name: Schremmer, Alexander
  last_name: Schremmer
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Wonisch D, Schremmer A, Wehrheim H. Zero Overhead Runtime Monitoring. In:
    <i>Proceedings of the 11th International Conference on Software Engineering and
    Formal Methods (SEFM)</i>. LNCS. ; 2013:244-258. doi:<a href="https://doi.org/10.1007/978-3-642-40561-7_17">10.1007/978-3-642-40561-7_17</a>'
  apa: Wonisch, D., Schremmer, A., &#38; Wehrheim, H. (2013). Zero Overhead Runtime
    Monitoring. In <i>Proceedings of the 11th International Conference on Software
    Engineering and Formal Methods (SEFM)</i> (pp. 244–258). <a href="https://doi.org/10.1007/978-3-642-40561-7_17">https://doi.org/10.1007/978-3-642-40561-7_17</a>
  bibtex: '@inproceedings{Wonisch_Schremmer_Wehrheim_2013, series={LNCS}, title={Zero
    Overhead Runtime Monitoring}, DOI={<a href="https://doi.org/10.1007/978-3-642-40561-7_17">10.1007/978-3-642-40561-7_17</a>},
    booktitle={Proceedings of the 11th International Conference on Software Engineering
    and Formal Methods (SEFM)}, author={Wonisch, Daniel and Schremmer, Alexander and
    Wehrheim, Heike}, year={2013}, pages={244–258}, collection={LNCS} }'
  chicago: Wonisch, Daniel, Alexander Schremmer, and Heike Wehrheim. “Zero Overhead
    Runtime Monitoring.” In <i>Proceedings of the 11th International Conference on
    Software Engineering and Formal Methods (SEFM)</i>, 244–58. LNCS, 2013. <a href="https://doi.org/10.1007/978-3-642-40561-7_17">https://doi.org/10.1007/978-3-642-40561-7_17</a>.
  ieee: D. Wonisch, A. Schremmer, and H. Wehrheim, “Zero Overhead Runtime Monitoring,”
    in <i>Proceedings of the 11th International Conference on Software Engineering
    and Formal Methods (SEFM)</i>, 2013, pp. 244–258.
  mla: Wonisch, Daniel, et al. “Zero Overhead Runtime Monitoring.” <i>Proceedings
    of the 11th International Conference on Software Engineering and Formal Methods
    (SEFM)</i>, 2013, pp. 244–58, doi:<a href="https://doi.org/10.1007/978-3-642-40561-7_17">10.1007/978-3-642-40561-7_17</a>.
  short: 'D. Wonisch, A. Schremmer, H. Wehrheim, in: Proceedings of the 11th International
    Conference on Software Engineering and Formal Methods (SEFM), 2013, pp. 244–258.'
date_created: 2017-10-17T12:42:23Z
date_updated: 2022-01-06T07:01:18Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-40561-7_17
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-16T11:18:41Z
  date_updated: 2018-03-16T11:18:41Z
  file_id: '1332'
  file_name: 469-WSW2013-2.pdf
  file_size: 394804
  relation: main_file
  success: 1
file_date_updated: 2018-03-16T11:18:41Z
has_accepted_license: '1'
language:
- iso: eng
page: 244-258
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 11th International Conference on Software Engineering
  and Formal Methods (SEFM)
series_title: LNCS
status: public
title: Zero Overhead Runtime Monitoring
type: conference
user_id: '477'
year: '2013'
...
---
_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'
...
---
_id: '498'
abstract:
- lang: eng
  text: Proof-carrying code approaches aim at safe execution of untrusted code by
    having the code producer attach a safety proof to the code which the code consumer
    only has to validate. Depending on the type of safety property, proofs can however
    become quite large and their validation - though faster than their construction
    - still time consuming. In this paper we introduce a new concept for safe execution
    of untrusted code. It keeps the idea of putting the time consuming part of proving
    on the side of the code producer, however, attaches no proofs to code anymore
    but instead uses the proof to transform the program into an equivalent but more
    efficiently verifiable program. Code consumers thus still do proving themselves,
    however, on a computationally inexpensive level only. Experimental results show
    that the proof effort can be reduced by several orders of magnitude, both with
    respect to time and space.
author:
- first_name: Daniel
  full_name: Wonisch, Daniel
  last_name: Wonisch
- first_name: Alexander
  full_name: Schremmer, Alexander
  last_name: Schremmer
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Wonisch D, Schremmer A, Wehrheim H. Programs from Proofs – A PCC Alternative.
    In: <i>Proceedings of the 25th International Conference on Computer Aided Verification
    (CAV)</i>. LNCS. ; 2013:912-927. doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_65">10.1007/978-3-642-39799-8_65</a>'
  apa: Wonisch, D., Schremmer, A., &#38; Wehrheim, H. (2013). Programs from Proofs
    – A PCC Alternative. In <i>Proceedings of the 25th International Conference on
    Computer Aided Verification (CAV)</i> (pp. 912–927). <a href="https://doi.org/10.1007/978-3-642-39799-8_65">https://doi.org/10.1007/978-3-642-39799-8_65</a>
  bibtex: '@inproceedings{Wonisch_Schremmer_Wehrheim_2013, series={LNCS}, title={Programs
    from Proofs – A PCC Alternative}, DOI={<a href="https://doi.org/10.1007/978-3-642-39799-8_65">10.1007/978-3-642-39799-8_65</a>},
    booktitle={Proceedings of the 25th International Conference on Computer Aided
    Verification (CAV)}, author={Wonisch, Daniel and Schremmer, Alexander and Wehrheim,
    Heike}, year={2013}, pages={912–927}, collection={LNCS} }'
  chicago: Wonisch, Daniel, Alexander Schremmer, and Heike Wehrheim. “Programs from
    Proofs – A PCC Alternative.” In <i>Proceedings of the 25th International Conference
    on Computer Aided Verification (CAV)</i>, 912–27. LNCS, 2013. <a href="https://doi.org/10.1007/978-3-642-39799-8_65">https://doi.org/10.1007/978-3-642-39799-8_65</a>.
  ieee: D. Wonisch, A. Schremmer, and H. Wehrheim, “Programs from Proofs – A PCC Alternative,”
    in <i>Proceedings of the 25th International Conference on Computer Aided Verification
    (CAV)</i>, 2013, pp. 912–927.
  mla: Wonisch, Daniel, et al. “Programs from Proofs – A PCC Alternative.” <i>Proceedings
    of the 25th International Conference on Computer Aided Verification (CAV)</i>,
    2013, pp. 912–27, doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_65">10.1007/978-3-642-39799-8_65</a>.
  short: 'D. Wonisch, A. Schremmer, H. Wehrheim, in: Proceedings of the 25th International
    Conference on Computer Aided Verification (CAV), 2013, pp. 912–927.'
date_created: 2017-10-17T12:42:29Z
date_updated: 2022-01-06T07:01:32Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-39799-8_65
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T13:42:30Z
  date_updated: 2018-03-15T13:42:30Z
  file_id: '1313'
  file_name: 498-WonischSchremmerWehrheim2013.pdf
  file_size: 487617
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T13:42:30Z
has_accepted_license: '1'
language:
- iso: eng
page: 912-927
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 25th International Conference on Computer Aided Verification
  (CAV)
series_title: LNCS
status: public
title: Programs from Proofs – A PCC Alternative
type: conference
user_id: '477'
year: '2013'
...
---
_id: '586'
abstract:
- lang: eng
  text: FPGAs, systems on chip and embedded systems are nowadays irreplaceable. They
    combine the computational power of application specific hardware with software-like
    flexibility. At runtime, they can adjust their functionality by downloading new
    hardware modules and integrating their functionality. Due to their growing capabilities,
    the demands made to reconfigurable hardware grow. Their deployment in increasingly
    security critical scenarios requires new ways of enforcing security since a failure
    in security has severe consequences. Aside from financial losses, a loss of human
    life and risks to national security are possible. With this work I present the
    novel and groundbreaking concept of proof-carrying hardware. It is a method for
    the verification of properties of hardware modules to guarantee security for a
    target platform at runtime. The producer of a hardware module delivers based on
    the consumer's safety policy a safety proof in combination with the reconfiguration
    bitstream. The extensive computation of a proof is a contrast to the comparatively
    undemanding checking of the proof. I present a prototype based on open-source
    tools and an abstract FPGA architecture and bitstream format. The proof of the
    usability of proof-carrying hardware provides the evaluation of the prototype
    with the exemplary application of securing combinational and bounded sequential
    equivalence of reference monitor modules for memory safety.
- lang: ger
  text: FPGAs, System on Chips und eingebettete Systeme sind heutzutage kaum mehr
    wegzudenken. Sie kombinieren die Rechenleistung von spezialisierter Hardware mit
    einer Software-ähnlichen Flexibilität. Zur Laufzeit können sie ihre Funktionalität
    anpassen, indem sie online neue Hardware Module beziehen und deren Funktionalität
    integrieren. Mit der Leistung wachsen auch die Anforderungen an rekonfigurierbare
    Hardware. Ihr Einsatz in immer sicherheitskritischeren Szenarien erfordert neue
    Wege um Sicherheit zu gewährleisten, da ein Versagen der Sicherheit gravierende
    Folgen mit sich bringt. Neben finanziellen Verlusten sind auch der Verlust von
    Menschenleben oder Einbußen in der nationalen Sicherheit denkbar. In dieser Arbeit
    stelle ich das neue und wegweisende Konzept der beweistragenden Hardware vor.
    Es ist eine Methode zur Verifizierung von Eigenschaften von Hardware Modulen um
    die Sicherheit der Zielplatformen zur Laufzeit zu garantieren. Der Produzent eines
    Hardware Moduls liefert, basierend auf den Sicherheitsbestimmungen des Konsumenten,
    einen Beweis der Sicherheit mit dem Rekonfigurierungsbitstrom. Die aufwendige
    Berechnung des Beweises steht im Kontrast zu der vergleichsweise unaufwendigen
    Überprüfung durch den Konsumenten. Ich präsentiere einen Prototypen basierend
    auf Open Source Werkzeugen und einer eigenen abstrakten FPGA Architektur samt
    Bitstromformat. Den Nachweis über die Nutzbarkeit von beweistragender Hardware
    erbringt die Evaluierung des Prototypen zur beispielhaften Anwendung der Sicherung
    von kombinatorischer und begrenzt sequenzieller Äquivalenz von Referenzmonitor-Modulen
    zur Speichersicherheit.
author:
- first_name: Stephanie
  full_name: Drzevitzky, Stephanie
  last_name: Drzevitzky
citation:
  ama: 'Drzevitzky S. <i>Proof-Carrying Hardware: A Novel Approach to Reconfigurable
    Hardware Security</i>. Universität Paderborn; 2012.'
  apa: 'Drzevitzky, S. (2012). <i>Proof-Carrying Hardware: A Novel Approach to Reconfigurable
    Hardware Security</i>. Universität Paderborn.'
  bibtex: '@book{Drzevitzky_2012, title={Proof-Carrying Hardware: A Novel Approach
    to Reconfigurable Hardware Security}, publisher={Universität Paderborn}, author={Drzevitzky,
    Stephanie}, year={2012} }'
  chicago: 'Drzevitzky, Stephanie. <i>Proof-Carrying Hardware: A Novel Approach to
    Reconfigurable Hardware Security</i>. Universität Paderborn, 2012.'
  ieee: 'S. Drzevitzky, <i>Proof-Carrying Hardware: A Novel Approach to Reconfigurable
    Hardware Security</i>. Universität Paderborn, 2012.'
  mla: 'Drzevitzky, Stephanie. <i>Proof-Carrying Hardware: A Novel Approach to Reconfigurable
    Hardware Security</i>. Universität Paderborn, 2012.'
  short: 'S. Drzevitzky, Proof-Carrying Hardware: A Novel Approach to Reconfigurable
    Hardware Security, Universität Paderborn, 2012.'
date_created: 2017-10-17T12:42:46Z
date_updated: 2022-01-06T07:02:44Z
ddc:
- '040'
department:
- _id: '78'
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T08:38:19Z
  date_updated: 2018-03-15T08:38:19Z
  file_id: '1261'
  file_name: 586-Drzevitzky-PhD_01.pdf
  file_size: 1438436
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T08:38:19Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://nbn-resolving.de/urn:nbn:de:hbz:466:2-10423
oa: '1'
page: '114'
project:
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
publication_status: published
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
title: 'Proof-Carrying Hardware: A Novel Approach to Reconfigurable Hardware Security'
type: dissertation
user_id: '477'
year: '2012'
...
---
_id: '590'
abstract:
- lang: eng
  text: 'Predicate abstraction is an established technique for reducing the size of
    the state space during verification. In this paper, we extend predication abstraction
    with block-abstraction memoization (BAM), which exploits the fact that blocks
    are often executed several times in a program. The verification can thus benefit
    from caching the values of previous block analyses and reusing them upon next
    entry into a block. In addition to function bodies, BAM also performs well for
    nested loops. To further increase effectiveness, block memoization has been integrated
    with lazy abstraction adopting a lazy strategy for cache refinement. Together,
    this achieves significant performance increases: our tool (an implementation within
    the configurable program analysis framework CPAchecker) has won the Competition
    on Software Verification 2012 in the category “Overall”.'
author:
- first_name: Daniel
  full_name: Wonisch, Daniel
  last_name: Wonisch
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Wonisch D, Wehrheim H. Predicate Analysis with Block-Abstraction Memoization.
    In: <i>Proceedings of the 14th International Conference on Formal Engineering
    Methods (ICFEM)</i>. LNCS. ; 2012:332-347. doi:<a href="https://doi.org/10.1007/978-3-642-34281-3_24">10.1007/978-3-642-34281-3_24</a>'
  apa: Wonisch, D., &#38; Wehrheim, H. (2012). Predicate Analysis with Block-Abstraction
    Memoization. In <i>Proceedings of the 14th International Conference on Formal
    Engineering Methods (ICFEM)</i> (pp. 332–347). <a href="https://doi.org/10.1007/978-3-642-34281-3_24">https://doi.org/10.1007/978-3-642-34281-3_24</a>
  bibtex: '@inproceedings{Wonisch_Wehrheim_2012, series={LNCS}, title={Predicate Analysis
    with Block-Abstraction Memoization}, DOI={<a href="https://doi.org/10.1007/978-3-642-34281-3_24">10.1007/978-3-642-34281-3_24</a>},
    booktitle={Proceedings of the 14th International Conference on Formal Engineering
    Methods (ICFEM)}, author={Wonisch, Daniel and Wehrheim, Heike}, year={2012}, pages={332–347},
    collection={LNCS} }'
  chicago: Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction
    Memoization.” In <i>Proceedings of the 14th International Conference on Formal
    Engineering Methods (ICFEM)</i>, 332–47. LNCS, 2012. <a href="https://doi.org/10.1007/978-3-642-34281-3_24">https://doi.org/10.1007/978-3-642-34281-3_24</a>.
  ieee: D. Wonisch and H. Wehrheim, “Predicate Analysis with Block-Abstraction Memoization,”
    in <i>Proceedings of the 14th International Conference on Formal Engineering Methods
    (ICFEM)</i>, 2012, pp. 332–347.
  mla: Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction
    Memoization.” <i>Proceedings of the 14th International Conference on Formal Engineering
    Methods (ICFEM)</i>, 2012, pp. 332–47, doi:<a href="https://doi.org/10.1007/978-3-642-34281-3_24">10.1007/978-3-642-34281-3_24</a>.
  short: 'D. Wonisch, H. Wehrheim, in: Proceedings of the 14th International Conference
    on Formal Engineering Methods (ICFEM), 2012, pp. 332–347.'
date_created: 2017-10-17T12:42:47Z
date_updated: 2022-01-06T07:02:46Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-34281-3_24
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T08:33:56Z
  date_updated: 2018-03-15T08:33:56Z
  file_id: '1258'
  file_name: 590-WonischWehrheim2012.pdf
  file_size: 320901
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T08:33:56Z
has_accepted_license: '1'
language:
- iso: eng
page: 332-347
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 14th International Conference on Formal Engineering
  Methods (ICFEM)
series_title: LNCS
status: public
title: Predicate Analysis with Block-Abstraction Memoization
type: conference
user_id: '477'
year: '2012'
...
---
_id: '608'
abstract:
- lang: eng
  text: 'Predicate abstraction is an established technique in software verification.
    It inherently includes an abstraction refinement loop successively adding predicates
    until the right level of abstraction is found. For concurrent systems, predicate
    abstraction can be combined with spotlight abstraction, further reducing the state
    space by abstracting away certain processes. Refinement then has to decide whether
    to add a new predicate or a new process. Selecting the right predicates and processes
    is a crucial task: The positive effect of abstraction may be compromised by unfavourable
    refinement decisions. Here we present a heuristic approach to abstraction refinement.
    The basis for a decision is a set of refinement candidates, derived by multiple
    counterexample-generation. Candidates are evaluated with respect to their influence
    on other components in the system. Experimental results show that our technique
    can significantly speed up verification as compared to a naive abstraction refinement.'
author:
- first_name: Nils
  full_name: Timm, Nils
  last_name: Timm
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
- first_name: Mike
  full_name: Czech, Mike
  last_name: Czech
citation:
  ama: 'Timm N, Wehrheim H, Czech M. Heuristic-Guided Abstraction Refinement for Concurrent
    Systems. In: <i>Proceedings of the 14th International Conference on Formal Engineering
    Methods (ICFEM)</i>. LNCS. ; 2012:348-363. doi:<a href="https://doi.org/10.1007/978-3-642-34281-3_25">10.1007/978-3-642-34281-3_25</a>'
  apa: Timm, N., Wehrheim, H., &#38; Czech, M. (2012). Heuristic-Guided Abstraction
    Refinement for Concurrent Systems. In <i>Proceedings of the 14th International
    Conference on Formal Engineering Methods (ICFEM)</i> (pp. 348–363). <a href="https://doi.org/10.1007/978-3-642-34281-3_25">https://doi.org/10.1007/978-3-642-34281-3_25</a>
  bibtex: '@inproceedings{Timm_Wehrheim_Czech_2012, series={LNCS}, title={Heuristic-Guided
    Abstraction Refinement for Concurrent Systems}, DOI={<a href="https://doi.org/10.1007/978-3-642-34281-3_25">10.1007/978-3-642-34281-3_25</a>},
    booktitle={Proceedings of the 14th International Conference on Formal Engineering
    Methods (ICFEM)}, author={Timm, Nils and Wehrheim, Heike and Czech, Mike}, year={2012},
    pages={348–363}, collection={LNCS} }'
  chicago: Timm, Nils, Heike Wehrheim, and Mike Czech. “Heuristic-Guided Abstraction
    Refinement for Concurrent Systems.” In <i>Proceedings of the 14th International
    Conference on Formal Engineering Methods (ICFEM)</i>, 348–63. LNCS, 2012. <a href="https://doi.org/10.1007/978-3-642-34281-3_25">https://doi.org/10.1007/978-3-642-34281-3_25</a>.
  ieee: N. Timm, H. Wehrheim, and M. Czech, “Heuristic-Guided Abstraction Refinement
    for Concurrent Systems,” in <i>Proceedings of the 14th International Conference
    on Formal Engineering Methods (ICFEM)</i>, 2012, pp. 348–363.
  mla: Timm, Nils, et al. “Heuristic-Guided Abstraction Refinement for Concurrent
    Systems.” <i>Proceedings of the 14th International Conference on Formal Engineering
    Methods (ICFEM)</i>, 2012, pp. 348–63, doi:<a href="https://doi.org/10.1007/978-3-642-34281-3_25">10.1007/978-3-642-34281-3_25</a>.
  short: 'N. Timm, H. Wehrheim, M. Czech, in: Proceedings of the 14th International
    Conference on Formal Engineering Methods (ICFEM), 2012, pp. 348–363.'
date_created: 2017-10-17T12:42:50Z
date_updated: 2022-01-06T07:02:52Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-34281-3_25
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T08:15:33Z
  date_updated: 2018-03-15T08:15:33Z
  file_id: '1250'
  file_name: 608-Timm2013-0main.pdf
  file_size: 396337
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T08:15:33Z
has_accepted_license: '1'
language:
- iso: eng
page: 348-363
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 14th International Conference on Formal Engineering
  Methods (ICFEM)
series_title: LNCS
status: public
title: Heuristic-Guided Abstraction Refinement for Concurrent Systems
type: conference
user_id: '477'
year: '2012'
...
---
_id: '624'
author:
- first_name: Marie-Christine
  full_name: Jakobs, Marie-Christine
  last_name: Jakobs
citation:
  ama: Jakobs M-C. <i>Change and Validity Analysis in Deductive Program Verification</i>.
    Universität Paderborn; 2012.
  apa: Jakobs, M.-C. (2012). <i>Change and Validity Analysis in Deductive Program
    Verification</i>. Universität Paderborn.
  bibtex: '@book{Jakobs_2012, title={Change and Validity Analysis in Deductive Program
    Verification}, publisher={Universität Paderborn}, author={Jakobs, Marie-Christine},
    year={2012} }'
  chicago: Jakobs, Marie-Christine. <i>Change and Validity Analysis in Deductive Program
    Verification</i>. Universität Paderborn, 2012.
  ieee: M.-C. Jakobs, <i>Change and Validity Analysis in Deductive Program Verification</i>.
    Universität Paderborn, 2012.
  mla: Jakobs, Marie-Christine. <i>Change and Validity Analysis in Deductive Program
    Verification</i>. Universität Paderborn, 2012.
  short: M.-C. Jakobs, Change and Validity Analysis in Deductive Program Verification,
    Universität Paderborn, 2012.
date_created: 2017-10-17T12:42:53Z
date_updated: 2022-01-06T07:02:58Z
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
title: Change and Validity Analysis in Deductive Program Verification
type: mastersthesis
user_id: '15504'
year: '2012'
...
---
_id: '627'
abstract:
- lang: eng
  text: Block Abstraction Memoization (ABM) is a technique in software model checking
    that exploits the modularity of programs during verification by caching. To this
    end, ABM records the results of block analyses and reuses them if possible when
    revisiting the same block again. In this paper we present an implementation of
    ABM into the predicate-analysis component of the software-verification framework
    CPAchecker. With our participation at the Competition on Software Verification
    we aim at providing evidence that ABM can not only substantially increase the
    efficiency of predicate analysis but also enables verification of a wider range
    of programs.
author:
- first_name: Daniel
  full_name: Wonisch, Daniel
  last_name: Wonisch
citation:
  ama: 'Wonisch D. Block Abstraction Memoization for CPAchecker. In: <i>Proceedings
    of the 18th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems (TACAS)</i>. LNCS. ; 2012:531-533. doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_41">10.1007/978-3-642-28756-5_41</a>'
  apa: Wonisch, D. (2012). Block Abstraction Memoization for CPAchecker. In <i>Proceedings
    of the 18th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems (TACAS)</i> (pp. 531–533). <a href="https://doi.org/10.1007/978-3-642-28756-5_41">https://doi.org/10.1007/978-3-642-28756-5_41</a>
  bibtex: '@inproceedings{Wonisch_2012, series={LNCS}, title={Block Abstraction Memoization
    for CPAchecker}, DOI={<a href="https://doi.org/10.1007/978-3-642-28756-5_41">10.1007/978-3-642-28756-5_41</a>},
    booktitle={Proceedings of the 18th International Conference on Tools and Algorithms
    for the Construction and Analysis of Systems (TACAS)}, author={Wonisch, Daniel},
    year={2012}, pages={531–533}, collection={LNCS} }'
  chicago: Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” In <i>Proceedings
    of the 18th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems (TACAS)</i>, 531–33. LNCS, 2012. <a href="https://doi.org/10.1007/978-3-642-28756-5_41">https://doi.org/10.1007/978-3-642-28756-5_41</a>.
  ieee: D. Wonisch, “Block Abstraction Memoization for CPAchecker,” in <i>Proceedings
    of the 18th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems (TACAS)</i>, 2012, pp. 531–533.
  mla: Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” <i>Proceedings
    of the 18th International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems (TACAS)</i>, 2012, pp. 531–33, doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_41">10.1007/978-3-642-28756-5_41</a>.
  short: 'D. Wonisch, in: Proceedings of the 18th International Conference on Tools
    and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, pp.
    531–533.'
date_created: 2017-10-17T12:42:54Z
date_updated: 2022-01-06T07:02:59Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-28756-5_41
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T06:46:05Z
  date_updated: 2018-03-15T06:46:05Z
  file_id: '1242'
  file_name: 627-WonischSV-Comp2012_01.pdf
  file_size: 184000
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T06:46:05Z
has_accepted_license: '1'
language:
- iso: eng
page: 531-533
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 18th International Conference on Tools and Algorithms
  for the Construction and Analysis of Systems (TACAS)
series_title: LNCS
status: public
title: Block Abstraction Memoization for CPAchecker
type: conference
user_id: '477'
year: '2012'
...
---
_id: '5183'
author:
- first_name: Eric
  full_name: Bodden, Eric
  id: '59256'
  last_name: Bodden
  orcid: 0000-0003-3470-3647
- first_name: Patrick
  full_name: Lam, Patrick
  last_name: Lam
- first_name: Laurie
  full_name: Hendren, Laurie
  last_name: Hendren
citation:
  ama: Bodden E, Lam P, Hendren L. Partially Evaluating Finite-State Runtime Monitors
    Ahead of Time. <i>ACM Transactions on Programming Languages and Systems</i>. 2012;34(2):1-52.
    doi:<a href="https://doi.org/10.1145/2220365.2220366">10.1145/2220365.2220366</a>
  apa: Bodden, E., Lam, P., &#38; Hendren, L. (2012). Partially Evaluating Finite-State
    Runtime Monitors Ahead of Time. <i>ACM Transactions on Programming Languages and
    Systems</i>, <i>34</i>(2), 1–52. <a href="https://doi.org/10.1145/2220365.2220366">https://doi.org/10.1145/2220365.2220366</a>
  bibtex: '@article{Bodden_Lam_Hendren_2012, title={Partially Evaluating Finite-State
    Runtime Monitors Ahead of Time}, volume={34}, DOI={<a href="https://doi.org/10.1145/2220365.2220366">10.1145/2220365.2220366</a>},
    number={2}, journal={ACM Transactions on Programming Languages and Systems}, publisher={Association
    for Computing Machinery (ACM)}, author={Bodden, Eric and Lam, Patrick and Hendren,
    Laurie}, year={2012}, pages={1–52} }'
  chicago: 'Bodden, Eric, Patrick Lam, and Laurie Hendren. “Partially Evaluating Finite-State
    Runtime Monitors Ahead of Time.” <i>ACM Transactions on Programming Languages
    and Systems</i> 34, no. 2 (2012): 1–52. <a href="https://doi.org/10.1145/2220365.2220366">https://doi.org/10.1145/2220365.2220366</a>.'
  ieee: E. Bodden, P. Lam, and L. Hendren, “Partially Evaluating Finite-State Runtime
    Monitors Ahead of Time,” <i>ACM Transactions on Programming Languages and Systems</i>,
    vol. 34, no. 2, pp. 1–52, 2012.
  mla: Bodden, Eric, et al. “Partially Evaluating Finite-State Runtime Monitors Ahead
    of Time.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 34,
    no. 2, Association for Computing Machinery (ACM), 2012, pp. 1–52, doi:<a href="https://doi.org/10.1145/2220365.2220366">10.1145/2220365.2220366</a>.
  short: E. Bodden, P. Lam, L. Hendren, ACM Transactions on Programming Languages
    and Systems 34 (2012) 1–52.
date_created: 2018-10-31T10:43:13Z
date_updated: 2022-01-06T07:01:41Z
ddc:
- '000'
department:
- _id: '76'
doi: 10.1145/2220365.2220366
extern: '1'
file:
- access_level: closed
  content_type: application/pdf
  creator: ups
  date_created: 2018-11-02T15:42:24Z
  date_updated: 2018-11-02T15:42:24Z
  file_id: '5310'
  file_name: a7-bodden.pdf
  file_size: 2280938
  relation: main_file
  success: 1
file_date_updated: 2018-11-02T15:42:24Z
has_accepted_license: '1'
intvolume: '        34'
issue: '2'
language:
- iso: eng
main_file_link:
- url: http://www.bodden.de/pubs/blh12partially.pdf
page: 1-52
project:
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
- _id: '12'
  name: SFB 901 - Subproject B4
publication: ACM Transactions on Programming Languages and Systems
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: Association for Computing Machinery (ACM)
status: public
title: Partially Evaluating Finite-State Runtime Monitors Ahead of Time
type: journal_article
user_id: '477'
volume: 34
year: '2012'
...
---
_id: '647'
author:
- first_name: Michael
  full_name: Leuschel, Michael
  last_name: Leuschel
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: Leuschel M, Wehrheim H. Selected papers on Integrated Formal Methods (iFM09).
    <i>Science of Computer Programming</i>. 2011;(10):835--836. doi:<a href="https://doi.org/10.1016/j.scico.2011.01.009">10.1016/j.scico.2011.01.009</a>
  apa: Leuschel, M., &#38; Wehrheim, H. (2011). Selected papers on Integrated Formal
    Methods (iFM09). <i>Science of Computer Programming</i>, (10), 835--836. <a href="https://doi.org/10.1016/j.scico.2011.01.009">https://doi.org/10.1016/j.scico.2011.01.009</a>
  bibtex: '@article{Leuschel_Wehrheim_2011, title={Selected papers on Integrated Formal
    Methods (iFM09)}, DOI={<a href="https://doi.org/10.1016/j.scico.2011.01.009">10.1016/j.scico.2011.01.009</a>},
    number={10}, journal={Science of Computer Programming}, publisher={Elsevier},
    author={Leuschel, Michael and Wehrheim, Heike}, year={2011}, pages={835--836}
    }'
  chicago: 'Leuschel, Michael, and Heike Wehrheim. “Selected Papers on Integrated
    Formal Methods (IFM09).” <i>Science of Computer Programming</i>, no. 10 (2011):
    835--836. <a href="https://doi.org/10.1016/j.scico.2011.01.009">https://doi.org/10.1016/j.scico.2011.01.009</a>.'
  ieee: M. Leuschel and H. Wehrheim, “Selected papers on Integrated Formal Methods
    (iFM09),” <i>Science of Computer Programming</i>, no. 10, pp. 835--836, 2011.
  mla: Leuschel, Michael, and Heike Wehrheim. “Selected Papers on Integrated Formal
    Methods (IFM09).” <i>Science of Computer Programming</i>, no. 10, Elsevier, 2011,
    pp. 835--836, doi:<a href="https://doi.org/10.1016/j.scico.2011.01.009">10.1016/j.scico.2011.01.009</a>.
  short: M. Leuschel, H. Wehrheim, Science of Computer Programming (2011) 835--836.
date_created: 2017-10-17T12:42:58Z
date_updated: 2022-01-06T07:03:06Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1016/j.scico.2011.01.009
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-14T13:56:48Z
  date_updated: 2018-03-14T13:56:48Z
  file_id: '1226'
  file_name: 647-LeuschelWehrheim.pdf
  file_size: 139105
  relation: main_file
  success: 1
file_date_updated: 2018-03-14T13:56:48Z
has_accepted_license: '1'
issue: '10'
language:
- iso: eng
page: 835--836
project:
- _id: '1'
  name: SFB 901
- _id: '11'
  name: SFB 901 - Subprojekt B3
- _id: '12'
  name: SFB 901 - Subproject B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Science of Computer Programming
publisher: Elsevier
status: public
title: Selected papers on Integrated Formal Methods (iFM09)
type: journal_article
user_id: '477'
year: '2011'
...
---
_id: '658'
author:
- first_name: Alexander
  full_name: Schremmer, Alexander
  last_name: Schremmer
citation:
  ama: Schremmer A. <i>Function Specification Inference Using Craig Interpolation</i>.
    Universität Paderborn; 2011.
  apa: Schremmer, A. (2011). <i>Function Specification Inference Using Craig Interpolation</i>.
    Universität Paderborn.
  bibtex: '@book{Schremmer_2011, title={Function Specification Inference Using Craig
    Interpolation}, publisher={Universität Paderborn}, author={Schremmer, Alexander},
    year={2011} }'
  chicago: Schremmer, Alexander. <i>Function Specification Inference Using Craig Interpolation</i>.
    Universität Paderborn, 2011.
  ieee: A. Schremmer, <i>Function Specification Inference Using Craig Interpolation</i>.
    Universität Paderborn, 2011.
  mla: Schremmer, Alexander. <i>Function Specification Inference Using Craig Interpolation</i>.
    Universität Paderborn, 2011.
  short: A. Schremmer, Function Specification Inference Using Craig Interpolation,
    Universität Paderborn, 2011.
date_created: 2017-10-17T12:43:00Z
date_updated: 2022-01-06T07:03:12Z
department:
- _id: '77'
language:
- iso: eng
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: Function Specification Inference Using Craig Interpolation
type: mastersthesis
user_id: '477'
year: '2011'
...
---
_id: '666'
abstract:
- lang: eng
  text: Reconfigurable systems on chip are increasingly deployed in security and safety
    critical contexts. When downloading and configuring new hardware functions, we
    want to make sure that modules adhere to certain security specifications and do
    not, for example, contain hardware Trojans. As a possible approach to achieving
    hardware security we propose and demonstrate the concept of proof-carrying hardware,
    a concept inspired by previous work on proof-carrying code techniques in the software
    domain. In this paper, we discuss the hardware trust and threat models behind
    proof-carrying hardware and then present our experimental setup. We detail the
    employed open-source tool chain for the runtime verification of combinational equivalence
    and our bitstream format for an abstract FPGA architecture that allows us to experimentally
    validate the feasibility of our approach.
author:
- first_name: Stephanie
  full_name: Drzevitzky, Stephanie
  last_name: Drzevitzky
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
citation:
  ama: 'Drzevitzky S, Platzner M. Achieving Hardware Security for Reconfigurable Systems
    on Chip by a Proof-Carrying Code Approach. In: <i>Proceedings of the 6th International
    Workshop on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC)</i>.
    ; 2011:58-65. doi:<a href="https://doi.org/10.1109/ReCoSoC.2011.5981499">10.1109/ReCoSoC.2011.5981499</a>'
  apa: Drzevitzky, S., &#38; Platzner, M. (2011). Achieving Hardware Security for
    Reconfigurable Systems on Chip by a Proof-Carrying Code Approach. In <i>Proceedings
    of the 6th International Workshop on Reconfigurable Communication-centric Systems-on-Chip
    (ReCoSoC)</i> (pp. 58–65). <a href="https://doi.org/10.1109/ReCoSoC.2011.5981499">https://doi.org/10.1109/ReCoSoC.2011.5981499</a>
  bibtex: '@inproceedings{Drzevitzky_Platzner_2011, title={Achieving Hardware Security
    for Reconfigurable Systems on Chip by a Proof-Carrying Code Approach}, DOI={<a
    href="https://doi.org/10.1109/ReCoSoC.2011.5981499">10.1109/ReCoSoC.2011.5981499</a>},
    booktitle={Proceedings of the 6th International Workshop on Reconfigurable Communication-centric
    Systems-on-Chip (ReCoSoC)}, author={Drzevitzky, Stephanie and Platzner, Marco},
    year={2011}, pages={58–65} }'
  chicago: Drzevitzky, Stephanie, and Marco Platzner. “Achieving Hardware Security
    for Reconfigurable Systems on Chip by a Proof-Carrying Code Approach.” In <i>Proceedings
    of the 6th International Workshop on Reconfigurable Communication-Centric Systems-on-Chip
    (ReCoSoC)</i>, 58–65, 2011. <a href="https://doi.org/10.1109/ReCoSoC.2011.5981499">https://doi.org/10.1109/ReCoSoC.2011.5981499</a>.
  ieee: S. Drzevitzky and M. Platzner, “Achieving Hardware Security for Reconfigurable
    Systems on Chip by a Proof-Carrying Code Approach,” in <i>Proceedings of the 6th
    International Workshop on Reconfigurable Communication-centric Systems-on-Chip
    (ReCoSoC)</i>, 2011, pp. 58–65.
  mla: Drzevitzky, Stephanie, and Marco Platzner. “Achieving Hardware Security for
    Reconfigurable Systems on Chip by a Proof-Carrying Code Approach.” <i>Proceedings
    of the 6th International Workshop on Reconfigurable Communication-Centric Systems-on-Chip
    (ReCoSoC)</i>, 2011, pp. 58–65, doi:<a href="https://doi.org/10.1109/ReCoSoC.2011.5981499">10.1109/ReCoSoC.2011.5981499</a>.
  short: 'S. Drzevitzky, M. Platzner, in: Proceedings of the 6th International Workshop
    on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC), 2011, pp. 58–65.'
date_created: 2017-10-17T12:43:01Z
date_updated: 2022-01-06T07:03:14Z
ddc:
- '040'
department:
- _id: '78'
doi: 10.1109/ReCoSoC.2011.5981499
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-14T13:40:48Z
  date_updated: 2018-03-14T13:40:48Z
  file_id: '1214'
  file_name: 666-drzevitzky11_recosoc.pdf
  file_size: 666039
  relation: main_file
  success: 1
file_date_updated: 2018-03-14T13:40:48Z
has_accepted_license: '1'
language:
- iso: eng
page: 58-65
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 6th International Workshop on Reconfigurable Communication-centric
  Systems-on-Chip (ReCoSoC)
status: public
title: Achieving Hardware Security for Reconfigurable Systems on Chip by a Proof-Carrying
  Code Approach
type: conference
user_id: '477'
year: '2011'
...