---
_id: '8012'
abstract:
- lang: eng
  text: Asynchronous programs are notoriously difficult to reason about because they
    spawn computation tasks which take effect asynchronously in a nondeterministic
    way. Devising inductive invariants for such programs requires understanding and
    stating complex relationships between an unbounded number of computation tasks
    in arbitrarily long executions. In this paper, we introduce inductive sequentialization,
    a new proof rule that sidesteps this complexity via a sequential reduction, a
    sequential program that captures every behavior of the original program up to
    reordering of coarse-grained commutative actions. A sequential reduction of a
    concurrent program is easy to reason about since it corresponds to a simple execution
    of the program in an idealized synchronous environment, where processes act in
    a fixed order and at the same speed. We have implemented and integrated our proof
    rule in the CIVL verifier, allowing us to provably derive fine-grained implementations
    of asynchronous programs. We have successfully applied our proof rule to a diverse
    set of message-passing protocols, including leader election protocols, two-phase
    commit, and Paxos.
article_processing_charge: No
author:
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Suha Orhun
  full_name: Mutluergil, Suha Orhun
  last_name: Mutluergil
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: 'Kragl B, Enea C, Henzinger TA, Mutluergil SO, Qadeer S. Inductive sequentialization
    of asynchronous programs. In: <i>Proceedings of the 41st ACM SIGPLAN Conference
    on Programming Language Design and Implementation</i>. Association for Computing
    Machinery; 2020:227-242. doi:<a href="https://doi.org/10.1145/3385412.3385980">10.1145/3385412.3385980</a>'
  apa: 'Kragl, B., Enea, C., Henzinger, T. A., Mutluergil, S. O., &#38; Qadeer, S.
    (2020). Inductive sequentialization of asynchronous programs. In <i>Proceedings
    of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>
    (pp. 227–242). London, United Kingdom: Association for Computing Machinery. <a
    href="https://doi.org/10.1145/3385412.3385980">https://doi.org/10.1145/3385412.3385980</a>'
  chicago: Kragl, Bernhard, Constantin Enea, Thomas A Henzinger, Suha Orhun Mutluergil,
    and Shaz Qadeer. “Inductive Sequentialization of Asynchronous Programs.” In <i>Proceedings
    of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>,
    227–42. Association for Computing Machinery, 2020. <a href="https://doi.org/10.1145/3385412.3385980">https://doi.org/10.1145/3385412.3385980</a>.
  ieee: B. Kragl, C. Enea, T. A. Henzinger, S. O. Mutluergil, and S. Qadeer, “Inductive
    sequentialization of asynchronous programs,” in <i>Proceedings of the 41st ACM
    SIGPLAN Conference on Programming Language Design and Implementation</i>, London,
    United Kingdom, 2020, pp. 227–242.
  ista: 'Kragl B, Enea C, Henzinger TA, Mutluergil SO, Qadeer S. 2020. Inductive sequentialization
    of asynchronous programs. Proceedings of the 41st ACM SIGPLAN Conference on Programming
    Language Design and Implementation. PLDI: Programming Language Design and Implementation,
    227–242.'
  mla: Kragl, Bernhard, et al. “Inductive Sequentialization of Asynchronous Programs.”
    <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
    and Implementation</i>, Association for Computing Machinery, 2020, pp. 227–42,
    doi:<a href="https://doi.org/10.1145/3385412.3385980">10.1145/3385412.3385980</a>.
  short: B. Kragl, C. Enea, T.A. Henzinger, S.O. Mutluergil, S. Qadeer, in:, Proceedings
    of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation,
    Association for Computing Machinery, 2020, pp. 227–242.
conference:
  end_date: 2020-06-20
  location: London, United Kingdom
  name: 'PLDI: Programming Language Design and Implementation'
  start_date: 2020-06-15
date_created: 2020-06-25T11:40:16Z
date_published: 2020-06-01T00:00:00Z
date_updated: 2023-09-07T13:18:00Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3385412.3385980
external_id:
  isi:
  - '000614622300016'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1145/3385412.3385980
month: '06'
oa: 1
oa_version: Published Version
page: 227-242
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language
  Design and Implementation
publication_identifier:
  isbn:
  - '9781450376136'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Inductive sequentialization of asynchronous programs
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2020'
...
---
_id: '8089'
abstract:
- lang: eng
  text: "We consider the classical problem of invariant generation for programs with
    polynomial assignments and focus on synthesizing invariants that are a conjunction
    of strict polynomial inequalities. We present a sound and semi-complete method
    based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize
    positive polynomials over a semi-algebraic set.\r\n\r\nOn the theoretical side,
    the worst-case complexity of our approach is subexponential, whereas the worst-case
    complexity of the previous complete method (Kapur, ACA 2004) is doubly-exponential.
    Even when restricted to linear invariants, the best previous complexity for complete
    invariant generation is exponential (Colon et al, CAV 2003). On the practical
    side, we reduce the invariant generation problem to quadratic programming (QCLP),
    which is a classical optimization problem with many industrial solvers. We demonstrate
    the applicability of our approach by providing experimental results on several
    academic benchmarks. To the best of our knowledge, the only previous invariant
    generation method that provides completeness guarantees for invariants consisting
    of polynomial inequalities is (Kapur, ACA 2004), which relies on quantifier elimination
    and cannot even handle toy programs such as our running example."
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Ehsan Kafshdar
  full_name: Goharshady, Ehsan Kafshdar
  last_name: Goharshady
citation:
  ama: 'Chatterjee K, Fu H, Goharshady AK, Goharshady EK. Polynomial invariant generation
    for non-deterministic recursive programs. In: <i>Proceedings of the 41st ACM SIGPLAN
    Conference on Programming Language Design and Implementation</i>. Association
    for Computing Machinery; 2020:672-687. doi:<a href="https://doi.org/10.1145/3385412.3385969">10.1145/3385412.3385969</a>'
  apa: 'Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Goharshady, E. K. (2020).
    Polynomial invariant generation for non-deterministic recursive programs. In <i>Proceedings
    of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>
    (pp. 672–687). London, United Kingdom: Association for Computing Machinery. <a
    href="https://doi.org/10.1145/3385412.3385969">https://doi.org/10.1145/3385412.3385969</a>'
  chicago: Chatterjee, Krishnendu, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan
    Kafshdar Goharshady. “Polynomial Invariant Generation for Non-Deterministic Recursive
    Programs.” In <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming
    Language Design and Implementation</i>, 672–87. Association for Computing Machinery,
    2020. <a href="https://doi.org/10.1145/3385412.3385969">https://doi.org/10.1145/3385412.3385969</a>.
  ieee: K. Chatterjee, H. Fu, A. K. Goharshady, and E. K. Goharshady, “Polynomial
    invariant generation for non-deterministic recursive programs,” in <i>Proceedings
    of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation</i>,
    London, United Kingdom, 2020, pp. 672–687.
  ista: 'Chatterjee K, Fu H, Goharshady AK, Goharshady EK. 2020. Polynomial invariant
    generation for non-deterministic recursive programs. Proceedings of the 41st ACM
    SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Programming
    Language Design and Implementation, 672–687.'
  mla: Chatterjee, Krishnendu, et al. “Polynomial Invariant Generation for Non-Deterministic
    Recursive Programs.” <i>Proceedings of the 41st ACM SIGPLAN Conference on Programming
    Language Design and Implementation</i>, Association for Computing Machinery, 2020,
    pp. 672–87, doi:<a href="https://doi.org/10.1145/3385412.3385969">10.1145/3385412.3385969</a>.
  short: K. Chatterjee, H. Fu, A.K. Goharshady, E.K. Goharshady, in:, Proceedings
    of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation,
    Association for Computing Machinery, 2020, pp. 672–687.
conference:
  end_date: 2020-06-20
  location: London, United Kingdom
  name: 'PLDI: Programming Language Design and Implementation'
  start_date: 2020-06-15
date_created: 2020-07-05T22:00:45Z
date_published: 2020-06-11T00:00:00Z
date_updated: 2025-06-02T08:53:42Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/3385412.3385969
external_id:
  arxiv:
  - '1902.04373'
  isi:
  - '000614622300045'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1902.04373
month: '06'
oa: 1
oa_version: Preprint
page: 672-687
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language
  Design and Implementation
publication_identifier:
  isbn:
  - '9781450376136'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Polynomial invariant generation for non-deterministic recursive programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2020'
...