---
_id: '11459'
abstract:
- lang: eng
  text: 'We present a novel approach to differential cost analysis that, given a program
    revision, attempts to statically bound the difference in resource usage, or cost,
    between the two program versions. Differential cost analysis is particularly interesting
    because of the many compelling applications for it, such as detecting resource-use
    regressions at code-review time or proving the absence of certain side-channel
    vulnerabilities. One prior approach to differential cost analysis is to apply
    relational reasoning that conceptually constructs a product program on which one
    can over-approximate the difference in costs between the two program versions.
    However, a significant challenge in any relational approach is effectively aligning
    the program versions to get precise results. In this paper, our key insight is
    that we can avoid the need for and the limitations of program alignment if, instead,
    we bound the difference of two cost-bound summaries rather than directly bounding
    the concrete cost difference. In particular, our method computes a threshold value
    for the maximal difference in cost between two program versions simultaneously
    using two kinds of cost-bound summaries---a potential function that evaluates
    to an upper bound for the cost incurred in the first program and an anti-potential
    function that evaluates to a lower bound for the cost incurred in the second.
    Our method has a number of desirable properties: it can be fully automated, it
    allows optimizing the threshold value on relative cost, it is suitable for programs
    that are not syntactically similar, and it supports non-determinism. We have evaluated
    an implementation of our approach on a number of program pairs collected from
    the literature, and we find that our method computes tight threshold values on
    relative cost in most examples.'
acknowledgement: "We thank Shaun Willows, Thomas Lugnet, and the Living Room Application
  Vending team for suggesting threshold\r\nbounds as a developer-friendly way to interact
  with a differential cost analyzer, and we thank Jim Christy, Daniel\r\nSchoepe,
  and the Prime Video Automated Reasoning team for their support and helpful suggestions
  throughout the\r\nproject. We also thank Michael Emmi for feedback on an earlier
  version of this paper. And finally, we thank the anonymous reviewers for their useful
  feedback and Aws Albarghouthi for shepherding the final version of the paper. Ðorđe
  Žikelić was also partially supported by ERC CoG 863818 (FoRM-SMArt)."
article_processing_charge: No
arxiv: 1
author:
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
- first_name: Bor-Yuh Evan
  full_name: Chang, Bor-Yuh Evan
  last_name: Chang
- first_name: Pauline
  full_name: Bolignano, Pauline
  last_name: Bolignano
- first_name: Franco
  full_name: Raimondi, Franco
  last_name: Raimondi
citation:
  ama: 'Zikelic D, Chang B-YE, Bolignano P, Raimondi F. Differential cost analysis
    with simultaneous potentials and anti-potentials. In: <i>Proceedings of the 43rd
    ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>.
    Association for Computing Machinery; 2022:442-457. doi:<a href="https://doi.org/10.1145/3519939.3523435">10.1145/3519939.3523435</a>'
  apa: 'Zikelic, D., Chang, B.-Y. E., Bolignano, P., &#38; Raimondi, F. (2022). Differential
    cost analysis with simultaneous potentials and anti-potentials. In <i>Proceedings
    of the 43rd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation</i> (pp. 442–457). San Diego, CA, United States: Association
    for Computing Machinery. <a href="https://doi.org/10.1145/3519939.3523435">https://doi.org/10.1145/3519939.3523435</a>'
  chicago: Zikelic, Dorde, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi.
    “Differential Cost Analysis with Simultaneous Potentials and Anti-Potentials.”
    In <i>Proceedings of the 43rd ACM SIGPLAN International Conference on Programming
    Language Design and Implementation</i>, 442–57. Association for Computing Machinery,
    2022. <a href="https://doi.org/10.1145/3519939.3523435">https://doi.org/10.1145/3519939.3523435</a>.
  ieee: D. Zikelic, B.-Y. E. Chang, P. Bolignano, and F. Raimondi, “Differential cost
    analysis with simultaneous potentials and anti-potentials,” in <i>Proceedings
    of the 43rd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation</i>, San Diego, CA, United States, 2022, pp. 442–457.
  ista: 'Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis
    with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM
    SIGPLAN International Conference on Programming Language Design and Implementation.
    PLDI: Programming Language Design and Implementation, 442–457.'
  mla: Zikelic, Dorde, et al. “Differential Cost Analysis with Simultaneous Potentials
    and Anti-Potentials.” <i>Proceedings of the 43rd ACM SIGPLAN International Conference
    on Programming Language Design and Implementation</i>, Association for Computing
    Machinery, 2022, pp. 442–57, doi:<a href="https://doi.org/10.1145/3519939.3523435">10.1145/3519939.3523435</a>.
  short: D. Zikelic, B.-Y.E. Chang, P. Bolignano, F. Raimondi, in:, Proceedings of
    the 43rd ACM SIGPLAN International Conference on Programming Language Design and
    Implementation, Association for Computing Machinery, 2022, pp. 442–457.
conference:
  end_date: 2022-06-17
  location: San Diego, CA, United States
  name: 'PLDI: Programming Language Design and Implementation'
  start_date: 2022-06-13
date_created: 2022-06-21T09:26:15Z
date_published: 2022-06-09T00:00:00Z
date_updated: 2025-07-14T09:09:54Z
day: '09'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1145/3519939.3523435
ec_funded: 1
external_id:
  arxiv:
  - '2204.00870'
  isi:
  - '000850435600030'
file:
- access_level: open_access
  checksum: 7eb915a2ca5b5ce4729321f33b2e16e1
  content_type: application/pdf
  creator: dernst
  date_created: 2022-06-27T07:38:21Z
  date_updated: 2022-06-27T07:38:21Z
  file_id: '11466'
  file_name: 2022_PLDI_Zikelic.pdf
  file_size: 318697
  relation: main_file
  success: 1
file_date_updated: 2022-06-27T07:38:21Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '06'
oa: 1
oa_version: Published Version
page: 442-457
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming
  Language Design and Implementation
publication_identifier:
  isbn:
  - '9781450392655'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Differential cost analysis with simultaneous potentials and anti-potentials
tmp:
  image: /images/cc_by_nc_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
    (CC BY-NC-ND 4.0)
  short: CC BY-NC-ND (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2022'
...