---
_id: '1439'
abstract:
- lang: eng
  text: Fault-tolerant distributed algorithms play an important role in many critical/high-availability
    applications. These algorithms are notoriously difficult to implement correctly,
    due to asynchronous communication and the occurrence of faults, such as the network
    dropping messages or computers crashing. We introduce PSYNC, a domain specific
    language based on the Heard-Of model, which views asynchronous faulty systems
    as synchronous ones with an adversarial environment that simulates asynchrony
    and faults by dropping messages. We define a runtime system for PSYNC that efficiently
    executes on asynchronous networks. We formalize the relation between the runtime
    system and PSYNC in terms of observational refinement. The high-level lockstep
    abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant
    distributed algorithms and enables automated formal verification. We have implemented
    an embedding of PSYNC in the SCALA programming language with a runtime system
    for asynchronous networks. We show the applicability of PSYNC by implementing
    several important fault-tolerant distributed algorithms and we compare the implementation
    of consensus algorithms in PSYNC against implementations in other languages in
    terms of code size, runtime efficiency, and verification.
acknowledgement: 'Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192
  and FA8650-15-C-7564) and NSF (Grant CCF-1138967). '
alternative_title:
- ACM SIGPLAN Notices
author:
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- 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: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: 'Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language
    for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:<a
    href="https://doi.org/10.1145/2837614.2837650">10.1145/2837614.2837650</a>'
  apa: 'Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2016). PSYNC: A partially
    synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp.
    400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg,
    FL, USA: ACM. <a href="https://doi.org/10.1145/2837614.2837650">https://doi.org/10.1145/2837614.2837650</a>'
  chicago: 'Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “PSYNC: A Partially
    Synchronous Language for Fault-Tolerant Distributed Algorithms,” 20–22:400–415.
    ACM, 2016. <a href="https://doi.org/10.1145/2837614.2837650">https://doi.org/10.1145/2837614.2837650</a>.'
  ieee: 'C. Dragoi, T. A. Henzinger, and D. Zufferey, “PSYNC: A partially synchronous
    language for fault-tolerant distributed algorithms,” presented at the POPL: Principles
    of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 400–415.'
  ista: 'Dragoi C, Henzinger TA, Zufferey D. 2016. PSYNC: A partially synchronous
    language for fault-tolerant distributed algorithms. POPL: Principles of Programming
    Languages, ACM SIGPLAN Notices, vol. 20–22, 400–415.'
  mla: 'Dragoi, Cezara, et al. <i>PSYNC: A Partially Synchronous Language for Fault-Tolerant
    Distributed Algorithms</i>. Vol. 20–22, ACM, 2016, pp. 400–15, doi:<a href="https://doi.org/10.1145/2837614.2837650">10.1145/2837614.2837650</a>.'
  short: C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415.
conference:
  end_date: 2016-01-22
  location: St. Petersburg, FL, USA
  name: 'POPL: Principles of Programming Languages'
  start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2021-01-12T06:50:45Z
day: '11'
department:
- _id: ToHe
doi: 10.1145/2837614.2837650
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://hal.inria.fr/hal-01251199/
month: '01'
oa: 1
oa_version: Preprint
page: 400 - 415
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: ACM
publist_id: '5759'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'PSYNC: A partially synchronous language for fault-tolerant distributed algorithms'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1498'
abstract:
- lang: eng
  text: Fault-tolerant distributed algorithms play an important role in many critical/high-availability
    applications. These algorithms are notoriously difficult to implement correctly,
    due to asynchronous communication and the occurrence of faults, such as the network
    dropping messages or computers crashing. Nonetheless there is surprisingly little
    language and verification support to build distributed systems based on fault-tolerant
    algorithms. In this paper, we present some of the challenges that a designer has
    to overcome to implement a fault-tolerant distributed system. Then we review different
    models that have been proposed to reason about distributed algorithms and sketch
    how such a model can form the basis for a domain-specific programming language.
    Adopting a high-level programming model can simplify the programmer's life and
    make the code amenable to automated verification, while still compiling to efficiently
    executable code. We conclude by summarizing the current status of an ongoing language
    design and implementation project that is based on this idea.
alternative_title:
- LIPIcs
author:
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- 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: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant
    distributed systems. 2015;32:90-102. doi:<a href="https://doi.org/10.4230/LIPIcs.SNAPL.2015.90">10.4230/LIPIcs.SNAPL.2015.90</a>
  apa: 'Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2015). The need for language
    support for fault-tolerant distributed systems. Presented at the SNAPL: Summit
    oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.SNAPL.2015.90">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>'
  chicago: Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for
    Language Support for Fault-Tolerant Distributed Systems.” Leibniz International
    Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2015. <a href="https://doi.org/10.4230/LIPIcs.SNAPL.2015.90">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>.
  ieee: C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support
    for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, pp. 90–102, 2015.
  ista: Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for
    fault-tolerant distributed systems. 32, 90–102.
  mla: Dragoi, Cezara, et al. <i>The Need for Language Support for Fault-Tolerant
    Distributed Systems</i>. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2015, pp. 90–102, doi:<a href="https://doi.org/10.4230/LIPIcs.SNAPL.2015.90">10.4230/LIPIcs.SNAPL.2015.90</a>.
  short: C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.
conference:
  end_date: 2015-05-06
  location: Asilomar, CA, United States
  name: 'SNAPL: Summit oN Advances in Programming Languages'
  start_date: 2015-05-03
date_created: 2018-12-11T11:52:22Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2020-08-11T10:09:14Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.SNAPL.2015.90
ec_funded: 1
file:
- access_level: open_access
  checksum: cf5e94baa89a2dc4c5de01abc676eda8
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:02Z
  date_updated: 2020-07-14T12:44:58Z
  file_id: '5050'
  file_name: IST-2016-499-v1+1_9.pdf
  file_size: 489362
  relation: main_file
file_date_updated: 2020-07-14T12:44:58Z
has_accepted_license: '1'
intvolume: '        32'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '01'
oa: 1
oa_version: Published Version
page: 90 - 102
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_identifier:
  isbn:
  - '978-3-939897-80-4 '
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5681'
pubrep_id: '499'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: The need for language support for fault-tolerant distributed systems
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: 32
year: '2015'
...
---
_id: '1392'
abstract:
- lang: eng
  text: Fault-tolerant distributed algorithms play an important role in ensuring the
    reliability of many software applications. In this paper we consider distributed
    algorithms whose computations are organized in rounds. To verify the correctness
    of such algorithms, we reason about (i) properties (such as invariants) of the
    state, (ii) the transitions controlled by the algorithm, and (iii) the communication
    graph. We introduce a logic that addresses these points, and contains set comprehensions
    with cardinality constraints, function symbols to describe the local states of
    each process, and a limited form of quantifier alternation to express the verification
    conditions. We show its use in automating the verification of consensus algorithms.
    In particular, we give a semi-decision procedure for the unsatisfiability problem
    of the logic and identify a decidable fragment. We successfully applied our framework
    to verify the correctness of a variety of consensus algorithms tolerant to both
    benign faults (message loss, process crashes) and value faults (message corruption).
acknowledgement: Supported by the Vienna Science and Technology Fund (WWTF) through
  grant PROSEED.
alternative_title:
- LNCS
author:
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- 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: Helmut
  full_name: Veith, Helmut
  last_name: Veith
- first_name: Josef
  full_name: Widder, Josef
  last_name: Widder
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework
    for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:<a
    href="https://doi.org/10.1007/978-3-642-54013-4_10">10.1007/978-3-642-54013-4_10</a>'
  apa: 'Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., &#38; Zufferey, D. (2014).
    A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181).
    Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
    San Diego, USA: Springer. <a href="https://doi.org/10.1007/978-3-642-54013-4_10">https://doi.org/10.1007/978-3-642-54013-4_10</a>'
  chicago: Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien
    Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81.
    Springer, 2014. <a href="https://doi.org/10.1007/978-3-642-54013-4_10">https://doi.org/10.1007/978-3-642-54013-4_10</a>.
  ieee: 'C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based
    framework for verifying consensus algorithms,” presented at the VMCAI: Verification,
    Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp.
    161–181.'
  ista: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based
    framework for verifying consensus algorithms. VMCAI: Verification, Model Checking
    and Abstract Interpretation, LNCS, vol. 8318, 161–181.'
  mla: Dragoi, Cezara, et al. <i>A Logic-Based Framework for Verifying Consensus Algorithms</i>.
    Vol. 8318, Springer, 2014, pp. 161–81, doi:<a href="https://doi.org/10.1007/978-3-642-54013-4_10">10.1007/978-3-642-54013-4_10</a>.
  short: C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer,
    2014, pp. 161–181.
conference:
  end_date: 2014-01-21
  location: San Diego, USA
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
  start_date: 2014-01-19
date_created: 2018-12-11T11:51:45Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:50:22Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-54013-4_10
ec_funded: 1
file:
- access_level: open_access
  checksum: bffa33d39be77df0da39defe97eabf84
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:06Z
  date_updated: 2020-07-14T12:44:48Z
  file_id: '4859'
  file_name: IST-2014-179-v1+1_vmcai14.pdf
  file_size: 444138
  relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: '      8318'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 161 - 181
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5817'
pubrep_id: '179'
quality_controlled: '1'
scopus_import: 1
status: public
title: A logic-based framework for verifying consensus algorithms
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...
---
_id: '2298'
abstract:
- lang: eng
  text: "We present a shape analysis for programs that manipulate overlaid data structures
    which share sets of objects. The abstract domain contains Separation Logic formulas
    that (1) combine a per-object separating conjunction with a per-field separating
    conjunction and (2) constrain a set of variables interpreted as sets of objects.
    The definition of the abstract domain operators is based on a notion of homomorphism
    between formulas, viewed as graphs, used recently to define optimal decision procedures
    for fragments of the Separation Logic. Based on a Frame Rule that supports the
    two versions of the separating conjunction, the analysis is able to reason in
    a modular manner about non-overlaid data structures and then, compose information
    only at a few program points, e.g., procedure returns. We have implemented this
    analysis in a prototype tool and applied it on several interesting case studies
    that manipulate overlaid and nested linked lists.\r\n"
alternative_title:
- LNCS
author:
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Mihaela
  full_name: Sighireanu, Mihaela
  last_name: Sighireanu
citation:
  ama: 'Dragoi C, Enea C, Sighireanu M. Local shape analysis for overlaid data structures.
    In: Vol 7935. Springer; 2013:150-171. doi:<a href="https://doi.org/10.1007/978-3-642-38856-9_10">10.1007/978-3-642-38856-9_10</a>'
  apa: 'Dragoi, C., Enea, C., &#38; Sighireanu, M. (2013). Local shape analysis for
    overlaid data structures (Vol. 7935, pp. 150–171). Presented at the SAS: Static
    Analysis Symposium, Seattle, WA, United States: Springer. <a href="https://doi.org/10.1007/978-3-642-38856-9_10">https://doi.org/10.1007/978-3-642-38856-9_10</a>'
  chicago: Dragoi, Cezara, Constantin Enea, and Mihaela Sighireanu. “Local Shape Analysis
    for Overlaid Data Structures,” 7935:150–71. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-38856-9_10">https://doi.org/10.1007/978-3-642-38856-9_10</a>.
  ieee: 'C. Dragoi, C. Enea, and M. Sighireanu, “Local shape analysis for overlaid
    data structures,” presented at the SAS: Static Analysis Symposium, Seattle, WA,
    United States, 2013, vol. 7935, pp. 150–171.'
  ista: 'Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data
    structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.'
  mla: Dragoi, Cezara, et al. <i>Local Shape Analysis for Overlaid Data Structures</i>.
    Vol. 7935, Springer, 2013, pp. 150–71, doi:<a href="https://doi.org/10.1007/978-3-642-38856-9_10">10.1007/978-3-642-38856-9_10</a>.
  short: C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.
conference:
  end_date: 2013-06-22
  location: Seattle, WA, United States
  name: 'SAS: Static Analysis Symposium'
  start_date: 2013-06-20
date_created: 2018-12-11T11:56:50Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:56:36Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-38856-9_10
ec_funded: 1
file:
- access_level: open_access
  checksum: 907edd33a5892e3af093365f1fd57ed7
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:10:36Z
  date_updated: 2020-07-14T12:45:37Z
  file_id: '4824'
  file_name: IST-2014-196-v1+1_sas13.pdf
  file_size: 299004
  relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: '      7935'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 150 - 171
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4630'
pubrep_id: '196'
quality_controlled: '1'
scopus_import: 1
status: public
title: Local shape analysis for overlaid data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7935
year: '2013'
...
---
_id: '5747'
article_processing_charge: No
author:
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- 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: 'Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent
    Objects with Cooperating Updates. In: <i>Computer Aided Verification</i>. Vol
    8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:<a
    href="https://doi.org/10.1007/978-3-642-39799-8_11">10.1007/978-3-642-39799-8_11</a>'
  apa: 'Dragoi, C., Gupta, A., &#38; Henzinger, T. A. (2013). Automatic Linearizability
    Proofs of Concurrent Objects with Cooperating Updates. In <i>Computer Aided Verification</i>
    (Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href="https://doi.org/10.1007/978-3-642-39799-8_11">https://doi.org/10.1007/978-3-642-39799-8_11</a>'
  chicago: 'Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability
    Proofs of Concurrent Objects with Cooperating Updates.” In <i>Computer Aided Verification</i>,
    8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. <a href="https://doi.org/10.1007/978-3-642-39799-8_11">https://doi.org/10.1007/978-3-642-39799-8_11</a>.'
  ieee: 'C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs
    of Concurrent Objects with Cooperating Updates,” in <i>Computer Aided Verification</i>,
    vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190.'
  ista: 'Dragoi C, Gupta A, Henzinger TA. 2013.Automatic Linearizability Proofs of
    Concurrent Objects with Cooperating Updates. In: Computer Aided Verification.
    vol. 8044, 174–190.'
  mla: Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects
    with Cooperating Updates.” <i>Computer Aided Verification</i>, vol. 8044, Springer
    Berlin Heidelberg, 2013, pp. 174–90, doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_11">10.1007/978-3-642-39799-8_11</a>.
  short: C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer
    Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.
conference:
  end_date: 2013-07-19
  location: Saint Petersburg, Russia
  name: CAV 2013
  start_date: 2013-07-13
date_created: 2018-12-18T13:10:21Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2023-09-05T14:16:07Z
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39799-8_11
ec_funded: 1
file:
- access_level: open_access
  checksum: a901cc6b71db08b61c0d4c0cbacc6287
  content_type: application/pdf
  creator: dernst
  date_created: 2018-12-18T13:13:33Z
  date_updated: 2020-07-14T12:47:10Z
  file_id: '5748'
  file_name: 2013_CAV_Dragoi.pdf
  file_size: 236480
  relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: '      8044'
language:
- iso: eng
oa: 1
oa_version: None
page: 174-190
place: Berlin, Heidelberg
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: Computer Aided Verification
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783642397981'
  - '9783642397998'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
pubrep_id: '195'
quality_controlled: '1'
scopus_import: '1'
series_title: CAV
status: public
title: Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 8044
year: '2013'
...
---
_id: '3253'
abstract:
- lang: eng
  text: We describe a framework for reasoning about programs with lists carrying integer
    numerical data. We use abstract domains to describe and manipulate complex constraints
    on configurations of these programs mixing constraints on the shape of the heap,
    sizes of the lists, on the multisets of data stored in these lists, and on the
    data at their different positions. Moreover, we provide powerful techniques for
    automatic validation of Hoare-triples and invariant checking, as well as for automatic
    synthesis of invariants and procedure summaries using modular inter-procedural
    analysis. The approach has been implemented in a tool called Celia and experimented
    successfully on a large benchmark of programs.
acknowledgement: This work was partly supported by the French National Research Agency
  (ANR) project Veridyc (ANR-09-SEGI-016).
alternative_title:
- LNCS
author:
- first_name: Ahmed
  full_name: Bouajjani, Ahmed
  last_name: Bouajjani
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Mihaela
  full_name: Sighireanu, Mihaela
  last_name: Sighireanu
citation:
  ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Abstract domains for automated
    reasoning about list manipulating programs with infinite data. In: Vol 7148. Springer;
    2012:1-22. doi:<a href="https://doi.org/10.1007/978-3-642-27940-9_1">10.1007/978-3-642-27940-9_1</a>'
  apa: 'Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Abstract
    domains for automated reasoning about list manipulating programs with infinite
    data (Vol. 7148, pp. 1–22). Presented at the VMCAI: Verification, Model Checking
    and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href="https://doi.org/10.1007/978-3-642-27940-9_1">https://doi.org/10.1007/978-3-642-27940-9_1</a>'
  chicago: Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
    “Abstract Domains for Automated Reasoning about List Manipulating Programs with
    Infinite Data,” 7148:1–22. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-27940-9_1">https://doi.org/10.1007/978-3-642-27940-9_1</a>.
  ieee: 'A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Abstract domains for
    automated reasoning about list manipulating programs with infinite data,” presented
    at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia,
    PA, USA, 2012, vol. 7148, pp. 1–22.'
  ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Abstract domains for automated
    reasoning about list manipulating programs with infinite data. VMCAI: Verification,
    Model Checking and Abstract Interpretation, LNCS, vol. 7148, 1–22.'
  mla: Bouajjani, Ahmed, et al. <i>Abstract Domains for Automated Reasoning about
    List Manipulating Programs with Infinite Data</i>. Vol. 7148, Springer, 2012,
    pp. 1–22, doi:<a href="https://doi.org/10.1007/978-3-642-27940-9_1">10.1007/978-3-642-27940-9_1</a>.
  short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2012, pp.
    1–22.
conference:
  end_date: 2012-01-24
  location: Philadelphia, PA, USA
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
  start_date: 2012-01-22
date_created: 2018-12-11T12:02:17Z
date_published: 2012-02-26T00:00:00Z
date_updated: 2021-01-12T07:42:09Z
day: '26'
department:
- _id: ToHe
doi: 10.1007/978-3-642-27940-9_1
intvolume: '      7148'
language:
- iso: eng
month: '02'
oa_version: None
page: 1 - 22
publication_status: published
publisher: Springer
publist_id: '3404'
quality_controlled: '1'
status: public
title: Abstract domains for automated reasoning about list manipulating programs with
  infinite data
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7148
year: '2012'
...
---
_id: '10903'
abstract:
- lang: eng
  text: We propose a logic-based framework for automated reasoning about sequential
    programs manipulating singly-linked lists and arrays with unbounded data. We introduce
    the logic SLAD, which allows combining shape constraints, written in a fragment
    of Separation Logic, with data and size constraints. We address the problem of
    checking the entailment between SLAD formulas, which is crucial in performing
    pre-post condition reasoning. Although this problem is undecidable in general
    for SLAD, we propose a sound and powerful procedure that is able to solve this
    problem for a large class of formulas, beyond the capabilities of existing techniques
    and tools. We prove that this procedure is complete, i.e., it is actually a decision
    procedure for this problem, for an important fragment of SLAD including known
    decidable logics. We implemented this procedure and shown its preciseness and
    its efficiency on a significant benchmark of formulas.
acknowledgement: This work has been partially supported by the French ANR project
  Veridyc
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ahmed
  full_name: Bouajjani, Ahmed
  last_name: Bouajjani
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Mihaela
  full_name: Sighireanu, Mihaela
  last_name: Sighireanu
citation:
  ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for
    programs manipulating lists and arrays with infinite data. In: <i>Automated Technology
    for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer;
    2012:167-182. doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_14">10.1007/978-3-642-33386-6_14</a>'
  apa: 'Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate
    invariant checking for programs manipulating lists and arrays with infinite data.
    In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182).
    Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-33386-6_14">https://doi.org/10.1007/978-3-642-33386-6_14</a>'
  chicago: 'Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
    “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite
    Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82.
    LNCS. Berlin, Heidelberg: Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33386-6_14">https://doi.org/10.1007/978-3-642-33386-6_14</a>.'
  ieee: A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking
    for programs manipulating lists and arrays with infinite data,” in <i>Automated
    Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012,
    vol. 7561, pp. 167–182.
  ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking
    for programs manipulating lists and arrays with infinite data. Automated Technology
    for Verification and Analysis. ATVA: Automated Technology for Verification and
    AnalysisLNCS, LNCS, vol. 7561, 167–182.'
  mla: Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating
    Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification
    and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_14">10.1007/978-3-642-33386-6_14</a>.
  short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology
    for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.
conference:
  end_date: 2012-10-06
  location: Thiruvananthapuram, India
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2012-10-03
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2023-09-05T14:07:24Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_14
intvolume: '      7561'
language:
- iso: eng
month: '10'
oa_version: None
page: 167-182
place: Berlin, Heidelberg
publication: Automated Technology for Verification and Analysis
publication_identifier:
  eisbn:
  - '9783642333866'
  eissn:
  - 1611-3349
  isbn:
  - '9783642333859'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Accurate invariant checking for programs manipulating lists and arrays with
  infinite data
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...