---
_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. Proceedings
of the 21st Conference on Formal Methods in Computer-Aided Design. Vol 2.
TU Wien Academic Press; 2021:143–152. doi:10.34727/2021/isbn.978-3-85448-046-4_23'
apa: 'Kragl, B., & Qadeer, S. (2021). The Civl verifier. In P. Ruzica &
M. W. Whalen (Eds.), Proceedings of the 21st Conference on Formal Methods in
Computer-Aided Design (Vol. 2, pp. 143–152). Virtual: TU Wien Academic Press.
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23'
chicago: Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” In Proceedings
of the 21st Conference on Formal Methods in Computer-Aided Design, edited
by Piskac Ruzica and Michael W. Whalen, 2:143–152. TU Wien Academic Press, 2021.
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23.
ieee: B. Kragl and S. Qadeer, “The Civl verifier,” in Proceedings of the 21st
Conference on Formal Methods in Computer-Aided Design, 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.” Proceedings of the
21st Conference on Formal Methods in Computer-Aided Design, edited by Piskac
Ruzica and Michael W. Whalen, vol. 2, TU Wien Academic Press, 2021, pp. 143–152,
doi:10.34727/2021/isbn.978-3-85448-046-4_23.
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
license: https://creativecommons.org/licenses/by/4.0/
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: '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
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: 28th
EACSL Annual Conference on Computer Science Logic. Vol 152. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CSL.2020.20'
apa: 'Ferrere, T., Henzinger, T. A., & Kragl, B. (2020). Monitoring event frequencies.
In 28th EACSL Annual Conference on Computer Science Logic (Vol. 152). Barcelona,
Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2020.20'
chicago: Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event
Frequencies.” In 28th EACSL Annual Conference on Computer Science Logic,
Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CSL.2020.20.
ieee: T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,”
in 28th EACSL Annual Conference on Computer Science Logic, 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.” 28th EACSL Annual
Conference on Computer Science Logic, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2020, doi:10.4230/LIPIcs.CSL.2020.20.
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: '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: Computer Aided Verification. Vol 12224. Springer Nature; 2020:275-298.
doi:10.1007/978-3-030-53288-8_14'
apa: Kragl, B., Qadeer, S., & Henzinger, T. A. (2020). Refinement for structured
concurrent programs. In Computer Aided Verification (Vol. 12224, pp. 275–298).
Springer Nature. https://doi.org/10.1007/978-3-030-53288-8_14
chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured
Concurrent Programs.” In Computer Aided Verification, 12224:275–98. Springer
Nature, 2020. https://doi.org/10.1007/978-3-030-53288-8_14.
ieee: B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent
programs,” in Computer Aided Verification, 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.” Computer
Aided Verification, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:10.1007/978-3-030-53288-8_14.
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: '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: Proceedings of the 41st ACM SIGPLAN Conference
on Programming Language Design and Implementation. Association for Computing
Machinery; 2020:227-242. doi:10.1145/3385412.3385980'
apa: 'Kragl, B., Enea, C., Henzinger, T. A., Mutluergil, S. O., & Qadeer, S.
(2020). Inductive sequentialization of asynchronous programs. In Proceedings
of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
(pp. 227–242). London, United Kingdom: Association for Computing Machinery. https://doi.org/10.1145/3385412.3385980'
chicago: Kragl, Bernhard, Constantin Enea, Thomas A Henzinger, Suha Orhun Mutluergil,
and Shaz Qadeer. “Inductive Sequentialization of Asynchronous Programs.” In Proceedings
of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation,
227–42. Association for Computing Machinery, 2020. https://doi.org/10.1145/3385412.3385980.
ieee: B. Kragl, C. Enea, T. A. Henzinger, S. O. Mutluergil, and S. Qadeer, “Inductive
sequentialization of asynchronous programs,” in Proceedings of the 41st ACM
SIGPLAN Conference on Programming Language Design and Implementation, 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.”
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
and Implementation, Association for Computing Machinery, 2020, pp. 227–42,
doi:10.1145/3385412.3385980.
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: '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:10.15479/AT:ISTA:8332'
apa: 'Kragl, B. (2020). Verifying concurrent programs: Refinement, synchronization,
sequentialization. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8332'
chicago: 'Kragl, Bernhard. “Verifying Concurrent Programs: Refinement, Synchronization,
Sequentialization.” Institute of Science and Technology Austria, 2020. https://doi.org/10.15479/AT:ISTA:8332.'
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. Verifying Concurrent Programs: Refinement, Synchronization,
Sequentialization. Institute of Science and Technology Austria, 2020, doi:10.15479/AT:ISTA:8332.'
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: '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:10.4230/LIPIcs.CONCUR.2018.21'
apa: 'Kragl, B., Qadeer, S., & 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. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21'
chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the
Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
https://doi.org/10.4230/LIPIcs.CONCUR.2018.21.
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. Synchronizing the Asynchronous. Vol. 118, 21,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.21.
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: '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:10.1007/978-3-319-96145-3_5'
apa: 'Kragl, B., & Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981,
pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer.
https://doi.org/10.1007/978-3-319-96145-3_5'
chicago: Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102.
Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_5.
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. Layered Concurrent Programs. Vol.
10981, Springer, 2018, pp. 79–102, doi:10.1007/978-3-319-96145-3_5.
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: '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. Synchronizing the Asynchronous. IST
Austria; 2017. doi:10.15479/AT:IST-2018-853-v2-2
apa: Henzinger, T. A., Kragl, B., & Qadeer, S. (2017). Synchronizing the
asynchronous. IST Austria. https://doi.org/10.15479/AT:IST-2018-853-v2-2
chicago: Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. Synchronizing
the Asynchronous. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2018-853-v2-2.
ieee: T. A. Henzinger, B. Kragl, and S. Qadeer, Synchronizing the asynchronous.
IST Austria, 2017.
ista: Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST
Austria, 28p.
mla: Henzinger, Thomas A., et al. Synchronizing the Asynchronous. IST Austria,
2017, doi:10.15479/AT:IST-2018-853-v2-2.
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:10.1007/978-3-662-54434-1_11'
apa: 'Chatterjee, K., Kragl, B., Mishra, S., & 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. https://doi.org/10.1007/978-3-662-54434-1_11'
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. https://doi.org/10.1007/978-3-662-54434-1_11.
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. Faster Algorithms for Weighted Recursive
State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
doi:10.1007/978-3-662-54434-1_11.
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. ATVA 2014. Vol 8837. Springer; 2014:185-200.
doi:10.1007/978-3-319-11936-6_14'
apa: 'Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional crisis
and proving identity. In F. Cassez & J.-F. Raskin (Eds.), ATVA 2014
(Vol. 8837, pp. 185–200). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_14'
chicago: Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional
Crisis and Proving Identity.” In ATVA 2014, edited by Franck Cassez and
Jean-François Raskin, 8837:185–200. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_14.
ieee: A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving
identity,” in ATVA 2014, 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.” ATVA
2014, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer,
2014, pp. 185–200, doi:10.1007/978-3-319-11936-6_14.
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:10.1007/978-3-642-45221-5_13
apa: 'Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree interpolation
in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_13'
chicago: Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation
in Vampire.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_13.
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. Tree Interpolation in Vampire. Vol. 8312, Springer,
2013, pp. 173–81, doi:10.1007/978-3-642-45221-5_13.
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'
...