---
_id: '20276'
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Beyer D, Wehrheim H. Verification Artifacts in Cooperative Verification: Survey
    and Unifying Component Framework. In: Margaria T, Steffen B, eds. <i>Leveraging
    Applications of Formal Methods, Verification and Validation: Verification Principles
    - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA
    2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i>. Vol 12476.
    Lecture Notes in Computer Science. Springer; 2020:143-167. doi:<a href="https://doi.org/10.1007/978-3-030-61362-4\_8">10.1007/978-3-030-61362-4\_8</a>'
  apa: 'Beyer, D., &#38; Wehrheim, H. (2020). Verification Artifacts in Cooperative
    Verification: Survey and Unifying Component Framework. In T. Margaria &#38; B.
    Steffen (Eds.), <i>Leveraging Applications of Formal Methods, Verification and
    Validation: Verification Principles - 9th International Symposium on Leveraging
    Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020,
    Proceedings, Part {I}</i> (Vol. 12476, pp. 143–167). Springer. <a href="https://doi.org/10.1007/978-3-030-61362-4\_8">https://doi.org/10.1007/978-3-030-61362-4\_8</a>'
  bibtex: '@inproceedings{Beyer_Wehrheim_2020, series={Lecture Notes in Computer Science},
    title={Verification Artifacts in Cooperative Verification: Survey and Unifying
    Component Framework}, volume={12476}, DOI={<a href="https://doi.org/10.1007/978-3-030-61362-4\_8">10.1007/978-3-030-61362-4\_8</a>},
    booktitle={Leveraging Applications of Formal Methods, Verification and Validation:
    Verification Principles - 9th International Symposium on Leveraging Applications
    of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings,
    Part {I}}, publisher={Springer}, author={Beyer, Dirk and Wehrheim, Heike}, editor={Margaria,
    Tiziana and Steffen, BernhardEditors}, year={2020}, pages={143–167}, collection={Lecture
    Notes in Computer Science} }'
  chicago: 'Beyer, Dirk, and Heike Wehrheim. “Verification Artifacts in Cooperative
    Verification: Survey and Unifying Component Framework.” In <i>Leveraging Applications
    of Formal Methods, Verification and Validation: Verification Principles - 9th
    International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020,
    Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i>, edited by Tiziana
    Margaria and Bernhard Steffen, 12476:143–67. Lecture Notes in Computer Science.
    Springer, 2020. <a href="https://doi.org/10.1007/978-3-030-61362-4\_8">https://doi.org/10.1007/978-3-030-61362-4\_8</a>.'
  ieee: 'D. Beyer and H. Wehrheim, “Verification Artifacts in Cooperative Verification:
    Survey and Unifying Component Framework,” in <i>Leveraging Applications of Formal
    Methods, Verification and Validation: Verification Principles - 9th International
    Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece,
    October 20-30, 2020, Proceedings, Part {I}</i>, 2020, vol. 12476, pp. 143–167.'
  mla: 'Beyer, Dirk, and Heike Wehrheim. “Verification Artifacts in Cooperative Verification:
    Survey and Unifying Component Framework.” <i>Leveraging Applications of Formal
    Methods, Verification and Validation: Verification Principles - 9th International
    Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece,
    October 20-30, 2020, Proceedings, Part {I}</i>, edited by Tiziana Margaria and
    Bernhard Steffen, vol. 12476, Springer, 2020, pp. 143–67, doi:<a href="https://doi.org/10.1007/978-3-030-61362-4\_8">10.1007/978-3-030-61362-4\_8</a>.'
  short: 'D. Beyer, H. Wehrheim, in: T. Margaria, B. Steffen (Eds.), Leveraging Applications
    of Formal Methods, Verification and Validation: Verification Principles - 9th
    International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020,
    Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}, Springer, 2020, pp.
    143–167.'
date_created: 2020-11-04T08:36:22Z
date_updated: 2022-01-06T06:54:25Z
department:
- _id: '77'
doi: 10.1007/978-3-030-61362-4\_8
editor:
- first_name: Tiziana
  full_name: Margaria, Tiziana
  last_name: Margaria
- first_name: Bernhard
  full_name: Steffen, Bernhard
  last_name: Steffen
intvolume: '     12476'
language:
- iso: eng
page: 143-167
project:
- _id: '85'
  name: Kooperative Softwareverifikation
publication: 'Leveraging Applications of Formal Methods, Verification and Validation:
  Verification Principles - 9th International Symposium on Leveraging Applications
  of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings,
  Part {I}'
publisher: Springer
series_title: Lecture Notes in Computer Science
status: public
title: 'Verification Artifacts in Cooperative Verification: Survey and Unifying Component
  Framework'
type: conference
user_id: '29719'
volume: 12476
year: '2020'
...
---
_id: '17825'
abstract:
- lang: eng
  text: "Software verification has recently made enormous progress due to the\r\ndevelopment
    of novel verification methods and the speed-up of supporting\r\ntechnologies like
    SMT solving. To keep software verification tools up to date\r\nwith these advances,
    tool developers keep on integrating newly designed methods\r\ninto their tools,
    almost exclusively by re-implementing the method within their\r\nown framework.
    While this allows for a conceptual re-use of methods, it\r\nrequires novel implementations
    for every new technique.\r\n  In this paper, we employ cooperative verification
    in order to avoid\r\nreimplementation and enable usage of novel tools as black-box
    components in\r\nverification. Specifically, cooperation is employed for the core
    ingredient of\r\nsoftware verification which is invariant generation. Finding
    an adequate loop\r\ninvariant is key to the success of a verification run. Our
    framework named\r\nCoVerCIG allows a master verification tool to delegate the
    task of invariant\r\ngeneration to one or several specialized helper invariant
    generators. Their\r\nresults are then utilized within the verification run of
    the master verifier,\r\nallowing in particular for crosschecking the validity
    of the invariant. We\r\nexperimentally evaluate our framework on an instance with
    two masters and three\r\ndifferent invariant generators using a number of benchmarks
    from SV-COMP 2020.\r\nThe experiments show that the use of CoVerCIG can increase
    the number of\r\ncorrectly verified tasks without increasing the used resources"
author:
- first_name: Jan Frederik
  full_name: Haltermann, Jan Frederik
  id: '44413'
  last_name: Haltermann
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: Haltermann JF, Wehrheim H. Cooperative Verification via Collective Invariant
    Generation. <i>arXiv:200804551</i>. 2020.
  apa: Haltermann, J. F., &#38; Wehrheim, H. (2020). Cooperative Verification via
    Collective Invariant Generation. <i>ArXiv:2008.04551</i>.
  bibtex: '@article{Haltermann_Wehrheim_2020, title={Cooperative Verification via
    Collective Invariant Generation}, journal={arXiv:2008.04551}, author={Haltermann,
    Jan Frederik and Wehrheim, Heike}, year={2020} }'
  chicago: Haltermann, Jan Frederik, and Heike Wehrheim. “Cooperative Verification
    via Collective Invariant Generation.” <i>ArXiv:2008.04551</i>, 2020.
  ieee: J. F. Haltermann and H. Wehrheim, “Cooperative Verification via Collective
    Invariant Generation,” <i>arXiv:2008.04551</i>. 2020.
  mla: Haltermann, Jan Frederik, and Heike Wehrheim. “Cooperative Verification via
    Collective Invariant Generation.” <i>ArXiv:2008.04551</i>, 2020.
  short: J.F. Haltermann, H. Wehrheim, ArXiv:2008.04551 (2020).
date_created: 2020-08-12T06:49:18Z
date_updated: 2022-01-06T06:53:20Z
department:
- _id: '77'
language:
- iso: eng
project:
- _id: '85'
  name: Kooperative Softwareverifikation
publication: arXiv:2008.04551
status: public
title: Cooperative Verification via Collective Invariant Generation
type: preprint
user_id: '44413'
year: '2020'
...
---
_id: '13872'
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Marie-Christine
  full_name: Jakobs, Marie-Christine
  last_name: Jakobs
citation:
  ama: 'Beyer D, Jakobs M-C. CoVeriTest: Cooperative Verifier-Based Testing. In: <i>Fundamental
    Approaches to Software Engineering</i>. Cham; 2019. doi:<a href="https://doi.org/10.1007/978-3-030-16722-6_23">10.1007/978-3-030-16722-6_23</a>'
  apa: 'Beyer, D., &#38; Jakobs, M.-C. (2019). CoVeriTest: Cooperative Verifier-Based
    Testing. In <i>Fundamental Approaches to Software Engineering</i>. Cham. <a href="https://doi.org/10.1007/978-3-030-16722-6_23">https://doi.org/10.1007/978-3-030-16722-6_23</a>'
  bibtex: '@inbook{Beyer_Jakobs_2019, place={Cham}, title={CoVeriTest: Cooperative
    Verifier-Based Testing}, DOI={<a href="https://doi.org/10.1007/978-3-030-16722-6_23">10.1007/978-3-030-16722-6_23</a>},
    booktitle={Fundamental Approaches to Software Engineering}, author={Beyer, Dirk
    and Jakobs, Marie-Christine}, year={2019} }'
  chicago: 'Beyer, Dirk, and Marie-Christine Jakobs. “CoVeriTest: Cooperative Verifier-Based
    Testing.” In <i>Fundamental Approaches to Software Engineering</i>. Cham, 2019.
    <a href="https://doi.org/10.1007/978-3-030-16722-6_23">https://doi.org/10.1007/978-3-030-16722-6_23</a>.'
  ieee: 'D. Beyer and M.-C. Jakobs, “CoVeriTest: Cooperative Verifier-Based Testing,”
    in <i>Fundamental Approaches to Software Engineering</i>, Cham, 2019.'
  mla: 'Beyer, Dirk, and Marie-Christine Jakobs. “CoVeriTest: Cooperative Verifier-Based
    Testing.” <i>Fundamental Approaches to Software Engineering</i>, 2019, doi:<a
    href="https://doi.org/10.1007/978-3-030-16722-6_23">10.1007/978-3-030-16722-6_23</a>.'
  short: 'D. Beyer, M.-C. Jakobs, in: Fundamental Approaches to Software Engineering,
    Cham, 2019.'
date_created: 2019-10-16T06:39:51Z
date_updated: 2022-01-06T06:51:45Z
department:
- _id: '77'
doi: 10.1007/978-3-030-16722-6_23
language:
- iso: eng
place: Cham
project:
- _id: '85'
  name: Kooperative Softwareverifikation
publication: Fundamental Approaches to Software Engineering
publication_identifier:
  isbn:
  - '9783030167219'
  - '9783030167226'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
status: public
title: 'CoVeriTest: Cooperative Verifier-Based Testing'
type: book_chapter
user_id: '44413'
year: '2019'
...
---
_id: '1096'
abstract:
- lang: eng
  text: to appear
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Marie-Christine
  full_name: Jakobs, Marie-Christine
  last_name: Jakobs
- first_name: Thomas
  full_name: Lemberger, Thomas
  last_name: Lemberger
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Beyer D, Jakobs M-C, Lemberger T, Wehrheim H. Reducer-Based Construction of
    Conditional Verifiers. In: <i>Proceedings of the 40th International Conference
    on Software Engineering (ICSE)</i>. ACM; 2018:1182--1193.'
  apa: 'Beyer, D., Jakobs, M.-C., Lemberger, T., &#38; Wehrheim, H. (2018). Reducer-Based
    Construction of Conditional Verifiers. In <i>Proceedings of the 40th International
    Conference on Software Engineering (ICSE)</i> (pp. 1182--1193). Gothenburg, Sweden:
    ACM.'
  bibtex: '@inproceedings{Beyer_Jakobs_Lemberger_Wehrheim_2018, title={Reducer-Based
    Construction of Conditional Verifiers}, booktitle={Proceedings of the 40th International
    Conference on Software Engineering (ICSE)}, publisher={ACM}, author={Beyer, Dirk
    and Jakobs, Marie-Christine and Lemberger, Thomas and Wehrheim, Heike}, year={2018},
    pages={1182--1193} }'
  chicago: Beyer, Dirk, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim.
    “Reducer-Based Construction of Conditional Verifiers.” In <i>Proceedings of the
    40th International Conference on Software Engineering (ICSE)</i>, 1182--1193.
    ACM, 2018.
  ieee: D. Beyer, M.-C. Jakobs, T. Lemberger, and H. Wehrheim, “Reducer-Based Construction
    of Conditional Verifiers,” in <i>Proceedings of the 40th International Conference
    on Software Engineering (ICSE)</i>, Gothenburg, Sweden, 2018, pp. 1182--1193.
  mla: Beyer, Dirk, et al. “Reducer-Based Construction of Conditional Verifiers.”
    <i>Proceedings of the 40th International Conference on Software Engineering (ICSE)</i>,
    ACM, 2018, pp. 1182--1193.
  short: 'D. Beyer, M.-C. Jakobs, T. Lemberger, H. Wehrheim, in: Proceedings of the
    40th International Conference on Software Engineering (ICSE), ACM, 2018, pp. 1182--1193.'
conference:
  end_date: 2018-06-03
  location: Gothenburg, Sweden
  name: 40th International Conference on Software Engineering
  start_date: 2018-05-27
date_created: 2018-01-08T10:52:51Z
date_updated: 2022-01-06T06:50:54Z
ddc:
- '000'
department:
- _id: '77'
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-11-21T10:50:51Z
  date_updated: 2018-11-21T10:50:51Z
  file_id: '5783'
  file_name: Reducer-Based Construction of Conditional Verifiers.pdf
  file_size: 826719
  relation: main_file
  success: 1
file_date_updated: 2018-11-21T10:50:51Z
has_accepted_license: '1'
language:
- iso: eng
page: 1182--1193
project:
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
- _id: '12'
  name: SFB 901 - Subproject B4
- _id: '85'
  name: Kooperative Softwareverifikation
publication: Proceedings of the 40th International Conference on Software Engineering
  (ICSE)
publisher: ACM
status: public
title: Reducer-Based Construction of Conditional Verifiers
type: conference
user_id: '29719'
year: '2018'
...