---
_id: '17413'
abstract:
- lang: eng
  text: Certification helps to increase trust in formal verification of safety-critical
    systems which require assurance on their correctness. In hardware model checking,
    a widely used formal verification technique, phase abstraction is considered one
    of the most commonly used preprocessing techniques. We present an approach to
    certify an extended form of phase abstraction using a generic certificate format.
    As in earlier works our approach involves constructing a witness circuit with
    an inductive invariant property that certifies the correctness of the entire model
    checking process, which is then validated by an independent certificate checker.
    We have implemented and evaluated the proposed approach including certification
    for various preprocessing configurations on hardware model checking competition
    benchmarks. As an improvement on previous work in this area, the proposed method
    is able to efficiently complete certification with an overhead of a fraction of
    model checking time.
acknowledgement: This work is supported by the Austrian Science Fund (FWF) under the
  project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG
  101020093, the Academy of Finland under the project 336092 and by a gift from Intel
  Corporation.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
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
- 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, Biere A, Heljanko K. Certifying phase abstraction. In: <i>Lecture
    Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i>. Vol 14739. Springer Nature; 2024:284-303.
    doi:<a href="https://doi.org/10.1007/978-3-031-63498-7_17">10.1007/978-3-031-63498-7_17</a>'
  apa: 'Froleyks, N., Yu, E., Biere, A., &#38; Heljanko, K. (2024). Certifying phase
    abstraction. In <i>Lecture Notes in Computer Science (including subseries Lecture
    Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol.
    14739, pp. 284–303). Nancy, France: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-63498-7_17">https://doi.org/10.1007/978-3-031-63498-7_17</a>'
  chicago: Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying
    Phase Abstraction.” In <i>Lecture Notes in Computer Science (Including Subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>,
    14739:284–303. Springer Nature, 2024. <a href="https://doi.org/10.1007/978-3-031-63498-7_17">https://doi.org/10.1007/978-3-031-63498-7_17</a>.
  ieee: N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,”
    in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in
    Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Nancy, France,
    2024, vol. 14739, pp. 284–303.
  ista: 'Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction.
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint
    Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.'
  mla: Froleyks, Nils, et al. “Certifying Phase Abstraction.” <i>Lecture Notes in
    Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i>, vol. 14739, Springer Nature, 2024, pp.
    284–303, doi:<a href="https://doi.org/10.1007/978-3-031-63498-7_17">10.1007/978-3-031-63498-7_17</a>.
  short: N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer
    Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture
    Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.
conference:
  end_date: 2024-07-06
  location: Nancy, France
  name: 'IJCAR: International Joint Conference on Automated Reasoning'
  start_date: 2024-07-03
date_created: 2024-08-11T22:01:13Z
date_published: 2024-07-01T00:00:00Z
date_updated: 2025-09-08T08:49:53Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-63498-7_17
ec_funded: 1
external_id:
  arxiv:
  - '2405.04297'
  isi:
  - '001273489700017'
file:
- access_level: open_access
  checksum: 7d7839fc8c5c680ea3ac09f40a66e55d
  content_type: application/pdf
  creator: dernst
  date_created: 2024-08-12T06:53:39Z
  date_updated: 2024-08-12T06:53:39Z
  file_id: '17414'
  file_name: 2024_LNCS_Froleyks.pdf
  file_size: 556902
  relation: main_file
  success: 1
file_date_updated: 2024-08-12T06:53:39Z
has_accepted_license: '1'
intvolume: '     14739'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 284-303
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
  in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031634970'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Certifying phase abstraction
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 14739
year: '2024'
...