---
_id: '14718'
abstract:
- lang: eng
  text: 'Binary decision diagrams (BDDs) are one of the fundamental data structures
    in formal methods and computer science in general. However, the performance of
    BDD-based algorithms greatly depends on memory latency due to the reliance on
    large hash tables and thus, by extension, on the speed of random memory access.
    This hinders the full utilisation of resources available on modern CPUs, since
    the absolute memory latency has not improved significantly for at least a decade.
    In this paper, we explore several implementation techniques that improve the performance
    of BDD manipulation either through enhanced memory locality or by partially eliminating
    random memory access. On a benchmark suite of 600+ BDDs derived from real-world
    applications, we demonstrate runtime that is comparable or better than parallelising
    the same operations on eight CPU cores. '
acknowledgement: "This work was supported by the European Union’s Horizon 2020 research
  and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 101034413
  and the\r\n“VAMOS” grant ERC-2020-AdG 101020093."
article_processing_charge: No
author:
- first_name: Samuel
  full_name: Pastva, Samuel
  id: 07c5ea74-f61c-11ec-a664-aa7c5d957b2b
  last_name: Pastva
  orcid: 0000-0003-1993-0331
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
citation:
  ama: 'Pastva S, Henzinger TA. Binary decision diagrams on modern hardware. In: <i>Proceedings
    of the 23rd Conference on Formal Methods in Computer-Aided Design</i>. TU Vienna
    Academic Press; 2023:122-131. doi:<a href="https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20">10.34727/2023/isbn.978-3-85448-060-0_20</a>'
  apa: 'Pastva, S., &#38; Henzinger, T. A. (2023). Binary decision diagrams on modern
    hardware. In <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
    Design</i> (pp. 122–131). Ames, IA, United States: TU Vienna Academic Press. <a
    href="https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20">https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>'
  chicago: Pastva, Samuel, and Thomas A Henzinger. “Binary Decision Diagrams on Modern
    Hardware.” In <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
    Design</i>, 122–31. TU Vienna Academic Press, 2023. <a href="https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20">https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>.
  ieee: S. Pastva and T. A. Henzinger, “Binary decision diagrams on modern hardware,”
    in <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design</i>,
    Ames, IA, United States, 2023, pp. 122–131.
  ista: 'Pastva S, Henzinger TA. 2023. Binary decision diagrams on modern hardware.
    Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design.
    FMCAD: Conference on Formal Methods in Computer-aided design, 122–131.'
  mla: Pastva, Samuel, and Thomas A. Henzinger. “Binary Decision Diagrams on Modern
    Hardware.” <i>Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
    Design</i>, TU Vienna Academic Press, 2023, pp. 122–31, doi:<a href="https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20">10.34727/2023/isbn.978-3-85448-060-0_20</a>.
  short: S. Pastva, T.A. Henzinger, in:, Proceedings of the 23rd Conference on Formal
    Methods in Computer-Aided Design, TU Vienna Academic Press, 2023, pp. 122–131.
conference:
  end_date: 2023-10-27
  location: Ames, IA, United States
  name: 'FMCAD: Conference on Formal Methods in Computer-aided design'
  start_date: 2023-10-25
date_created: 2023-12-31T23:01:03Z
date_published: 2023-10-01T00:00:00Z
date_updated: 2024-01-02T08:16:28Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2023/isbn.978-3-85448-060-0_20
ec_funded: 1
file:
- access_level: open_access
  checksum: 818d6e13dd508f3a04f0941081022e5d
  content_type: application/pdf
  creator: dernst
  date_created: 2024-01-02T08:14:23Z
  date_updated: 2024-01-02T08:14:23Z
  file_id: '14721'
  file_name: 2023_FMCAD_Pastva.pdf
  file_size: 524321
  relation: main_file
  success: 1
file_date_updated: 2024-01-02T08:14:23Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 122-131
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
  call_identifier: H2020
  grant_number: '101034413'
  name: 'IST-BRIDGE: International postdoctoral program'
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided
  Design
publication_identifier:
  isbn:
  - '9783854480600'
publication_status: published
publisher: TU Vienna Academic Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Binary decision diagrams on modern hardware
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
year: '2023'
...