---
OA_place: publisher
OA_type: hybrid
_id: '20189'
abstract:
- lang: eng
  text: Certification was made mandatory for the first time in the latest hardware
    model checking competition. In this case study, we investigate the trade-offs
    of requiring certificates for both passing and failing properties in the competition.
    Our evaluation shows that participating model checkers were able to produce compact,
    correct certificates that could be verified with minimal overhead. Furthermore,
    the certifying winner of the competition outperforms the previous non-certifying
    state-of-the-art model checker, demonstrating that certification can be adopted
    without compromising model checking efficiency.
acknowledgement: "This work is supported in part by the ERC-2020-AdG 101020093, the
  LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland
  under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of
  course also owe a big thank-you to the submitters of model checkers and benchmarks
  to the competition over all these years. Without their enthusiasm and support neither
  the competition nor this study would exist."
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Nils
  full_name: Froleyks, Nils
  last_name: Froleyks
- first_name: Zhengqi
  full_name: Yu, Zhengqi
  id: 20aa2ae8-f2f1-11ed-bbfa-8205053f1342
  last_name: Yu
  orcid: 0000-0002-4993-773X
- first_name: Mathias
  full_name: Preiner, Mathias
  last_name: Preiner
- first_name: Armin
  full_name: Biere, Armin
  last_name: Biere
- first_name: Keijo
  full_name: Heljanko, Keijo
  last_name: Heljanko
citation:
  ama: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates
    to the hardware model checking competition. In: <i>37th International Conference
    on Computer Aided Verification</i>. Vol 15931. Springer Nature; 2025:281-295.
    doi:<a href="https://doi.org/10.1007/978-3-031-98668-0_14">10.1007/978-3-031-98668-0_14</a>'
  apa: 'Froleyks, N., Yu, E., Preiner, M., Biere, A., &#38; Heljanko, K. (2025). Introducing
    certificates to the hardware model checking competition. In <i>37th International
    Conference on Computer Aided Verification</i> (Vol. 15931, pp. 281–295). Zagreb,
    Croatia: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-98668-0_14">https://doi.org/10.1007/978-3-031-98668-0_14</a>'
  chicago: Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko.
    “Introducing Certificates to the Hardware Model Checking Competition.” In <i>37th
    International Conference on Computer Aided Verification</i>, 15931:281–95. Springer
    Nature, 2025. <a href="https://doi.org/10.1007/978-3-031-98668-0_14">https://doi.org/10.1007/978-3-031-98668-0_14</a>.
  ieee: N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates
    to the hardware model checking competition,” in <i>37th International Conference
    on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.
  ista: 'Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates
    to the hardware model checking competition. 37th International Conference on Computer
    Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.'
  mla: Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking
    Competition.” <i>37th International Conference on Computer Aided Verification</i>,
    vol. 15931, Springer Nature, 2025, pp. 281–95, doi:<a href="https://doi.org/10.1007/978-3-031-98668-0_14">10.1007/978-3-031-98668-0_14</a>.
  short: N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International
    Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.
conference:
  end_date: 2025-07-25
  location: Zagreb, Croatia
  name: 'CAV: Computer Aided Verification'
  start_date: 2025-07-23
date_created: 2025-08-17T22:01:36Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-12-01T12:34:05Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-98668-0_14
ec_funded: 1
external_id:
  isi:
  - '001562507100014'
file:
- access_level: open_access
  checksum: 15ec1bc9b9409d3b2736f4c9d5f42fd1
  content_type: application/pdf
  creator: dernst
  date_created: 2025-09-02T05:46:10Z
  date_updated: 2025-09-02T05:46:10Z
  file_id: '20266'
  file_name: 2025_CAV_Froleyks.pdf
  file_size: 1078274
  relation: main_file
  success: 1
file_date_updated: 2025-09-02T05:46:10Z
has_accepted_license: '1'
intvolume: '     15931'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '01'
oa: 1
oa_version: Published Version
page: 281-295
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 37th International Conference on Computer Aided Verification
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031986673'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Introducing certificates to the hardware model checking competition
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15931
year: '2025'
...