---
_id: '408'
abstract:
- lang: eng
  text: Verification of hardware and software usually proceeds separately, software
    analysis relying on the correctness of processors executing instructions. This
    assumption is valid as long as the software runs on standard CPUs that have been
    extensively validated and are in wide use. However, for processors exploiting
    custom instruction set extensions to meet performance and energy constraints the
    validation might be less extensive, challenging the correctness assumption.In
    this paper we present an approach for integrating software analyses with hardware
    verification, specifically targeting custom instruction set extensions. We propose
    three different techniques for deriving the properties to be proven for the hardware
    implementation of a custom instruction in order to support software analyses.
    The techniques are designed to explore the trade-off between generality and efficiency
    and span from proving functional equivalence over checking the rules of a particular
    analysis domain to verifying actual pre and post conditions resulting from program
    analysis. We demonstrate and compare the three techniques on example programs
    with custom instructions, using stateof-the-art software and hardware verification
    techniques.
author:
- first_name: Marie-Christine
  full_name: Jakobs, Marie-Christine
  last_name: Jakobs
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
- first_name: Tobias
  full_name: Wiersema, Tobias
  id: '3118'
  last_name: Wiersema
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Jakobs M-C, Platzner M, Wiersema T, Wehrheim H. Integrating Software and Hardware
    Verification. In: Albert E, Sekerinski E, eds. <i>Proceedings of the 11th International
    Conference on Integrated Formal Methods (IFM)</i>. LNCS. ; 2014:307-322. doi:<a
    href="https://doi.org/10.1007/978-3-319-10181-1_19">10.1007/978-3-319-10181-1_19</a>'
  apa: Jakobs, M.-C., Platzner, M., Wiersema, T., &#38; Wehrheim, H. (2014). Integrating
    Software and Hardware Verification. In E. Albert &#38; E. Sekerinski (Eds.), <i>Proceedings
    of the 11th International Conference on Integrated Formal Methods (iFM)</i> (pp.
    307–322). <a href="https://doi.org/10.1007/978-3-319-10181-1_19">https://doi.org/10.1007/978-3-319-10181-1_19</a>
  bibtex: '@inproceedings{Jakobs_Platzner_Wiersema_Wehrheim_2014, series={LNCS}, title={Integrating
    Software and Hardware Verification}, DOI={<a href="https://doi.org/10.1007/978-3-319-10181-1_19">10.1007/978-3-319-10181-1_19</a>},
    booktitle={Proceedings of the 11th International Conference on Integrated Formal
    Methods (iFM)}, author={Jakobs, Marie-Christine and Platzner, Marco and Wiersema,
    Tobias and Wehrheim, Heike}, editor={Albert, Elvira and Sekerinski, EmilEditors},
    year={2014}, pages={307–322}, collection={LNCS} }'
  chicago: Jakobs, Marie-Christine, Marco Platzner, Tobias Wiersema, and Heike Wehrheim.
    “Integrating Software and Hardware Verification.” In <i>Proceedings of the 11th
    International Conference on Integrated Formal Methods (IFM)</i>, edited by Elvira
    Albert and Emil Sekerinski, 307–22. LNCS, 2014. <a href="https://doi.org/10.1007/978-3-319-10181-1_19">https://doi.org/10.1007/978-3-319-10181-1_19</a>.
  ieee: M.-C. Jakobs, M. Platzner, T. Wiersema, and H. Wehrheim, “Integrating Software
    and Hardware Verification,” in <i>Proceedings of the 11th International Conference
    on Integrated Formal Methods (iFM)</i>, 2014, pp. 307–322.
  mla: Jakobs, Marie-Christine, et al. “Integrating Software and Hardware Verification.”
    <i>Proceedings of the 11th International Conference on Integrated Formal Methods
    (IFM)</i>, edited by Elvira Albert and Emil Sekerinski, 2014, pp. 307–22, doi:<a
    href="https://doi.org/10.1007/978-3-319-10181-1_19">10.1007/978-3-319-10181-1_19</a>.
  short: 'M.-C. Jakobs, M. Platzner, T. Wiersema, H. Wehrheim, in: E. Albert, E. Sekerinski
    (Eds.), Proceedings of the 11th International Conference on Integrated Formal
    Methods (IFM), 2014, pp. 307–322.'
date_created: 2017-10-17T12:42:11Z
date_updated: 2022-01-06T07:00:14Z
ddc:
- '040'
department:
- _id: '77'
- _id: '78'
doi: 10.1007/978-3-319-10181-1_19
editor:
- first_name: Elvira
  full_name: Albert, Elvira
  last_name: Albert
- first_name: Emil
  full_name: Sekerinski, Emil
  last_name: Sekerinski
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-16T11:35:28Z
  date_updated: 2018-03-16T11:35:28Z
  file_id: '1364'
  file_name: 408-jakobs14_ifm.pdf
  file_size: 561325
  relation: main_file
  success: 1
file_date_updated: 2018-03-16T11:35:28Z
has_accepted_license: '1'
language:
- iso: eng
page: 307-322
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 Integrated Formal
  Methods (iFM)
series_title: LNCS
status: public
title: Integrating Software and Hardware Verification
type: conference
user_id: '477'
year: '2014'
...
---
_id: '417'
abstract:
- lang: eng
  text: 'Model transformation is a key concept in modeldrivensoftware engineering.
    The definition of model transformationsis usually based on meta-models describing
    the abstractsyntax of languages. While meta-models are thereby able to abstractfrom
    superfluous details of concrete syntax, they often loosestructural information
    inherent in languages, like information onmodel elements always occurring together
    in particular shapes.As a consequence, model transformations cannot naturally
    re-uselanguage structures, thus leading to unnecessary complexity intheir development
    as well as analysis.In this paper, we propose a new approach to model transformationdevelopment
    which allows to simplify and improve thequality of the developed transformations
    via the exploitation ofthe languages’ structures. The approach is based on context-freegrammars
    and transformations defined by pairing productions ofsource and target grammars.
    We show that such transformationsexhibit three important characteristics: they
    are sound, completeand deterministic.'
author:
- first_name: Galina
  full_name: Besova, Galina
  last_name: Besova
- first_name: Dominik
  full_name: Steenke, Dominik
  last_name: Steenke
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Besova G, Steenke D, Wehrheim H. Grammar-based model transformations. In:
    <i>Proceedings 3rd Workshop on Model Driven Approaches in System Development (MDASD)</i>.
    ; 2014:1601-1610. doi:<a href="https://doi.org/10.1016/j.cl.2015.05.003">10.1016/j.cl.2015.05.003</a>'
  apa: Besova, G., Steenke, D., &#38; Wehrheim, H. (2014). Grammar-based model transformations.
    In <i>Proceedings 3rd Workshop on Model Driven Approaches in System Development
    (MDASD)</i> (pp. 1601–1610). <a href="https://doi.org/10.1016/j.cl.2015.05.003">https://doi.org/10.1016/j.cl.2015.05.003</a>
  bibtex: '@inproceedings{Besova_Steenke_Wehrheim_2014, title={Grammar-based model
    transformations}, DOI={<a href="https://doi.org/10.1016/j.cl.2015.05.003">10.1016/j.cl.2015.05.003</a>},
    booktitle={Proceedings 3rd Workshop on Model Driven Approaches in System Development
    (MDASD)}, author={Besova, Galina and Steenke, Dominik and Wehrheim, Heike}, year={2014},
    pages={1601–1610} }'
  chicago: Besova, Galina, Dominik Steenke, and Heike Wehrheim. “Grammar-Based Model
    Transformations.” In <i>Proceedings 3rd Workshop on Model Driven Approaches in
    System Development (MDASD)</i>, 1601–10, 2014. <a href="https://doi.org/10.1016/j.cl.2015.05.003">https://doi.org/10.1016/j.cl.2015.05.003</a>.
  ieee: G. Besova, D. Steenke, and H. Wehrheim, “Grammar-based model transformations,”
    in <i>Proceedings 3rd Workshop on Model Driven Approaches in System Development
    (MDASD)</i>, 2014, pp. 1601–1610.
  mla: Besova, Galina, et al. “Grammar-Based Model Transformations.” <i>Proceedings
    3rd Workshop on Model Driven Approaches in System Development (MDASD)</i>, 2014,
    pp. 1601–10, doi:<a href="https://doi.org/10.1016/j.cl.2015.05.003">10.1016/j.cl.2015.05.003</a>.
  short: 'G. Besova, D. Steenke, H. Wehrheim, in: Proceedings 3rd Workshop on Model
    Driven Approaches in System Development (MDASD), 2014, pp. 1601–1610.'
date_created: 2017-10-17T12:42:13Z
date_updated: 2022-01-06T07:00:28Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1016/j.cl.2015.05.003
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-16T11:33:33Z
  date_updated: 2018-03-16T11:33:33Z
  file_id: '1360'
  file_name: 417-main.pdf
  file_size: 643382
  relation: main_file
  success: 1
file_date_updated: 2018-03-16T11:33:33Z
has_accepted_license: '1'
language:
- iso: eng
page: 1601-1610
project:
- _id: '1'
  name: SFB 901
- _id: '11'
  name: SFB 901 - Subprojekt B3
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings 3rd Workshop on Model Driven Approaches in System Development
  (MDASD)
status: public
title: Grammar-based model transformations
type: conference
user_id: '477'
year: '2014'
...
---
_id: '418'
author:
- first_name: Felix
  full_name: Pauck, Felix
  id: '22398'
  last_name: Pauck
citation:
  ama: Pauck F. <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>.
    Universität Paderborn; 2014.
  apa: Pauck, F. (2014). <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>.
    Universität Paderborn.
  bibtex: '@book{Pauck_2014, title={Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren},
    publisher={Universität Paderborn}, author={Pauck, Felix}, year={2014} }'
  chicago: Pauck, Felix. <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>.
    Universität Paderborn, 2014.
  ieee: F. Pauck, <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>.
    Universität Paderborn, 2014.
  mla: Pauck, Felix. <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>.
    Universität Paderborn, 2014.
  short: F. Pauck, Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren,
    Universität Paderborn, 2014.
date_created: 2017-10-17T12:42:13Z
date_updated: 2022-01-06T07:00:30Z
ddc:
- '000'
department:
- _id: '77'
file:
- access_level: open_access
  content_type: application/pdf
  creator: fpauck
  date_created: 2019-08-07T09:00:20Z
  date_updated: 2019-08-07T09:05:38Z
  file_id: '12906'
  file_name: fpauck_2014.pdf
  file_size: 3191756
  relation: main_file
  title: Bachelorarbeit
file_date_updated: 2019-08-07T09:05:38Z
has_accepted_license: '1'
language:
- iso: ger
oa: '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: Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren
type: bachelorsthesis
user_id: '22398'
year: '2014'
...
---
_id: '3176'
author:
- first_name: Tobias
  full_name: Isenberg, Tobias
  last_name: Isenberg
- first_name: Dominik
  full_name: Steenken, Dominik
  last_name: Steenken
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Isenberg T, Steenken D, Wehrheim H. Bounded Model Checking of Graph Transformation
    Systems via {SMT} Solving. In: Beyer D, Boreale M, eds. <i>Formal Techniques for
    Distributed Systems - Joint {IFIP} {WG} 6.1 International Conference, {FMOODS/FORTE}
    2013, Held as Part of the 8th International Federated Conference on Distributed
    Computing Techniques, DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings</i>.
    Lecture Notes in Computer Science. ; 2013:178--192. doi:<a href="https://doi.org/10.1007/978-3-642-38592-6_13">10.1007/978-3-642-38592-6_13</a>'
  apa: Isenberg, T., Steenken, D., &#38; Wehrheim, H. (2013). Bounded Model Checking
    of Graph Transformation Systems via {SMT} Solving. In D. Beyer &#38; M. Boreale
    (Eds.), <i>Formal Techniques for Distributed Systems - Joint {IFIP} {WG} 6.1 International
    Conference, {FMOODS/FORTE} 2013, Held as Part of the 8th International Federated
    Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy,
    June 3-5, 2013. Proceedings</i> (pp. 178--192). <a href="https://doi.org/10.1007/978-3-642-38592-6_13">https://doi.org/10.1007/978-3-642-38592-6_13</a>
  bibtex: '@inproceedings{Isenberg_Steenken_Wehrheim_2013, series={Lecture Notes in
    Computer Science}, title={Bounded Model Checking of Graph Transformation Systems
    via {SMT} Solving}, DOI={<a href="https://doi.org/10.1007/978-3-642-38592-6_13">10.1007/978-3-642-38592-6_13</a>},
    booktitle={Formal Techniques for Distributed Systems - Joint {IFIP} {WG} 6.1 International
    Conference, {FMOODS/FORTE} 2013, Held as Part of the 8th International Federated
    Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy,
    June 3-5, 2013. Proceedings}, author={Isenberg, Tobias and Steenken, Dominik and
    Wehrheim, Heike}, editor={Beyer, Dirk and Boreale, MicheleEditors}, year={2013},
    pages={178--192}, collection={Lecture Notes in Computer Science} }'
  chicago: Isenberg, Tobias, Dominik Steenken, and Heike Wehrheim. “Bounded Model
    Checking of Graph Transformation Systems via {SMT} Solving.” In <i>Formal Techniques
    for Distributed Systems - Joint {IFIP} {WG} 6.1 International Conference, {FMOODS/FORTE}
    2013, Held as Part of the 8th International Federated Conference on Distributed
    Computing Techniques, DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings</i>,
    edited by Dirk Beyer and Michele Boreale, 178--192. Lecture Notes in Computer
    Science, 2013. <a href="https://doi.org/10.1007/978-3-642-38592-6_13">https://doi.org/10.1007/978-3-642-38592-6_13</a>.
  ieee: T. Isenberg, D. Steenken, and H. Wehrheim, “Bounded Model Checking of Graph
    Transformation Systems via {SMT} Solving,” in <i>Formal Techniques for Distributed
    Systems - Joint {IFIP} {WG} 6.1 International Conference, {FMOODS/FORTE} 2013,
    Held as Part of the 8th International Federated Conference on Distributed Computing
    Techniques, DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings</i>, 2013,
    pp. 178--192.
  mla: Isenberg, Tobias, et al. “Bounded Model Checking of Graph Transformation Systems
    via {SMT} Solving.” <i>Formal Techniques for Distributed Systems - Joint {IFIP}
    {WG} 6.1 International Conference, {FMOODS/FORTE} 2013, Held as Part of the 8th
    International Federated Conference on Distributed Computing Techniques, DisCoTec
    2013, Florence, Italy, June 3-5, 2013. Proceedings</i>, edited by Dirk Beyer and
    Michele Boreale, 2013, pp. 178--192, doi:<a href="https://doi.org/10.1007/978-3-642-38592-6_13">10.1007/978-3-642-38592-6_13</a>.
  short: 'T. Isenberg, D. Steenken, H. Wehrheim, in: D. Beyer, M. Boreale (Eds.),
    Formal Techniques for Distributed Systems - Joint {IFIP} {WG} 6.1 International
    Conference, {FMOODS/FORTE} 2013, Held as Part of the 8th International Federated
    Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy,
    June 3-5, 2013. Proceedings, 2013, pp. 178--192.'
date_created: 2018-06-13T08:08:39Z
date_updated: 2022-01-06T06:59:02Z
department:
- _id: '77'
doi: 10.1007/978-3-642-38592-6_13
editor:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Michele
  full_name: Boreale, Michele
  last_name: Boreale
page: 178--192
publication: Formal Techniques for Distributed Systems - Joint {IFIP} {WG} 6.1 International
  Conference, {FMOODS/FORTE} 2013, Held as Part of the 8th International Federated
  Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy,
  June 3-5, 2013. Proceedings
series_title: Lecture Notes in Computer Science
status: public
title: Bounded Model Checking of Graph Transformation Systems via {SMT} Solving
type: conference
user_id: '29719'
year: '2013'
...
---
_id: '3177'
author:
- first_name: Oleg
  full_name: Travkin, Oleg
  last_name: Travkin
- first_name: Annika
  full_name: Mütze, Annika
  last_name: Mütze
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Travkin O, Mütze A, Wehrheim H. {SPIN} as a Linearizability Checker under
    Weak Memory Models. In: Bertacco V, Legay A, eds. <i>Hardware and Software: Verification
    and Testing - 9th International Haifa Verification Conference, {HVC} 2013, Haifa,
    Israel, November 5-7, 2013, Proceedings</i>. Lecture Notes in Computer Science.
    ; 2013:311--326. doi:<a href="https://doi.org/10.1007/978-3-319-03077-7_21">10.1007/978-3-319-03077-7_21</a>'
  apa: 'Travkin, O., Mütze, A., &#38; Wehrheim, H. (2013). {SPIN} as a Linearizability
    Checker under Weak Memory Models. In V. Bertacco &#38; A. Legay (Eds.), <i>Hardware
    and Software: Verification and Testing - 9th International Haifa Verification
    Conference, {HVC} 2013, Haifa, Israel, November 5-7, 2013, Proceedings</i> (pp.
    311--326). <a href="https://doi.org/10.1007/978-3-319-03077-7_21">https://doi.org/10.1007/978-3-319-03077-7_21</a>'
  bibtex: '@inproceedings{Travkin_Mütze_Wehrheim_2013, series={Lecture Notes in Computer
    Science}, title={{SPIN} as a Linearizability Checker under Weak Memory Models},
    DOI={<a href="https://doi.org/10.1007/978-3-319-03077-7_21">10.1007/978-3-319-03077-7_21</a>},
    booktitle={Hardware and Software: Verification and Testing - 9th International
    Haifa Verification Conference, {HVC} 2013, Haifa, Israel, November 5-7, 2013,
    Proceedings}, author={Travkin, Oleg and Mütze, Annika and Wehrheim, Heike}, editor={Bertacco,
    Valeria and Legay, AxelEditors}, year={2013}, pages={311--326}, collection={Lecture
    Notes in Computer Science} }'
  chicago: 'Travkin, Oleg, Annika Mütze, and Heike Wehrheim. “{SPIN} as a Linearizability
    Checker under Weak Memory Models.” In <i>Hardware and Software: Verification and
    Testing - 9th International Haifa Verification Conference, {HVC} 2013, Haifa,
    Israel, November 5-7, 2013, Proceedings</i>, edited by Valeria Bertacco and Axel
    Legay, 311--326. Lecture Notes in Computer Science, 2013. <a href="https://doi.org/10.1007/978-3-319-03077-7_21">https://doi.org/10.1007/978-3-319-03077-7_21</a>.'
  ieee: 'O. Travkin, A. Mütze, and H. Wehrheim, “{SPIN} as a Linearizability Checker
    under Weak Memory Models,” in <i>Hardware and Software: Verification and Testing
    - 9th International Haifa Verification Conference, {HVC} 2013, Haifa, Israel,
    November 5-7, 2013, Proceedings</i>, 2013, pp. 311--326.'
  mla: 'Travkin, Oleg, et al. “{SPIN} as a Linearizability Checker under Weak Memory
    Models.” <i>Hardware and Software: Verification and Testing - 9th International
    Haifa Verification Conference, {HVC} 2013, Haifa, Israel, November 5-7, 2013,
    Proceedings</i>, edited by Valeria Bertacco and Axel Legay, 2013, pp. 311--326,
    doi:<a href="https://doi.org/10.1007/978-3-319-03077-7_21">10.1007/978-3-319-03077-7_21</a>.'
  short: 'O. Travkin, A. Mütze, H. Wehrheim, in: V. Bertacco, A. Legay (Eds.), Hardware
    and Software: Verification and Testing - 9th International Haifa Verification
    Conference, {HVC} 2013, Haifa, Israel, November 5-7, 2013, Proceedings, 2013,
    pp. 311--326.'
date_created: 2018-06-13T08:09:44Z
date_updated: 2022-01-06T06:59:02Z
department:
- _id: '77'
doi: 10.1007/978-3-319-03077-7_21
editor:
- first_name: Valeria
  full_name: Bertacco, Valeria
  last_name: Bertacco
- first_name: Axel
  full_name: Legay, Axel
  last_name: Legay
page: 311--326
publication: 'Hardware and Software: Verification and Testing - 9th International
  Haifa Verification Conference, {HVC} 2013, Haifa, Israel, November 5-7, 2013, Proceedings'
series_title: Lecture Notes in Computer Science
status: public
title: '{SPIN} as a Linearizability Checker under Weak Memory Models'
type: conference
user_id: '29719'
year: '2013'
...
---
_id: '3178'
author:
- first_name: Brijesh
  full_name: Dongol, Brijesh
  last_name: Dongol
- first_name: Oleg
  full_name: Travkin, Oleg
  last_name: Travkin
- first_name: John
  full_name: Derrick, John
  last_name: Derrick
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Dongol B, Travkin O, Derrick J, Wehrheim H. A High-Level Semantics for Program
    Execution under Total Store Order Memory. In: Liu Z, Woodcock J, Zhu H, eds. <i>Theoretical
    Aspects of Computing - {ICTAC} 2013 - 10th International Colloquium, Shanghai,
    China, September 4-6, 2013. Proceedings</i>. Lecture Notes in Computer Science.
    ; 2013:177--194. doi:<a href="https://doi.org/10.1007/978-3-642-39718-9_11">10.1007/978-3-642-39718-9_11</a>'
  apa: Dongol, B., Travkin, O., Derrick, J., &#38; Wehrheim, H. (2013). A High-Level
    Semantics for Program Execution under Total Store Order Memory. In Z. Liu, J.
    Woodcock, &#38; H. Zhu (Eds.), <i>Theoretical Aspects of Computing - {ICTAC} 2013
    - 10th International Colloquium, Shanghai, China, September 4-6, 2013. Proceedings</i>
    (pp. 177--194). <a href="https://doi.org/10.1007/978-3-642-39718-9_11">https://doi.org/10.1007/978-3-642-39718-9_11</a>
  bibtex: '@inproceedings{Dongol_Travkin_Derrick_Wehrheim_2013, series={Lecture Notes
    in Computer Science}, title={A High-Level Semantics for Program Execution under
    Total Store Order Memory}, DOI={<a href="https://doi.org/10.1007/978-3-642-39718-9_11">10.1007/978-3-642-39718-9_11</a>},
    booktitle={Theoretical Aspects of Computing - {ICTAC} 2013 - 10th International
    Colloquium, Shanghai, China, September 4-6, 2013. Proceedings}, author={Dongol,
    Brijesh and Travkin, Oleg and Derrick, John and Wehrheim, Heike}, editor={Liu,
    Zhiming and Woodcock, Jim and Zhu, HuibiaoEditors}, year={2013}, pages={177--194},
    collection={Lecture Notes in Computer Science} }'
  chicago: Dongol, Brijesh, Oleg Travkin, John Derrick, and Heike Wehrheim. “A High-Level
    Semantics for Program Execution under Total Store Order Memory.” In <i>Theoretical
    Aspects of Computing - {ICTAC} 2013 - 10th International Colloquium, Shanghai,
    China, September 4-6, 2013. Proceedings</i>, edited by Zhiming Liu, Jim Woodcock,
    and Huibiao Zhu, 177--194. Lecture Notes in Computer Science, 2013. <a href="https://doi.org/10.1007/978-3-642-39718-9_11">https://doi.org/10.1007/978-3-642-39718-9_11</a>.
  ieee: B. Dongol, O. Travkin, J. Derrick, and H. Wehrheim, “A High-Level Semantics
    for Program Execution under Total Store Order Memory,” in <i>Theoretical Aspects
    of Computing - {ICTAC} 2013 - 10th International Colloquium, Shanghai, China,
    September 4-6, 2013. Proceedings</i>, 2013, pp. 177--194.
  mla: Dongol, Brijesh, et al. “A High-Level Semantics for Program Execution under
    Total Store Order Memory.” <i>Theoretical Aspects of Computing - {ICTAC} 2013
    - 10th International Colloquium, Shanghai, China, September 4-6, 2013. Proceedings</i>,
    edited by Zhiming Liu et al., 2013, pp. 177--194, doi:<a href="https://doi.org/10.1007/978-3-642-39718-9_11">10.1007/978-3-642-39718-9_11</a>.
  short: 'B. Dongol, O. Travkin, J. Derrick, H. Wehrheim, in: Z. Liu, J. Woodcock,
    H. Zhu (Eds.), Theoretical Aspects of Computing - {ICTAC} 2013 - 10th International
    Colloquium, Shanghai, China, September 4-6, 2013. Proceedings, 2013, pp. 177--194.'
date_created: 2018-06-13T08:13:31Z
date_updated: 2022-01-06T06:59:02Z
department:
- _id: '77'
doi: 10.1007/978-3-642-39718-9_11
editor:
- first_name: Zhiming
  full_name: Liu, Zhiming
  last_name: Liu
- first_name: Jim
  full_name: Woodcock, Jim
  last_name: Woodcock
- first_name: Huibiao
  full_name: Zhu, Huibiao
  last_name: Zhu
page: 177--194
publication: Theoretical Aspects of Computing - {ICTAC} 2013 - 10th International
  Colloquium, Shanghai, China, September 4-6, 2013. Proceedings
series_title: Lecture Notes in Computer Science
status: public
title: A High-Level Semantics for Program Execution under Total Store Order Memory
type: conference
user_id: '29719'
year: '2013'
...
---
_id: '3179'
author:
- first_name: Steffen
  full_name: Ziegert, Steffen
  last_name: Ziegert
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Ziegert S, Wehrheim H. Temporal Reconfiguration Plans for Self-Adaptive Systems.
    In: Kowalewski S, Rumpe B, eds. <i>Software Engineering 2013: Fachtagung Des GI-Fachbereichs
    Softwaretechnik, 26. Februar - 2. M{\"{a}}rz 2013 in Aachen</i>. {LNI}. ; 2013:271--284.'
  apa: 'Ziegert, S., &#38; Wehrheim, H. (2013). Temporal Reconfiguration Plans for
    Self-Adaptive Systems. In S. Kowalewski &#38; B. Rumpe (Eds.), <i>Software Engineering
    2013: Fachtagung des GI-Fachbereichs Softwaretechnik, 26. Februar - 2. M{\"{a}}rz
    2013 in Aachen</i> (pp. 271--284).'
  bibtex: '@inproceedings{Ziegert_Wehrheim_2013, series={{LNI}}, title={Temporal Reconfiguration
    Plans for Self-Adaptive Systems}, booktitle={Software Engineering 2013: Fachtagung
    des GI-Fachbereichs Softwaretechnik, 26. Februar - 2. M{\"{a}}rz 2013 in Aachen},
    author={Ziegert, Steffen and Wehrheim, Heike}, editor={Kowalewski, Stefan and
    Rumpe, BernhardEditors}, year={2013}, pages={271--284}, collection={{LNI}} }'
  chicago: 'Ziegert, Steffen, and Heike Wehrheim. “Temporal Reconfiguration Plans
    for Self-Adaptive Systems.” In <i>Software Engineering 2013: Fachtagung Des GI-Fachbereichs
    Softwaretechnik, 26. Februar - 2. M{\"{a}}rz 2013 in Aachen</i>, edited by Stefan
    Kowalewski and Bernhard Rumpe, 271--284. {LNI}, 2013.'
  ieee: 'S. Ziegert and H. Wehrheim, “Temporal Reconfiguration Plans for Self-Adaptive
    Systems,” in <i>Software Engineering 2013: Fachtagung des GI-Fachbereichs Softwaretechnik,
    26. Februar - 2. M{\"{a}}rz 2013 in Aachen</i>, 2013, pp. 271--284.'
  mla: 'Ziegert, Steffen, and Heike Wehrheim. “Temporal Reconfiguration Plans for
    Self-Adaptive Systems.” <i>Software Engineering 2013: Fachtagung Des GI-Fachbereichs
    Softwaretechnik, 26. Februar - 2. M{\"{a}}rz 2013 in Aachen</i>, edited by Stefan
    Kowalewski and Bernhard Rumpe, 2013, pp. 271--284.'
  short: 'S. Ziegert, H. Wehrheim, in: S. Kowalewski, B. Rumpe (Eds.), Software Engineering
    2013: Fachtagung Des GI-Fachbereichs Softwaretechnik, 26. Februar - 2. M{\"{a}}rz
    2013 in Aachen, 2013, pp. 271--284.'
date_created: 2018-06-13T08:15:08Z
date_updated: 2022-01-06T06:59:02Z
department:
- _id: '77'
editor:
- first_name: Stefan
  full_name: Kowalewski, Stefan
  last_name: Kowalewski
- first_name: Bernhard
  full_name: Rumpe, Bernhard
  last_name: Rumpe
page: 271--284
publication: 'Software Engineering 2013: Fachtagung des GI-Fachbereichs Softwaretechnik,
  26. Februar - 2. M{\"{a}}rz 2013 in Aachen'
series_title: '{LNI}'
status: public
title: Temporal Reconfiguration Plans for Self-Adaptive Systems
type: conference
user_id: '29719'
year: '2013'
...
---
_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: '517'
abstract:
- lang: eng
  text: In the Semantic (Web) Services area, services are considered black boxes with
    a semantic description of their interfaces as to allow for precise service selection
    and configuration. The semantic description is usually grounded on domain-specific
    concepts as modeled in ontologies. This accounts for types used in service signatures,
    but also predicates occurring in preconditions and effects of services. Ontologies,
    in particular those enhanced with rules, capture the knowledge of domain experts
    on properties of and relations between domain concepts. In this paper, we present
    a verification technique for service compositions which makes use of this domain
    knowledge. We consider a service composition to be an assembly of services of
    which we just know signatures, preconditions, and effects. We aim at proving that
    a composition satisfies a (user-defined) requirement, specified in terms of guaranteed
    preconditions and required postconditions. As an underlying verification engine
    we use an SMT solver. To take advantage of the domain knowledge (and often, to
    enable verification at all), the knowledge is fed into the solver in the form of
    sorts, uninterpreted functions and in particular assertions as to enhance the
    solver’s reasoning capabilities. Thereby, we allow for deductions within a domain
    previously unknown to the solver. We exemplify our technique on a case study from
    the area of water network optimization software.
author:
- first_name: Sven
  full_name: Walther, Sven
  last_name: Walther
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Walther S, Wehrheim H. Knowledge-Based Verification of Service Compositions
    - An SMT approach. In: <i>Proceedings of the 18th IEEE International Conference
    on Engineering of Complex Computer Systems (ICECCS)</i>. ; 2013:24-32. doi:<a
    href="https://doi.org/10.1109/ICECCS.2013.14">10.1109/ICECCS.2013.14</a>'
  apa: Walther, S., &#38; Wehrheim, H. (2013). Knowledge-Based Verification of Service
    Compositions - An SMT approach. In <i>Proceedings of the 18th IEEE International
    Conference on Engineering of Complex Computer Systems (ICECCS)</i> (pp. 24–32).
    <a href="https://doi.org/10.1109/ICECCS.2013.14">https://doi.org/10.1109/ICECCS.2013.14</a>
  bibtex: '@inproceedings{Walther_Wehrheim_2013, title={Knowledge-Based Verification
    of Service Compositions - An SMT approach}, DOI={<a href="https://doi.org/10.1109/ICECCS.2013.14">10.1109/ICECCS.2013.14</a>},
    booktitle={Proceedings of the 18th IEEE International Conference on Engineering
    of Complex Computer Systems (ICECCS)}, author={Walther, Sven and Wehrheim, Heike},
    year={2013}, pages={24–32} }'
  chicago: Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service
    Compositions - An SMT Approach.” In <i>Proceedings of the 18th IEEE International
    Conference on Engineering of Complex Computer Systems (ICECCS)</i>, 24–32, 2013.
    <a href="https://doi.org/10.1109/ICECCS.2013.14">https://doi.org/10.1109/ICECCS.2013.14</a>.
  ieee: S. Walther and H. Wehrheim, “Knowledge-Based Verification of Service Compositions
    - An SMT approach,” in <i>Proceedings of the 18th IEEE International Conference
    on Engineering of Complex Computer Systems (ICECCS)</i>, 2013, pp. 24–32.
  mla: Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service
    Compositions - An SMT Approach.” <i>Proceedings of the 18th IEEE International
    Conference on Engineering of Complex Computer Systems (ICECCS)</i>, 2013, pp.
    24–32, doi:<a href="https://doi.org/10.1109/ICECCS.2013.14">10.1109/ICECCS.2013.14</a>.
  short: 'S. Walther, H. Wehrheim, in: Proceedings of the 18th IEEE International
    Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.'
date_created: 2017-10-17T12:42:33Z
date_updated: 2022-01-06T07:01:41Z
ddc:
- '000'
department:
- _id: '77'
doi: 10.1109/ICECCS.2013.14
file:
- access_level: closed
  content_type: application/pdf
  creator: ups
  date_created: 2018-11-02T13:26:08Z
  date_updated: 2018-11-02T13:26:08Z
  file_id: '5248'
  file_name: 06601801.pdf
  file_size: 217085
  relation: main_file
file_date_updated: 2018-11-02T13:26:08Z
has_accepted_license: '1'
language:
- iso: eng
page: '24 - 32 '
project:
- _id: '1'
  name: SFB 901
- _id: '11'
  name: SFB 901 - Subprojekt B3
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 18th IEEE International Conference on Engineering
  of Complex Computer Systems (ICECCS)
status: public
title: Knowledge-Based Verification of Service Compositions - An SMT approach
type: conference
user_id: '477'
year: '2013'
...
---
_id: '3180'
author:
- first_name: Oleg
  full_name: Travkin, Oleg
  last_name: Travkin
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
- first_name: Gerhard
  full_name: Schellhorn, Gerhard
  last_name: Schellhorn
citation:
  ama: Travkin O, Wehrheim H, Schellhorn G. Proving Linearizability of Multiset with
    Local Proof Obligations. <i>{ECEASST}</i>. 2012.
  apa: Travkin, O., Wehrheim, H., &#38; Schellhorn, G. (2012). Proving Linearizability
    of Multiset with Local Proof Obligations. <i>{ECEASST}</i>.
  bibtex: '@article{Travkin_Wehrheim_Schellhorn_2012, title={Proving Linearizability
    of Multiset with Local Proof Obligations}, journal={{ECEASST}}, author={Travkin,
    Oleg and Wehrheim, Heike and Schellhorn, Gerhard}, year={2012} }'
  chicago: Travkin, Oleg, Heike Wehrheim, and Gerhard Schellhorn. “Proving Linearizability
    of Multiset with Local Proof Obligations.” <i>{ECEASST}</i>, 2012.
  ieee: O. Travkin, H. Wehrheim, and G. Schellhorn, “Proving Linearizability of Multiset
    with Local Proof Obligations,” <i>{ECEASST}</i>, 2012.
  mla: Travkin, Oleg, et al. “Proving Linearizability of Multiset with Local Proof
    Obligations.” <i>{ECEASST}</i>, 2012.
  short: O. Travkin, H. Wehrheim, G. Schellhorn, {ECEASST} (2012).
date_created: 2018-06-13T08:16:49Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
publication: '{ECEASST}'
status: public
title: Proving Linearizability of Multiset with Local Proof Obligations
type: journal_article
user_id: '29719'
year: '2012'
...
---
_id: '3181'
author:
- first_name: Thomas
  full_name: Ruhroth, Thomas
  last_name: Ruhroth
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: Ruhroth T, Wehrheim H. Model evolution and refinement. <i>Sci Comput Program</i>.
    2012;(3):270--289. doi:<a href="https://doi.org/10.1016/j.scico.2011.04.007">10.1016/j.scico.2011.04.007</a>
  apa: Ruhroth, T., &#38; Wehrheim, H. (2012). Model evolution and refinement. <i>Sci.
    Comput. Program.</i>, (3), 270--289. <a href="https://doi.org/10.1016/j.scico.2011.04.007">https://doi.org/10.1016/j.scico.2011.04.007</a>
  bibtex: '@article{Ruhroth_Wehrheim_2012, title={Model evolution and refinement},
    DOI={<a href="https://doi.org/10.1016/j.scico.2011.04.007">10.1016/j.scico.2011.04.007</a>},
    number={3}, journal={Sci. Comput. Program.}, author={Ruhroth, Thomas and Wehrheim,
    Heike}, year={2012}, pages={270--289} }'
  chicago: 'Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.”
    <i>Sci. Comput. Program.</i>, no. 3 (2012): 270--289. <a href="https://doi.org/10.1016/j.scico.2011.04.007">https://doi.org/10.1016/j.scico.2011.04.007</a>.'
  ieee: T. Ruhroth and H. Wehrheim, “Model evolution and refinement,” <i>Sci. Comput.
    Program.</i>, no. 3, pp. 270--289, 2012.
  mla: Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.” <i>Sci.
    Comput. Program.</i>, no. 3, 2012, pp. 270--289, doi:<a href="https://doi.org/10.1016/j.scico.2011.04.007">10.1016/j.scico.2011.04.007</a>.
  short: T. Ruhroth, H. Wehrheim, Sci. Comput. Program. (2012) 270--289.
date_created: 2018-06-13T08:17:58Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1016/j.scico.2011.04.007
issue: '3'
page: 270--289
publication: Sci. Comput. Program.
status: public
title: Model evolution and refinement
type: journal_article
user_id: '29719'
year: '2012'
...
---
_id: '3182'
author:
- first_name: Gerhard
  full_name: Schellhorn, Gerhard
  last_name: Schellhorn
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
- first_name: John
  full_name: Derrick, John
  last_name: Derrick
citation:
  ama: 'Schellhorn G, Wehrheim H, Derrick J. How to Prove Algorithms Linearisable.
    In: Madhusudan P, A. Seshia S, eds. <i>Computer Aided Verification - 24th International
    Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>. Lecture
    Notes in Computer Science. ; 2012:243--259. doi:<a href="https://doi.org/10.1007/978-3-642-31424-7_21">10.1007/978-3-642-31424-7_21</a>'
  apa: Schellhorn, G., Wehrheim, H., &#38; Derrick, J. (2012). How to Prove Algorithms
    Linearisable. In P. Madhusudan &#38; S. A. Seshia (Eds.), <i>Computer Aided Verification
    - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012
    Proceedings</i> (pp. 243--259). <a href="https://doi.org/10.1007/978-3-642-31424-7_21">https://doi.org/10.1007/978-3-642-31424-7_21</a>
  bibtex: '@inproceedings{Schellhorn_Wehrheim_Derrick_2012, series={Lecture Notes
    in Computer Science}, title={How to Prove Algorithms Linearisable}, DOI={<a href="https://doi.org/10.1007/978-3-642-31424-7_21">10.1007/978-3-642-31424-7_21</a>},
    booktitle={Computer Aided Verification - 24th International Conference, {CAV}
    2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings}, author={Schellhorn, Gerhard
    and Wehrheim, Heike and Derrick, John}, editor={Madhusudan, P. and A. Seshia,
    SanjitEditors}, year={2012}, pages={243--259}, collection={Lecture Notes in Computer
    Science} }'
  chicago: Schellhorn, Gerhard, Heike Wehrheim, and John Derrick. “How to Prove Algorithms
    Linearisable.” In <i>Computer Aided Verification - 24th International Conference,
    {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>, edited by P. Madhusudan
    and Sanjit A. Seshia, 243--259. Lecture Notes in Computer Science, 2012. <a href="https://doi.org/10.1007/978-3-642-31424-7_21">https://doi.org/10.1007/978-3-642-31424-7_21</a>.
  ieee: G. Schellhorn, H. Wehrheim, and J. Derrick, “How to Prove Algorithms Linearisable,”
    in <i>Computer Aided Verification - 24th International Conference, {CAV} 2012,
    Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>, 2012, pp. 243--259.
  mla: Schellhorn, Gerhard, et al. “How to Prove Algorithms Linearisable.” <i>Computer
    Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA,
    USA, July 7-13, 2012 Proceedings</i>, edited by P. Madhusudan and Sanjit A. Seshia,
    2012, pp. 243--259, doi:<a href="https://doi.org/10.1007/978-3-642-31424-7_21">10.1007/978-3-642-31424-7_21</a>.
  short: 'G. Schellhorn, H. Wehrheim, J. Derrick, in: P. Madhusudan, S. A. Seshia
    (Eds.), Computer Aided Verification - 24th International Conference, {CAV} 2012,
    Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, pp. 243--259.'
date_created: 2018-06-13T08:19:33Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1007/978-3-642-31424-7_21
editor:
- first_name: P.
  full_name: Madhusudan, P.
  last_name: Madhusudan
- first_name: Sanjit
  full_name: A. Seshia, Sanjit
  last_name: A. Seshia
page: 243--259
publication: Computer Aided Verification - 24th International Conference, {CAV} 2012,
  Berkeley, CA, USA, July 7-13, 2012 Proceedings
series_title: Lecture Notes in Computer Science
status: public
title: How to Prove Algorithms Linearisable
type: conference
user_id: '29719'
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: '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: '565'
abstract:
- lang: eng
  text: 'In model-driven development of multi-layer systems (e.g. application, platform
    and infrastructure), each layer is usually described by separate models. When
    generating analysis models or code, these separate models rst of all need to be
    linked. Hence, existing model transformations for single layers cannot be simply
    re-used. In this paper, we present a modular approach to the transformation of
    multi-layer systems. It employs model weaving to dene the interconnections between
    models of dierent layers. The weaving models themselves are subject to model transformations:
    The result of transforming a weaving model constitutes a conguration for the models
    obtained by transforming single layers, thereby allowing for a re-use of existing
    model transformations. We exemplify our approach by the generation of analysis
    models for component-based software.'
author:
- first_name: Galina
  full_name: Besova, Galina
  last_name: Besova
- first_name: Sven
  full_name: Walther, Sven
  last_name: Walther
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
- first_name: Steffen
  full_name: Becker, Steffen
  last_name: Becker
citation:
  ama: 'Besova G, Walther S, Wehrheim H, Becker S. Weaving-based configuration and
    modular transformation of multi-layer systems. In: <i>Proceedings of the 15th
    International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i>.
    LNCS. ; 2012:776-792. doi:<a href="https://doi.org/10.1007/978-3-642-33666-9_49">10.1007/978-3-642-33666-9_49</a>'
  apa: Besova, G., Walther, S., Wehrheim, H., &#38; Becker, S. (2012). Weaving-based
    configuration and modular transformation of multi-layer systems. In <i>Proceedings
    of the 15th International Conference on Model Driven Engineering Languages &#38;
    Systems (MoDELS)</i> (pp. 776–792). <a href="https://doi.org/10.1007/978-3-642-33666-9_49">https://doi.org/10.1007/978-3-642-33666-9_49</a>
  bibtex: '@inproceedings{Besova_Walther_Wehrheim_Becker_2012, series={LNCS}, title={Weaving-based
    configuration and modular transformation of multi-layer systems}, DOI={<a href="https://doi.org/10.1007/978-3-642-33666-9_49">10.1007/978-3-642-33666-9_49</a>},
    booktitle={Proceedings of the 15th International Conference on Model Driven Engineering
    Languages &#38; Systems (MoDELS)}, author={Besova, Galina and Walther, Sven and
    Wehrheim, Heike and Becker, Steffen}, year={2012}, pages={776–792}, collection={LNCS}
    }'
  chicago: Besova, Galina, Sven Walther, Heike Wehrheim, and Steffen Becker. “Weaving-Based
    Configuration and Modular Transformation of Multi-Layer Systems.” In <i>Proceedings
    of the 15th International Conference on Model Driven Engineering Languages &#38;
    Systems (MoDELS)</i>, 776–92. LNCS, 2012. <a href="https://doi.org/10.1007/978-3-642-33666-9_49">https://doi.org/10.1007/978-3-642-33666-9_49</a>.
  ieee: G. Besova, S. Walther, H. Wehrheim, and S. Becker, “Weaving-based configuration
    and modular transformation of multi-layer systems,” in <i>Proceedings of the 15th
    International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i>,
    2012, pp. 776–792.
  mla: Besova, Galina, et al. “Weaving-Based Configuration and Modular Transformation
    of Multi-Layer Systems.” <i>Proceedings of the 15th International Conference on
    Model Driven Engineering Languages &#38; Systems (MoDELS)</i>, 2012, pp. 776–92,
    doi:<a href="https://doi.org/10.1007/978-3-642-33666-9_49">10.1007/978-3-642-33666-9_49</a>.
  short: 'G. Besova, S. Walther, H. Wehrheim, S. Becker, in: Proceedings of the 15th
    International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS),
    2012, pp. 776–792.'
date_created: 2017-10-17T12:42:42Z
date_updated: 2022-01-06T07:02:20Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-642-33666-9_49
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-15T10:24:06Z
  date_updated: 2018-03-15T10:24:06Z
  file_id: '1276'
  file_name: 565-Besova_et_al._-_2012_-_Weaving-Based_Configuration_and_Modular_Transformation_of_Multi-layer_Systems_01.pdf
  file_size: 589972
  relation: main_file
  success: 1
file_date_updated: 2018-03-15T10:24:06Z
has_accepted_license: '1'
language:
- iso: eng
page: 776-792
project:
- _id: '1'
  name: SFB 901
- _id: '11'
  name: SFB 901 - Subprojekt B3
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 15th International Conference on Model Driven Engineering
  Languages & Systems (MoDELS)
series_title: LNCS
status: public
title: Weaving-based configuration and modular transformation of multi-layer systems
type: conference
user_id: '477'
year: '2012'
...
---
_id: '3183'
author:
- first_name: Steve
  full_name: Schneider, Steve
  last_name: Schneider
- first_name: Helen
  full_name: Treharne, Helen
  last_name: Treharne
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Schneider S, Treharne H, Wehrheim H. Bounded Retransmission in Event-B{\(\parallel\)}CSP:
    a Case Study. <i>Electr Notes Theor Comput Sci</i>. 2011:69--80. doi:<a href="https://doi.org/10.1016/j.entcs.2011.11.019">10.1016/j.entcs.2011.11.019</a>'
  apa: 'Schneider, S., Treharne, H., &#38; Wehrheim, H. (2011). Bounded Retransmission
    in Event-B{\(\parallel\)}CSP: a Case Study. <i>Electr. Notes Theor. Comput. Sci.</i>,
    69--80. <a href="https://doi.org/10.1016/j.entcs.2011.11.019">https://doi.org/10.1016/j.entcs.2011.11.019</a>'
  bibtex: '@article{Schneider_Treharne_Wehrheim_2011, title={Bounded Retransmission
    in Event-B{\(\parallel\)}CSP: a Case Study}, DOI={<a href="https://doi.org/10.1016/j.entcs.2011.11.019">10.1016/j.entcs.2011.11.019</a>},
    journal={Electr. Notes Theor. Comput. Sci.}, author={Schneider, Steve and Treharne,
    Helen and Wehrheim, Heike}, year={2011}, pages={69--80} }'
  chicago: 'Schneider, Steve, Helen Treharne, and Heike Wehrheim. “Bounded Retransmission
    in Event-B{\(\parallel\)}CSP: A Case Study.” <i>Electr. Notes Theor. Comput. Sci.</i>,
    2011, 69--80. <a href="https://doi.org/10.1016/j.entcs.2011.11.019">https://doi.org/10.1016/j.entcs.2011.11.019</a>.'
  ieee: 'S. Schneider, H. Treharne, and H. Wehrheim, “Bounded Retransmission in Event-B{\(\parallel\)}CSP:
    a Case Study,” <i>Electr. Notes Theor. Comput. Sci.</i>, pp. 69--80, 2011.'
  mla: 'Schneider, Steve, et al. “Bounded Retransmission in Event-B{\(\parallel\)}CSP:
    A Case Study.” <i>Electr. Notes Theor. Comput. Sci.</i>, 2011, pp. 69--80, doi:<a
    href="https://doi.org/10.1016/j.entcs.2011.11.019">10.1016/j.entcs.2011.11.019</a>.'
  short: S. Schneider, H. Treharne, H. Wehrheim, Electr. Notes Theor. Comput. Sci.
    (2011) 69--80.
date_created: 2018-06-13T08:20:47Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1016/j.entcs.2011.11.019
page: 69--80
publication: Electr. Notes Theor. Comput. Sci.
status: public
title: 'Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study'
type: journal_article
user_id: '29719'
year: '2011'
...
---
_id: '3184'
author:
- first_name: John
  full_name: Derrick, John
  last_name: Derrick
- first_name: Gerhard
  full_name: Schellhorn, Gerhard
  last_name: Schellhorn
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: Derrick J, Schellhorn G, Wehrheim H. Mechanically verified proof obligations
    for linearizability. <i>{ACM} Trans Program Lang Syst</i>. 2011;(1):4:1--4:43.
    doi:<a href="https://doi.org/10.1145/1889997.1890001">10.1145/1889997.1890001</a>
  apa: Derrick, J., Schellhorn, G., &#38; Wehrheim, H. (2011). Mechanically verified
    proof obligations for linearizability. <i>{ACM} Trans. Program. Lang. Syst.</i>,
    (1), 4:1--4:43. <a href="https://doi.org/10.1145/1889997.1890001">https://doi.org/10.1145/1889997.1890001</a>
  bibtex: '@article{Derrick_Schellhorn_Wehrheim_2011, title={Mechanically verified
    proof obligations for linearizability}, DOI={<a href="https://doi.org/10.1145/1889997.1890001">10.1145/1889997.1890001</a>},
    number={1}, journal={{ACM} Trans. Program. Lang. Syst.}, author={Derrick, John
    and Schellhorn, Gerhard and Wehrheim, Heike}, year={2011}, pages={4:1--4:43} }'
  chicago: 'Derrick, John, Gerhard Schellhorn, and Heike Wehrheim. “Mechanically Verified
    Proof Obligations for Linearizability.” <i>{ACM} Trans. Program. Lang. Syst.</i>,
    no. 1 (2011): 4:1--4:43. <a href="https://doi.org/10.1145/1889997.1890001">https://doi.org/10.1145/1889997.1890001</a>.'
  ieee: J. Derrick, G. Schellhorn, and H. Wehrheim, “Mechanically verified proof obligations
    for linearizability,” <i>{ACM} Trans. Program. Lang. Syst.</i>, no. 1, pp. 4:1--4:43,
    2011.
  mla: Derrick, John, et al. “Mechanically Verified Proof Obligations for Linearizability.”
    <i>{ACM} Trans. Program. Lang. Syst.</i>, no. 1, 2011, pp. 4:1--4:43, doi:<a href="https://doi.org/10.1145/1889997.1890001">10.1145/1889997.1890001</a>.
  short: J. Derrick, G. Schellhorn, H. Wehrheim, {ACM} Trans. Program. Lang. Syst.
    (2011) 4:1--4:43.
date_created: 2018-06-13T08:22:02Z
date_updated: 2022-01-06T06:59:03Z
department:
- _id: '77'
doi: 10.1145/1889997.1890001
issue: '1'
page: 4:1--4:43
publication: '{ACM} Trans. Program. Lang. Syst.'
status: public
title: Mechanically verified proof obligations for linearizability
type: journal_article
user_id: '29719'
year: '2011'
...