---
_id: '10688'
abstract:
- lang: eng
  text: "Civl is a static verifier for concurrent programs designed around the conceptual
    framework of layered refinement,\r\nwhich views the task of verifying a program
    as a sequence of program simplification steps each justified by its own invariant.
    Civl verifies a layered concurrent program that compactly expresses all the programs
    in this sequence and the supporting invariants. This paper presents the design
    and implementation of the Civl verifier."
acknowledgement: This research was performed while Bernhard Kragl was at IST Austria,
  supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein
  Award).
alternative_title:
- Conference Series
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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: 'Kragl B, Qadeer S. The Civl verifier. In: Ruzica P, Whalen MW, eds. <i>Proceedings
    of the 21st Conference on Formal Methods in Computer-Aided Design</i>. Vol 2.
    TU Wien Academic Press; 2021:143–152. doi:<a href="https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23">10.34727/2021/isbn.978-3-85448-046-4_23</a>'
  apa: 'Kragl, B., &#38; Qadeer, S. (2021). The Civl verifier. In P. Ruzica &#38;
    M. W. Whalen (Eds.), <i>Proceedings of the 21st Conference on Formal Methods in
    Computer-Aided Design</i> (Vol. 2, pp. 143–152). Virtual: TU Wien Academic Press.
    <a href="https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23">https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23</a>'
  chicago: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” In <i>Proceedings
    of the 21st Conference on Formal Methods in Computer-Aided Design</i>, edited
    by Piskac Ruzica and Michael W. Whalen, 2:143–152. TU Wien Academic Press, 2021.
    <a href="https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23">https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23</a>.
  ieee: B. Kragl and S. Qadeer, “The Civl verifier,” in <i>Proceedings of the 21st
    Conference on Formal Methods in Computer-Aided Design</i>, Virtual, 2021, vol.
    2, pp. 143–152.
  ista: 'Kragl B, Qadeer S. 2021. The Civl verifier. Proceedings of the 21st Conference
    on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided
    Design, Conference Series, vol. 2, 143–152.'
  mla: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” <i>Proceedings of the
    21st Conference on Formal Methods in Computer-Aided Design</i>, edited by Piskac
    Ruzica and Michael W. Whalen, vol. 2, TU Wien Academic Press, 2021, pp. 143–152,
    doi:<a href="https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23">10.34727/2021/isbn.978-3-85448-046-4_23</a>.
  short: B. Kragl, S. Qadeer, in:, P. Ruzica, M.W. Whalen (Eds.), Proceedings of the
    21st Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press,
    2021, pp. 143–152.
conference:
  end_date: 2021-10-22
  location: Virtual
  name: 'FMCAD: Formal Methods in Computer-Aided Design'
  start_date: 2021-10-20
date_created: 2022-01-26T08:01:30Z
date_published: 2021-10-01T00:00:00Z
date_updated: 2022-01-26T08:20:41Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.34727/2021/isbn.978-3-85448-046-4_23
editor:
- first_name: Piskac
  full_name: Ruzica, Piskac
  last_name: Ruzica
- first_name: Michael W.
  full_name: Whalen, Michael W.
  last_name: Whalen
file:
- access_level: open_access
  checksum: 35438ac9f9750340b7f8ae4ae3220d9f
  content_type: application/pdf
  creator: cchlebak
  date_created: 2022-01-26T08:04:29Z
  date_updated: 2022-01-26T08:04:29Z
  file_id: '10689'
  file_name: 2021_FCAD2021_Kragl.pdf
  file_size: 390555
  relation: main_file
  success: 1
file_date_updated: 2022-01-26T08:04:29Z
has_accepted_license: '1'
intvolume: '         2'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 143–152
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Proceedings of the 21st Conference on Formal Methods in Computer-Aided
  Design
publication_identifier:
  isbn:
  - 978-3-85448-046-4
publication_status: published
publisher: TU Wien Academic Press
quality_controlled: '1'
status: public
title: The Civl verifier
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: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2021'
...
---
_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: '8195'
abstract:
- lang: eng
  text: This paper presents a foundation for refining concurrent programs with structured
    control flow. The verification problem is decomposed into subproblems that aid
    interactive program development, proof reuse, and automation. The formalization
    in this paper is the basis of a new design and implementation of the Civl verifier.
acknowledgement: "Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe
  Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award)."
alternative_title:
- LNCS
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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- 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: 'Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs.
    In: <i>Computer Aided Verification</i>. Vol 12224. Springer Nature; 2020:275-298.
    doi:<a href="https://doi.org/10.1007/978-3-030-53288-8_14">10.1007/978-3-030-53288-8_14</a>'
  apa: Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2020). Refinement for structured
    concurrent programs. In <i>Computer Aided Verification</i> (Vol. 12224, pp. 275–298).
    Springer Nature. <a href="https://doi.org/10.1007/978-3-030-53288-8_14">https://doi.org/10.1007/978-3-030-53288-8_14</a>
  chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured
    Concurrent Programs.” In <i>Computer Aided Verification</i>, 12224:275–98. Springer
    Nature, 2020. <a href="https://doi.org/10.1007/978-3-030-53288-8_14">https://doi.org/10.1007/978-3-030-53288-8_14</a>.
  ieee: B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent
    programs,” in <i>Computer Aided Verification</i>, 2020, vol. 12224, pp. 275–298.
  ista: Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent
    programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.
  mla: Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” <i>Computer
    Aided Verification</i>, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:<a
    href="https://doi.org/10.1007/978-3-030-53288-8_14">10.1007/978-3-030-53288-8_14</a>.
  short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer
    Nature, 2020, pp. 275–298.
date_created: 2020-08-03T11:45:35Z
date_published: 2020-07-14T00:00:00Z
date_updated: 2023-09-07T13:18:00Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-53288-8_14
external_id:
  isi:
  - '000695276000014'
file:
- access_level: open_access
  content_type: application/pdf
  creator: dernst
  date_created: 2020-08-06T08:14:54Z
  date_updated: 2020-08-06T08:14:54Z
  file_id: '8201'
  file_name: 2020_LNCS_Kragl.pdf
  file_size: 804237
  relation: main_file
  success: 1
file_date_updated: 2020-08-06T08:14:54Z
has_accepted_license: '1'
intvolume: '     12224'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 275-298
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Computer Aided Verification
publication_identifier:
  eisbn:
  - '9783030532888'
  eissn:
  - 1611-3349
  isbn:
  - '9783030532871'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Refinement for structured concurrent programs
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 12224
year: '2020'
...
---
_id: '8332'
abstract:
- lang: eng
  text: "Designing and verifying concurrent programs is a notoriously challenging,
    time consuming, and error prone task, even for experts. This is due to the sheer
    number of possible interleavings of a concurrent program, all of which have to
    be tracked and accounted for in a formal proof. Inventing an inductive invariant
    that captures all interleavings of a low-level implementation is theoretically
    possible, but practically intractable. We develop a refinement-based verification
    framework that provides mechanisms to simplify proof construction by decomposing
    the verification task into smaller subtasks.\r\n\r\nIn a first line of work, we
    present a foundation for refinement reasoning over structured concurrent programs.
    We introduce layered concurrent programs as a compact notation to represent multi-layer
    refinement proofs. A layered concurrent program specifies a sequence of connected
    concurrent programs, from most concrete to most abstract, such that common parts
    of different programs are written exactly once. Each program in this sequence
    is expressed as structured concurrent program, i.e., a program over (potentially
    recursive) procedures, imperative control flow, gated atomic actions, structured
    parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based
    verifiers, which represent concurrent systems as flat transition relations. We
    present a powerful refinement proof rule that decomposes refinement checking over
    structured programs into modular verification conditions. Refinement checking
    is supported by a new form of modular, parameterized invariants, called yield
    invariants, and a linear permission system to enhance local reasoning.\r\n\r\nIn
    a second line of work, we present two new reduction-based program transformations
    that target asynchronous programs. These transformations reduce the number of
    interleavings that need to be considered, thus reducing the complexity of invariants.
    Synchronization simplifies the verification of asynchronous programs by introducing
    the fiction, for proof purposes, that asynchronous operations complete synchronously.
    Synchronization summarizes an asynchronous computation as immediate atomic effect.
    Inductive sequentialization establishes sequential reductions 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.\r\n\r\nOur
    approach is implemented the CIVL verifier, which has been successfully used for
    the verification of several complex concurrent programs. In our methodology, the
    overall correctness of a program is established piecemeal by focusing on the invariant
    required for each refinement step separately. While the programmer does the creative
    work of specifying the chain of programs and the inductive invariant justifying
    each link in the chain, the tool automatically constructs the verification conditions
    underlying each refinement step."
alternative_title:
- ISTA Thesis
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
citation:
  ama: 'Kragl B. Verifying concurrent programs: Refinement, synchronization, sequentialization.
    2020. doi:<a href="https://doi.org/10.15479/AT:ISTA:8332">10.15479/AT:ISTA:8332</a>'
  apa: 'Kragl, B. (2020). <i>Verifying concurrent programs: Refinement, synchronization,
    sequentialization</i>. Institute of Science and Technology Austria. <a href="https://doi.org/10.15479/AT:ISTA:8332">https://doi.org/10.15479/AT:ISTA:8332</a>'
  chicago: 'Kragl, Bernhard. “Verifying Concurrent Programs: Refinement, Synchronization,
    Sequentialization.” Institute of Science and Technology Austria, 2020. <a href="https://doi.org/10.15479/AT:ISTA:8332">https://doi.org/10.15479/AT:ISTA:8332</a>.'
  ieee: 'B. Kragl, “Verifying concurrent programs: Refinement, synchronization, sequentialization,”
    Institute of Science and Technology Austria, 2020.'
  ista: 'Kragl B. 2020. Verifying concurrent programs: Refinement, synchronization,
    sequentialization. Institute of Science and Technology Austria.'
  mla: 'Kragl, Bernhard. <i>Verifying Concurrent Programs: Refinement, Synchronization,
    Sequentialization</i>. Institute of Science and Technology Austria, 2020, doi:<a
    href="https://doi.org/10.15479/AT:ISTA:8332">10.15479/AT:ISTA:8332</a>.'
  short: 'B. Kragl, Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization,
    Institute of Science and Technology Austria, 2020.'
date_created: 2020-09-04T12:24:12Z
date_published: 2020-09-03T00:00:00Z
date_updated: 2023-09-13T08:45:08Z
day: '03'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:8332
file:
- access_level: open_access
  checksum: 26fe261550f691280bda4c454bf015c7
  content_type: application/pdf
  creator: bkragl
  date_created: 2020-09-04T12:17:47Z
  date_updated: 2020-09-04T12:17:47Z
  file_id: '8333'
  file_name: kragl-thesis.pdf
  file_size: 1348815
  relation: main_file
- access_level: closed
  checksum: b9694ce092b7c55557122adba8337ebc
  content_type: application/zip
  creator: bkragl
  date_created: 2020-09-04T13:00:17Z
  date_updated: 2020-09-04T13:00:17Z
  file_id: '8335'
  file_name: kragl-thesis.zip
  file_size: 372312
  relation: source_file
file_date_updated: 2020-09-04T13:00:17Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '120'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '133'
    relation: part_of_dissertation
    status: public
  - id: '8012'
    relation: part_of_dissertation
    status: public
  - id: '8195'
    relation: part_of_dissertation
    status: public
  - id: '160'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
title: 'Verifying concurrent programs: Refinement, synchronization, sequentialization'
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2020'
...
---
_id: '7348'
abstract:
- lang: eng
  text: 'The monitoring of event frequencies can be used to recognize behavioral anomalies,
    to identify trends, and to deduce or discard hypotheses about the underlying system.
    For example, the performance of a web server may be monitored based on the ratio
    of the total count of requests from the least and most active clients. Exact frequency
    monitoring, however, can be prohibitively expensive; in the above example it would
    require as many counters as there are clients. In this paper, we propose the efficient
    probabilistic monitoring of common frequency properties, including the mode (i.e.,
    the most common event) and the median of an event sequence. We define a logic
    to express composite frequency properties as a combination of atomic frequency
    properties. Our main contribution is an algorithm that, under suitable probabilistic
    assumptions, can be used to monitor these important frequency properties with
    four counters, independent of the number of different events. Our algorithm samples
    longer and longer subwords of an infinite event sequence. We prove the almost-sure
    convergence of our algorithm by generalizing ergodic theory from increasing-length
    prefixes to increasing-length subwords of an infinite sequence. A similar algorithm
    could be used to learn a connected Markov chain of a given structure from observing
    its outputs, to arbitrary precision, for a given confidence. '
alternative_title:
- LIPIcs
article_number: '20'
article_processing_charge: No
arxiv: 1
author:
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- 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: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
citation:
  ama: 'Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: <i>28th
    EACSL Annual Conference on Computer Science Logic</i>. Vol 152. Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik; 2020. doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2020.20">10.4230/LIPIcs.CSL.2020.20</a>'
  apa: 'Ferrere, T., Henzinger, T. A., &#38; Kragl, B. (2020). Monitoring event frequencies.
    In <i>28th EACSL Annual Conference on Computer Science Logic</i> (Vol. 152). Barcelona,
    Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CSL.2020.20">https://doi.org/10.4230/LIPIcs.CSL.2020.20</a>'
  chicago: Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event
    Frequencies.” In <i>28th EACSL Annual Conference on Computer Science Logic</i>,
    Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href="https://doi.org/10.4230/LIPIcs.CSL.2020.20">https://doi.org/10.4230/LIPIcs.CSL.2020.20</a>.
  ieee: T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,”
    in <i>28th EACSL Annual Conference on Computer Science Logic</i>, Barcelona, Spain,
    2020, vol. 152.
  ista: 'Ferrere T, Henzinger TA, Kragl B. 2020. Monitoring event frequencies. 28th
    EACSL Annual Conference on Computer Science Logic. CSL: Computer Science Logic,
    LIPIcs, vol. 152, 20.'
  mla: Ferrere, Thomas, et al. “Monitoring Event Frequencies.” <i>28th EACSL Annual
    Conference on Computer Science Logic</i>, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2020, doi:<a href="https://doi.org/10.4230/LIPIcs.CSL.2020.20">10.4230/LIPIcs.CSL.2020.20</a>.
  short: T. Ferrere, T.A. Henzinger, B. Kragl, in:, 28th EACSL Annual Conference on
    Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
conference:
  end_date: 2020-01-16
  location: Barcelona, Spain
  name: 'CSL: Computer Science Logic'
  start_date: 2020-01-13
date_created: 2020-01-21T11:22:21Z
date_published: 2020-01-15T00:00:00Z
date_updated: 2021-01-12T08:13:12Z
day: '15'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CSL.2020.20
external_id:
  arxiv:
  - '1910.06097'
file:
- access_level: open_access
  checksum: b9a691d658d075c6369d3304d17fb818
  content_type: application/pdf
  creator: bkragl
  date_created: 2020-01-21T11:21:04Z
  date_updated: 2020-07-14T12:47:56Z
  file_id: '7349'
  file_name: main.pdf
  file_size: 617206
  relation: main_file
file_date_updated: 2020-07-14T12:47:56Z
has_accepted_license: '1'
intvolume: '       152'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: 28th EACSL Annual Conference on Computer Science Logic
publication_identifier:
  isbn:
  - '9783959771320'
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: 1
status: public
title: Monitoring event frequencies
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: 152
year: '2020'
...
---
_id: '160'
abstract:
- lang: eng
  text: We present layered concurrent programs, a compact and expressive notation
    for specifying refinement proofs of concurrent programs. A layered concurrent
    program specifies a sequence of connected concurrent programs, from most concrete
    to most abstract, such that common parts of different programs are written exactly
    once. These programs are expressed in the ordinary syntax of imperative concurrent
    programs using gated atomic actions, sequencing, choice, and (recursive) procedure
    calls. Each concurrent program is automatically extracted from the layered program.
    We reduce refinement to the safety of a sequence of concurrent checker programs,
    one each to justify the connection between every two consecutive concurrent programs.
    These checker programs are also automatically extracted from the layered program.
    Layered concurrent programs have been implemented in the CIVL verifier which has
    been successfully used for the verification of several complex concurrent programs.
alternative_title:
- LNCS
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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: 'Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102.
    doi:<a href="https://doi.org/10.1007/978-3-319-96145-3_5">10.1007/978-3-319-96145-3_5</a>'
  apa: 'Kragl, B., &#38; Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981,
    pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer.
    <a href="https://doi.org/10.1007/978-3-319-96145-3_5">https://doi.org/10.1007/978-3-319-96145-3_5</a>'
  chicago: Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102.
    Springer, 2018. <a href="https://doi.org/10.1007/978-3-319-96145-3_5">https://doi.org/10.1007/978-3-319-96145-3_5</a>.
  ieee: 'B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV:
    Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.'
  ista: 'Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided
    Verification, LNCS, vol. 10981, 79–102.'
  mla: Kragl, Bernhard, and Shaz Qadeer. <i>Layered Concurrent Programs</i>. Vol.
    10981, Springer, 2018, pp. 79–102, doi:<a href="https://doi.org/10.1007/978-3-319-96145-3_5">10.1007/978-3-319-96145-3_5</a>.
  short: B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102.
conference:
  end_date: 2018-07-17
  location: Oxford, UK
  name: 'CAV: Computer Aided Verification'
  start_date: 2018-07-14
date_created: 2018-12-11T11:44:57Z
date_published: 2018-07-18T00:00:00Z
date_updated: 2023-09-13T08:45:09Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-96145-3_5
external_id:
  isi:
  - '000491481600005'
file:
- access_level: open_access
  checksum: c64fff560fe5a7532ec10626ad1c215e
  content_type: application/pdf
  creator: dernst
  date_created: 2018-12-17T12:52:12Z
  date_updated: 2020-07-14T12:45:04Z
  file_id: '5705'
  file_name: 2018_LNCS_Kragl.pdf
  file_size: 1603844
  relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: '     10981'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 79 - 102
project:
- _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: Springer
publist_id: '7761'
quality_controlled: '1'
related_material:
  record:
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Layered Concurrent Programs
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10981
year: '2018'
...
---
_id: '133'
abstract:
- lang: eng
  text: Synchronous programs are easy to specify because the side effects of an operation
    are finished by the time the invocation of the operation returns to the caller.
    Asynchronous programs, on the other hand, are difficult to specify because there
    are side effects due to pending computation scheduled as a result of the invocation
    of an operation. They are also difficult to verify because of the large number
    of possible interleavings of concurrent computation threads. We present synchronization,
    a new proof rule that simplifies the verification of asynchronous programs by
    introducing the fiction, for proof purposes, that asynchronous operations complete
    synchronously. Synchronization summarizes an asynchronous computation as immediate
    atomic effect. Modular verification is enabled via pending asynchronous calls
    in atomic summaries, and a complementary proof rule that eliminates pending asynchronous
    calls when components and their specifications are composed. We evaluate synchronization
    in the context of a multi-layer refinement verification methodology on a collection
    of benchmark programs.
alternative_title:
- LIPIcs
article_number: '21'
author:
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- 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: 'Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118.
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">10.4230/LIPIcs.CONCUR.2018.21</a>'
  apa: 'Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2018). Synchronizing the asynchronous
    (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory,
    Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>'
  chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the
    Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
    <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>.
  ieee: 'B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,”
    presented at the CONCUR: International Conference on Concurrency Theory, Beijing,
    China, 2018, vol. 118.'
  ista: 'Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR:
    International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.'
  mla: Kragl, Bernhard, et al. <i>Synchronizing the Asynchronous</i>. Vol. 118, 21,
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">10.4230/LIPIcs.CONCUR.2018.21</a>.
  short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2018.
conference:
  end_date: 2018-09-07
  location: Beijing, China
  name: 'CONCUR: International Conference on Concurrency Theory'
  start_date: 2018-09-04
date_created: 2018-12-11T11:44:48Z
date_published: 2018-08-13T00:00:00Z
date_updated: 2023-09-07T13:18:00Z
day: '13'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CONCUR.2018.21
file:
- access_level: open_access
  checksum: c90895f4c5fafc18ddc54d1c8848077e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:46Z
  date_updated: 2020-07-14T12:44:44Z
  file_id: '5368'
  file_name: IST-2018-853-v2+2_concur2018.pdf
  file_size: 745438
  relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: '       118'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
publication_identifier:
  issn:
  - '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7790'
pubrep_id: '1039'
quality_controlled: '1'
related_material:
  record:
  - id: '6426'
    relation: earlier_version
    status: public
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: 1
status: public
title: Synchronizing the asynchronous
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: 118
year: '2018'
...
---
_id: '6426'
abstract:
- lang: eng
  text: Synchronous programs are easy to specify because the side effects of an operation
    are finished by the time the invocation of the operation returns to the caller.
    Asynchronous programs, on the other hand, are difficult to specify because there
    are side effects due to pending computation scheduled as a result of the invocation
    of an operation. They are also difficult to verify because of the large number
    of possible interleavings of concurrent asynchronous computation threads. We show
    that specifications and correctness proofs for asynchronous programs can be structured
    by introducing the fiction, for proof purposes, that intermediate, non-quiescent
    states of asynchronous operations can be ignored. Then, the task of specification
    becomes relatively simple and the task of verification can be naturally decomposed
    into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure
    of an asynchronous program, the atomic effect of non-atomic operations and the
    synchronous effect of asynchronous operations. This structuring of specifications
    and proofs corresponds to the introduction of multiple layers of stepwise refinement
    for asynchronous programs. We present the first proof rule, called synchronization,
    to reduce asynchronous invocations on a lower layer to synchronous invocations
    on a higher layer. We implemented our proof method in CIVL and evaluated it on
    a collection of benchmark programs.
alternative_title:
- IST Austria Technical Report
author:
- 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: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: Henzinger TA, Kragl B, Qadeer S. <i>Synchronizing the Asynchronous</i>. IST
    Austria; 2017. doi:<a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">10.15479/AT:IST-2018-853-v2-2</a>
  apa: Henzinger, T. A., Kragl, B., &#38; Qadeer, S. (2017). <i>Synchronizing the
    asynchronous</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">https://doi.org/10.15479/AT:IST-2018-853-v2-2</a>
  chicago: Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. <i>Synchronizing
    the Asynchronous</i>. IST Austria, 2017. <a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">https://doi.org/10.15479/AT:IST-2018-853-v2-2</a>.
  ieee: T. A. Henzinger, B. Kragl, and S. Qadeer, <i>Synchronizing the asynchronous</i>.
    IST Austria, 2017.
  ista: Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST
    Austria, 28p.
  mla: Henzinger, Thomas A., et al. <i>Synchronizing the Asynchronous</i>. IST Austria,
    2017, doi:<a href="https://doi.org/10.15479/AT:IST-2018-853-v2-2">10.15479/AT:IST-2018-853-v2-2</a>.
  short: T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST
    Austria, 2017.
date_created: 2019-05-13T08:15:55Z
date_published: 2017-08-04T00:00:00Z
date_updated: 2023-02-21T16:59:21Z
day: '04'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2018-853-v2-2
file:
- access_level: open_access
  checksum: b48d42725182d7ca10107a118815f4cf
  content_type: application/pdf
  creator: dernst
  date_created: 2019-05-13T08:14:44Z
  date_updated: 2020-07-14T12:47:30Z
  file_id: '6431'
  file_name: main(1).pdf
  file_size: 971347
  relation: main_file
file_date_updated: 2020-07-14T12:47:30Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: '28'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
related_material:
  record:
  - id: '133'
    relation: later_version
    status: public
status: public
title: Synchronizing the asynchronous
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '1011'
abstract:
- lang: eng
  text: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly
    equivalent, are standard models for interprocedural analysis. Yet RSMs are more
    convenient as they (a) explicitly model function calls and returns, and (b) specify
    many natural parameters for algorithmic analysis, e.g., the number of entries
    and exits. We consider a general framework where RSM transitions are labeled from
    a semiring and path properties are algebraic with semiring operations, which can
    model, e.g., interprocedural reachability and dataflow analysis problems. Our
    main contributions are new algorithms for several fundamental problems. As compared
    to a direct translation of RSMs to PDSs and the best-known existing bounds of
    PDSs, our analysis algorithm improves the complexity for finite-height semirings
    (that subsumes reachability and standard dataflow properties). We further consider
    the problem of extracting distance values from the representation structures computed
    by our algorithm, and give efficient algorithms that distinguish the complexity
    of a one-time preprocessing from the complexity of each individual query. Another
    advantage of our algorithm is that our improvements carry over to the concurrent
    setting, where we improve the bestknown complexity for the context-bounded analysis
    of concurrent RSMs. Finally, we provide a prototype implementation that gives
    a significant speed-up on several benchmarks from the SLAM/SDV project.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Samarth
  full_name: Mishra, Samarth
  last_name: Mishra
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted
    recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a
    href="https://doi.org/10.1007/978-3-662-54434-1_11">10.1007/978-3-662-54434-1_11</a>'
  apa: 'Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster
    algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201,
    pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala,
    Sweden: Springer. <a href="https://doi.org/10.1007/978-3-662-54434-1_11">https://doi.org/10.1007/978-3-662-54434-1_11</a>'
  chicago: Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis.
    “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok
    Yang, 10201:287–313. Springer, 2017. <a href="https://doi.org/10.1007/978-3-662-54434-1_11">https://doi.org/10.1007/978-3-662-54434-1_11</a>.
  ieee: 'K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms
    for weighted recursive state machines,” presented at the ESOP: European Symposium
    on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.'
  ista: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms
    for weighted recursive state machines. ESOP: European Symposium on Programming,
    LNCS, vol. 10201, 287–313.'
  mla: Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive
    State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
    doi:<a href="https://doi.org/10.1007/978-3-662-54434-1_11">10.1007/978-3-662-54434-1_11</a>.
  short: K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.),
    Springer, 2017, pp. 287–313.
conference:
  end_date: 2017-04-29
  location: Uppsala, Sweden
  name: 'ESOP: European Symposium on Programming'
  start_date: 2017-04-22
date_created: 2018-12-11T11:49:41Z
date_published: 2017-03-19T00:00:00Z
date_updated: 2023-09-22T09:44:50Z
day: '19'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-54434-1_11
ec_funded: 1
editor:
- first_name: Hongseok
  full_name: Yang, Hongseok
  last_name: Yang
external_id:
  isi:
  - '000681702400011'
intvolume: '     10201'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1701.04914
month: '03'
oa: 1
oa_version: Submitted Version
page: 287 - 313
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
  issn:
  - '03029743'
publication_status: published
publisher: Springer
publist_id: '6384'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for weighted recursive state machines
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10201
year: '2017'
...
---
_id: '1872'
abstract:
- lang: eng
  text: Extensionality axioms are common when reasoning about data collections, such
    as arrays and functions in program analysis, or sets in mathematics. An extensionality
    axiom asserts that two collections are equal if they consist of the same elements
    at the same indices. Using extensionality is often required to show that two collections
    are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly,
    while humans have no problem with proving such set identities using extensionality,
    they are very hard for superposition theorem provers because of the calculi they
    use. In this paper we show how addition of a new inference rule, called extensionality
    resolution, allows first-order theorem provers to easily solve problems no modern
    first-order theorem prover can solve. We illustrate this by running the VAMPIRE
    theorem prover with extensionality resolution on a number of set theory and array
    problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP
    library of first-order problems that were never solved before by any prover.
acknowledgement: This research was supported in part by the Austrian National Research
  Network RiSE (S11410-N23).
alternative_title:
- LNCS
author:
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Laura
  full_name: Kovács, Laura
  last_name: Kovács
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Andrei
  full_name: Voronkov, Andrei
  last_name: Voronkov
citation:
  ama: 'Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity.
    In: Cassez F, Raskin J-F, eds. <i>ATVA 2014</i>. Vol 8837. Springer; 2014:185-200.
    doi:<a href="https://doi.org/10.1007/978-3-319-11936-6_14">10.1007/978-3-319-11936-6_14</a>'
  apa: 'Gupta, A., Kovács, L., Kragl, B., &#38; Voronkov, A. (2014). Extensional crisis
    and proving identity. In F. Cassez &#38; J.-F. Raskin (Eds.), <i>ATVA 2014</i>
    (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. <a href="https://doi.org/10.1007/978-3-319-11936-6_14">https://doi.org/10.1007/978-3-319-11936-6_14</a>'
  chicago: Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional
    Crisis and Proving Identity.” In <i>ATVA 2014</i>, edited by Franck Cassez and
    Jean-François Raskin, 8837:185–200. Springer, 2014. <a href="https://doi.org/10.1007/978-3-319-11936-6_14">https://doi.org/10.1007/978-3-319-11936-6_14</a>.
  ieee: A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving
    identity,” in <i>ATVA 2014</i>, Sydney, Australia, 2014, vol. 8837, pp. 185–200.
  ista: 'Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving
    identity. ATVA 2014. ATVA: Automated Technology for Verification and Analysis,
    LNCS, vol. 8837, 185–200.'
  mla: Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” <i>ATVA
    2014</i>, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer,
    2014, pp. 185–200, doi:<a href="https://doi.org/10.1007/978-3-319-11936-6_14">10.1007/978-3-319-11936-6_14</a>.
  short: A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, F. Cassez, J.-F. Raskin
    (Eds.), ATVA 2014, Springer, 2014, pp. 185–200.
conference:
  end_date: 2014-11-07
  location: Sydney, Australia
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2014-11-03
date_created: 2018-12-11T11:54:28Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2021-01-12T06:53:45Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-11936-6_14
ec_funded: 1
editor:
- first_name: Franck
  full_name: Cassez, Franck
  last_name: Cassez
- first_name: Jean-François
  full_name: Raskin, Jean-François
  last_name: Raskin
file:
- access_level: open_access
  checksum: af4bd3fc1f4c93075e4dc5cbf625fe7b
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:10:15Z
  date_updated: 2020-07-14T12:45:19Z
  file_id: '4801'
  file_name: IST-2016-641-v1+1_atva2014.pdf
  file_size: 244294
  relation: main_file
file_date_updated: 2020-07-14T12:45:19Z
has_accepted_license: '1'
intvolume: '      8837'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 185 - 200
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
publication: ATVA 2014
publication_status: published
publisher: Springer
publist_id: '5226'
pubrep_id: '641'
quality_controlled: '1'
scopus_import: 1
status: public
title: Extensional crisis and proving identity
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 8837
year: '2014'
...
---
_id: '2237'
abstract:
- lang: eng
  text: We describe new extensions of the Vampire theorem prover for computing tree
    interpolants. These extensions generalize Craig interpolation in Vampire, and
    can also be used to derive sequence interpolants. We evaluated our implementation
    on a large number of examples over the theory of linear integer arithmetic and
    integer-indexed arrays, with and without quantifiers. When compared to other methods,
    our experiments show that some examples could only be solved by our implementation.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Régis
  full_name: Blanc, Régis
  last_name: Blanc
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Laura
  full_name: Kovács, Laura
  last_name: Kovács
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
citation:
  ama: Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181.
    doi:<a href="https://doi.org/10.1007/978-3-642-45221-5_13">10.1007/978-3-642-45221-5_13</a>
  apa: 'Blanc, R., Gupta, A., Kovács, L., &#38; Kragl, B. (2013). Tree interpolation
    in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence,
    and Reasoning, Stellenbosch, South Africa: Springer. <a href="https://doi.org/10.1007/978-3-642-45221-5_13">https://doi.org/10.1007/978-3-642-45221-5_13</a>'
  chicago: Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation
    in Vampire.” Lecture Notes in Computer Science. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-45221-5_13">https://doi.org/10.1007/978-3-642-45221-5_13</a>.
  ieee: R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,”
    vol. 8312. Springer, pp. 173–181, 2013.
  ista: Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire.
    8312, 173–181.
  mla: Blanc, Régis, et al. <i>Tree Interpolation in Vampire</i>. Vol. 8312, Springer,
    2013, pp. 173–81, doi:<a href="https://doi.org/10.1007/978-3-642-45221-5_13">10.1007/978-3-642-45221-5_13</a>.
  short: R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.
conference:
  end_date: 2013-12-19
  location: Stellenbosch, South Africa
  name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
  start_date: 2013-12-14
date_created: 2018-12-11T11:56:29Z
date_published: 2013-01-14T00:00:00Z
date_updated: 2020-08-11T10:09:42Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-45221-5_13
file:
- access_level: open_access
  checksum: 9cebaafca032e6769d273f393305c705
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T11:10:40Z
  date_updated: 2020-07-14T12:45:34Z
  file_id: '7858'
  file_name: 2013_LPAR_Blanc.pdf
  file_size: 279206
  relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: '      8312'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 173 - 181
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '4724'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Tree interpolation in Vampire
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8312
year: '2013'
...