---
_id: '2239'
abstract:
- lang: eng
text: The analysis of the energy consumption of software is an important goal for
quantitative formal methods. Current methods, using weighted transition systems
or energy games, model the energy source as an ideal resource whose status is
characterized by one number, namely the amount of remaining energy. Real batteries,
however, exhibit behaviors that can deviate substantially from an ideal energy
resource. Based on a discretization of a standard continuous battery model, we
introduce battery transition systems. In this model, a battery is viewed as consisting
of two parts-the available-charge tank and the bound-charge tank. Any charge or
discharge is applied to the available-charge tank. Over time, the energy from
each tank diffuses to the other tank. Battery transition systems are infinite
state systems that, being not well-structured, fall into no decidable class that
is known to us. Nonetheless, we are able to prove that the !-regular modelchecking
problem is decidable for battery transition systems. We also present a case study
on the verification of control programs for energy-constrained semi-autonomous
robots.
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol
49. ACM; 2014:595-606. doi:10.1145/2535838.2535875'
apa: 'Boker, U., Henzinger, T. A., & Radhakrishna, A. (2014). Battery transition
systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming
Languages, San Diego, USA: ACM. https://doi.org/10.1145/2535838.2535875'
chicago: Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition
Systems,” 49:595–606. ACM, 2014. https://doi.org/10.1145/2535838.2535875.
ieee: 'U. Boker, T. A. Henzinger, and A. Radhakrishna, “Battery transition systems,”
presented at the POPL: Principles of Programming Languages, San Diego, USA, 2014,
vol. 49, no. 1, pp. 595–606.'
ista: 'Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems.
POPL: Principles of Programming Languages vol. 49, 595–606.'
mla: Boker, Udi, et al. Battery Transition Systems. Vol. 49, no. 1, ACM,
2014, pp. 595–606, doi:10.1145/2535838.2535875.
short: U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.
conference:
end_date: 2014-01-24
location: San Diego, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2014-01-22
date_created: 2018-12-11T11:56:30Z
date_published: 2014-01-13T00:00:00Z
date_updated: 2021-01-12T06:56:13Z
day: '13'
department:
- _id: ToHe
doi: 10.1145/2535838.2535875
ec_funded: 1
intvolume: ' 49'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 595 - 606
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_identifier:
isbn:
- 978-145032544-8
publication_status: published
publisher: ACM
publist_id: '4722'
quality_controlled: '1'
scopus_import: 1
status: public
title: Battery transition systems
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 49
year: '2014'
...
---
_id: '1376'
abstract:
- lang: eng
text: 'We consider the distributed synthesis problem for temporal logic specifications.
Traditionally, the problem has been studied for LTL, and the previous results
show that the problem is decidable iff there is no information fork in the architecture.
We consider the problem for fragments of LTL and our main results are as follows:
(1) We show that the problem is undecidable for architectures with information
forks even for the fragment of LTL with temporal operators restricted to next
and eventually. (2) For specifications restricted to globally along with non-nested
next operators, we establish decidability (in EXPSPACE) for star architectures
where the processes receive disjoint inputs, whereas we establish undecidability
for architectures containing an information fork-meet structure. (3) Finally,
we consider LTL without the next operator, and establish decidability (NEXPTIME-complete)
for all architectures for a fragment that consists of a set of safety assumptions,
and a set of guarantees where each guarantee is a safety, reachability, or liveness
condition.'
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- 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, Henzinger TA, Otop J, Pavlogiannis A. Distributed synthesis
for LTL fragments. In: 13th International Conference on Formal Methods in Computer-Aided
Design. IEEE; 2013:18-25. doi:10.1109/FMCAD.2013.6679386'
apa: 'Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013).
Distributed synthesis for LTL fragments. In 13th International Conference on
Formal Methods in Computer-Aided Design (pp. 18–25). Portland, OR, United
States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679386'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis.
“Distributed Synthesis for LTL Fragments.” In 13th International Conference
on Formal Methods in Computer-Aided Design, 18–25. IEEE, 2013. https://doi.org/10.1109/FMCAD.2013.6679386.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, “Distributed
synthesis for LTL fragments,” in 13th International Conference on Formal Methods
in Computer-Aided Design, Portland, OR, United States, 2013, pp. 18–25.
ista: 'Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis
for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided
Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25.'
mla: Chatterjee, Krishnendu, et al. “Distributed Synthesis for LTL Fragments.” 13th
International Conference on Formal Methods in Computer-Aided Design, IEEE,
2013, pp. 18–25, doi:10.1109/FMCAD.2013.6679386.
short: K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International
Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25.
conference:
end_date: 2013-10-23
location: Portland, OR, United States
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2013-10-20
date_created: 2018-12-11T11:51:40Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2023-02-23T12:24:53Z
day: '11'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679386
ec_funded: 1
language:
- iso: eng
month: '12'
oa_version: None
page: 18 - 25
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 13th International Conference on Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5835'
quality_controlled: '1'
related_material:
record:
- id: '5406'
relation: earlier_version
status: public
status: public
title: Distributed synthesis for LTL fragments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1385'
abstract:
- lang: eng
text: It is often difficult to correctly implement a Boolean controller for a complex
system, especially when concurrency is involved. Yet, it may be easy to formally
specify a controller. For instance, for a pipelined processor it suffices to state
that the visible behavior of the pipelined system should be identical to a non-pipelined
reference system (Burch-Dill paradigm). We present a novel procedure to efficiently
synthesize multiple Boolean control signals from a specification given as a quantified
first-order formula (with a specific quantifier structure). Our approach uses
uninterpreted functions to abstract details of the design. We construct an unsatisfiable
SMT formula from the given specification. Then, from just one proof of unsatisfiability,
we use a variant of Craig interpolation to compute multiple coordinated interpolants
that implement the Boolean control signals. Our method avoids iterative learning
and back-substitution of the control functions. We applied our approach to synthesize
a controller for a simple two-stage pipelined processor, and present first experimental
results.
acknowledgement: "This research was supported by the European Commission through project\r\nDIAMOND
\ (FP7-2009-IST-4-248613), and QUAINT (I774-N23), "
arxiv: 1
author:
- first_name: Georg
full_name: Hofferek, Georg
last_name: Hofferek
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Jie
full_name: Jiang, Jie
last_name: Jiang
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
citation:
ama: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple
boolean functions using interpolation on a single proof. In: 2013 Formal Methods
in Computer-Aided Design. IEEE; 2013:77-84. doi:10.1109/FMCAD.2013.6679394'
apa: 'Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., & Bloem, R. (2013).
Synthesizing multiple boolean functions using interpolation on a single proof.
In 2013 Formal Methods in Computer-Aided Design (pp. 77–84). Portland,
OR, United States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679394'
chicago: Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick
Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single
Proof.” In 2013 Formal Methods in Computer-Aided Design, 77–84. IEEE, 2013.
https://doi.org/10.1109/FMCAD.2013.6679394.
ieee: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing
multiple boolean functions using interpolation on a single proof,” in 2013
Formal Methods in Computer-Aided Design, Portland, OR, United States, 2013,
pp. 77–84.
ista: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple
boolean functions using interpolation on a single proof. 2013 Formal Methods in
Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84.'
mla: Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation
on a Single Proof.” 2013 Formal Methods in Computer-Aided Design, IEEE,
2013, pp. 77–84, doi:10.1109/FMCAD.2013.6679394.
short: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal
Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.
conference:
end_date: 2013-10-23
location: Portland, OR, United States
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2013-10-20
date_created: 2018-12-11T11:51:43Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2021-01-12T06:50:19Z
day: '11'
department:
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679394
ec_funded: 1
external_id:
arxiv:
- '1308.4767'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1308.4767
month: '12'
oa: 1
oa_version: Preprint
page: 77 - 84
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: 2013 Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5825'
quality_controlled: '1'
status: public
title: Synthesizing multiple boolean functions using interpolation on a single proof
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1387'
abstract:
- lang: eng
text: Choices made by nondeterministic word automata depend on both the past (the
prefix of the word read so far) and the future (the suffix yet to be read). In
several applications, most notably synthesis, the future is diverse or unknown,
leading to algorithms that are based on deterministic automata. Hoping to retain
some of the advantages of nondeterministic automata, researchers have studied
restricted classes of nondeterministic automata. Three such classes are nondeterministic
automata that are good for trees (GFT; i.e., ones that can be expanded to tree
automata accepting the derived tree languages, thus whose choices should satisfy
diverse futures), good for games (GFG; i.e., ones whose choices depend only on
the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent
deterministic automata). The theoretical properties and relative merits of the
different classes are still open, having vagueness on whether they really differ
from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known
whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also
open is the possible succinctness of GFG and GFT automata compared to deterministic
automata. We study these problems for ω-regular automata with all common acceptance
conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction
for GFG automata.
acknowledgement: and ERC Grant QUALITY.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Denis
full_name: Kuperberg, Denis
last_name: Kuperberg
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Michał
full_name: Skrzypczak, Michał
last_name: Skrzypczak
citation:
ama: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. Nondeterminism in the presence
of a diverse or unknown future. 2013;7966(PART 2):89-100. doi:10.1007/978-3-642-39212-2_11
apa: 'Boker, U., Kuperberg, D., Kupferman, O., & Skrzypczak, M. (2013). Nondeterminism
in the presence of a diverse or unknown future. Presented at the ICALP: Automata,
Languages and Programming, Riga, Latvia: Springer. https://doi.org/10.1007/978-3-642-39212-2_11'
chicago: Boker, Udi, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. “Nondeterminism
in the Presence of a Diverse or Unknown Future.” Lecture Notes in Computer Science.
Springer, 2013. https://doi.org/10.1007/978-3-642-39212-2_11.
ieee: U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak, “Nondeterminism in
the presence of a diverse or unknown future,” vol. 7966, no. PART 2. Springer,
pp. 89–100, 2013.
ista: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. 2013. Nondeterminism in the
presence of a diverse or unknown future. 7966(PART 2), 89–100.
mla: Boker, Udi, et al. Nondeterminism in the Presence of a Diverse or Unknown
Future. Vol. 7966, no. PART 2, Springer, 2013, pp. 89–100, doi:10.1007/978-3-642-39212-2_11.
short: U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.
conference:
end_date: 2013-07-12
location: Riga, Latvia
name: 'ICALP: Automata, Languages and Programming'
start_date: 2013-07-08
date_created: 2018-12-11T11:51:44Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:09Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39212-2_11
ec_funded: 1
file:
- access_level: open_access
checksum: 98bc02e3793072e279ec8d364b381ff3
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T11:05:50Z
date_updated: 2020-07-14T12:44:48Z
file_id: '7857'
file_name: 2013_ICALP_Boker.pdf
file_size: 276982
relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: ' 7966'
issue: PART 2
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 89 - 100
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5823'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Nondeterminism in the presence of a diverse or unknown future
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7966
year: '2013'
...
---
_id: '1405'
abstract:
- lang: eng
text: "Motivated by the analysis of highly dynamic message-passing systems, i.e.
unbounded thread creation, mobility, etc. we present a framework for the analysis
of depth-bounded systems. Depth-bounded systems are one of the most expressive
known fragment of the π-calculus for which interesting verification problems are
still decidable. Even though they are infinite state systems depth-bounded systems
are well-structured, thus can be analyzed algorithmically. We give an interpretation
of depth-bounded systems as graph-rewriting systems. This gives more flexibility
and ease of use to apply depth-bounded systems to other type of systems like shared
memory concurrency.\r\n\r\nFirst, we develop an adequate domain of limits for
depth-bounded systems, a prerequisite for the effective representation of downward-closed
sets. Downward-closed sets are needed by forward saturation-based algorithms to
represent potentially infinite sets of states. Then, we present an abstract interpretation
framework to compute the covering set of well-structured transition systems. Because,
in general, the covering set is not computable, our abstraction over-approximates
the actual covering set. Our abstraction captures the essence of acceleration
based-algorithms while giving up enough precision to ensure convergence. We have
implemented the analysis in the PICASSO tool and show that it is accurate in practice.
Finally, we build some further analyses like termination using the covering set
as starting point."
acknowledgement: "This work was supported in part by the Austrian Science Fund NFN
RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative
Reactve Modeling).\r\nChapter 2, 3, and 4 are joint work with Thomas A. Henzinger
and Thomas Wies. Chapter 2 was published in FoSSaCS 2010 as “Forward Analysis of
Depth-Bounded Processes” [112]. Chapter 3 was published in VMCAI 2012 as “Ideal
Abstractions for Well-Structured Transition Systems” [114]. Chap- ter 5.1 is joint
work with Kshitij Bansal, Eric Koskinen, and Thomas Wies. It was published in TACAS
2013 as “Structural Counter Abstraction” [13]. The author’s contribution in this
part is mostly related to the implementation. The theory required to understand
the method and its implementation is quickly recalled to make the thesis self-contained,
but should not be considered as a contribution. For the details of the methods,
we refer the reader to the orig- inal publication [13] and the corresponding technical
report [14]. Chapter 5.2 is ongoing work with Shahram Esmaeilsabzali, Rupak Majumdar,
and Thomas Wies. I also would like to thank the people who supported over the past
4 years. My advisor Thomas A. Henzinger who gave me a lot of freedom to work on
projects I was interested in. My collaborators, especially Thomas Wies with whom
I worked since the beginning. The members of my thesis committee, Viktor Kun- cak
and Rupak Majumdar, who also agreed to advise me. Simon Aeschbacher, Pavol Cerny,
Cezara Dragoi, Arjun Radhakrishna, my family, friends and col- leagues who created
an enjoyable environment. "
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: Zufferey D. Analysis of dynamic message passing programs. 2013. doi:10.15479/at:ista:1405
apa: Zufferey, D. (2013). Analysis of dynamic message passing programs. Institute
of Science and Technology Austria. https://doi.org/10.15479/at:ista:1405
chicago: Zufferey, Damien. “Analysis of Dynamic Message Passing Programs.” Institute
of Science and Technology Austria, 2013. https://doi.org/10.15479/at:ista:1405.
ieee: D. Zufferey, “Analysis of dynamic message passing programs,” Institute of
Science and Technology Austria, 2013.
ista: Zufferey D. 2013. Analysis of dynamic message passing programs. Institute
of Science and Technology Austria.
mla: Zufferey, Damien. Analysis of Dynamic Message Passing Programs. Institute
of Science and Technology Austria, 2013, doi:10.15479/at:ista:1405.
short: D. Zufferey, Analysis of Dynamic Message Passing Programs, Institute of Science
and Technology Austria, 2013.
date_created: 2018-12-11T11:51:50Z
date_published: 2013-09-05T00:00:00Z
date_updated: 2023-09-07T11:36:37Z
day: '05'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
- _id: GradSch
doi: 10.15479/at:ista:1405
ec_funded: 1
file:
- access_level: open_access
checksum: ed2d7b52933d134e8dc69d569baa284e
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T11:28:36Z
date_updated: 2021-02-22T11:28:36Z
file_id: '9176'
file_name: 2013_Zufferey_thesis_final.pdf
file_size: 1514906
relation: main_file
success: 1
- access_level: closed
checksum: cecc4c4b14225bee973d32e3dba91a55
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-16T14:42:52Z
date_updated: 2021-11-17T13:47:58Z
file_id: '10298'
file_name: 2013_Zufferey_thesis_final_pdfa.pdf
file_size: 1378313
relation: main_file
file_date_updated: 2021-11-17T13:47:58Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- url: http://dzufferey.github.io/files/2013_thesis.pdf
month: '09'
oa: 1
oa_version: Published Version
page: '134'
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5802'
related_material:
record:
- id: '2847'
relation: part_of_dissertation
status: public
- id: '3251'
relation: part_of_dissertation
status: public
- id: '4361'
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: Analysis of dynamic message passing programs
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2013'
...
---
_id: '5402'
abstract:
- lang: eng
text: "Linearizability requires that the outcome of calls by competing threads to
a concurrent data structure is the same as some sequential execution where each
thread has exclusive access to the data structure. In an ordered data structure,
such as a queue or a stack, linearizability is ensured by requiring threads commit
in the order dictated by the sequential semantics of the data structure; e.g.,
in a concurrent queue implementation a dequeue can only remove the oldest element.
\r\nIn this paper, we investigate the impact of this strict ordering, by comparing
what linearizability allows to what existing implementations do. We first give
an operational definition for linearizability which allows us to build the most
general linearizable implementation as a transition system for any given sequential
specification. We then use this operational definition to categorize linearizable
implementations based on whether they are bound or free. In a bound implementation,
whenever all threads observe the same logical state, the updates to the logical
state and the temporal order of commits coincide. All existing queue implementations
we know of are bound. We then proceed to present, to the best of our knowledge,
the first ever free queue implementation. Our experiments show that free implementations
have the potential for better performance by suffering less from contention."
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: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: Henzinger TA, Sezgin A. How Free Is Your Linearizable Concurrent Data Structure?
IST Austria; 2013. doi:10.15479/AT:IST-2013-123-v1-1
apa: Henzinger, T. A., & Sezgin, A. (2013). How free is your linearizable
concurrent data structure? IST Austria. https://doi.org/10.15479/AT:IST-2013-123-v1-1
chicago: Henzinger, Thomas A, and Ali Sezgin. How Free Is Your Linearizable Concurrent
Data Structure? IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-123-v1-1.
ieee: T. A. Henzinger and A. Sezgin, How free is your linearizable concurrent
data structure? IST Austria, 2013.
ista: Henzinger TA, Sezgin A. 2013. How free is your linearizable concurrent data
structure?, IST Austria, 16p.
mla: Henzinger, Thomas A., and Ali Sezgin. How Free Is Your Linearizable Concurrent
Data Structure? IST Austria, 2013, doi:10.15479/AT:IST-2013-123-v1-1.
short: T.A. Henzinger, A. Sezgin, How Free Is Your Linearizable Concurrent Data
Structure?, IST Austria, 2013.
date_created: 2018-12-12T11:39:07Z
date_published: 2013-06-12T00:00:00Z
date_updated: 2020-07-14T23:04:47Z
day: '12'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2013-123-v1-1
file:
- access_level: open_access
checksum: ce580605ae9756a8c99d7b403ebb8eed
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:19Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5480'
file_name: IST-2013-123-v1+1_main-concur2013.pdf
file_size: 249790
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '16'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '123'
status: public
title: How free is your linearizable concurrent data structure?
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5406'
abstract:
- lang: eng
text: 'We consider the distributed synthesis problem fortemporal logic specifications.
Traditionally, the problem has been studied for LTL, and the previous results
show that the problem is decidable iff there is no information fork in the architecture.
We consider the problem for fragments of LTLand our main results are as follows:
(1) We show that the problem is undecidable for architectures with information
forks even for the fragment of LTL with temporal operators restricted to next
and eventually. (2) For specifications restricted to globally along with non-nested
next operators, we establish decidability (in EXPSPACE) for star architectures
where the processes receive disjoint inputs, whereas we establish undecidability
for architectures containing an information fork-meet structure. (3)Finally, we
consider LTL without the next operator, and establish decidability (NEXPTIME-complete)
for all architectures for a fragment that consists of a set of safety assumptions,
and a set of guarantees where each guarantee is a safety, reachability, or liveness
condition.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- 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, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis
for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1
apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013).
Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis.
Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed
synthesis for LTL Fragments. IST Austria, 2013.
ista: Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis
for LTL Fragments, IST Austria, 11p.
mla: Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments.
IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1.
short: K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis
for LTL Fragments, IST Austria, 2013.
date_created: 2018-12-12T11:39:09Z
date_published: 2013-07-08T00:00:00Z
date_updated: 2023-02-21T17:01:26Z
day: '08'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2013-130-v1-1
file:
- access_level: open_access
checksum: 855513ebaf6f72228800c5fdb522f93c
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:18Z
date_updated: 2020-07-14T12:46:45Z
file_id: '5540'
file_name: IST-2013-130-v1+1_Distributed_Synthesis.pdf
file_size: 467895
relation: main_file
file_date_updated: 2020-07-14T12:46:45Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '11'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '130'
related_material:
record:
- id: '1376'
relation: later_version
status: public
status: public
title: Distributed synthesis for LTL Fragments
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '5747'
article_processing_charge: No
author:
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent
Objects with Cooperating Updates. In: Computer Aided Verification. Vol
8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:10.1007/978-3-642-39799-8_11'
apa: 'Dragoi, C., Gupta, A., & Henzinger, T. A. (2013). Automatic Linearizability
Proofs of Concurrent Objects with Cooperating Updates. In Computer Aided Verification
(Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_11'
chicago: 'Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability
Proofs of Concurrent Objects with Cooperating Updates.” In Computer Aided Verification,
8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. https://doi.org/10.1007/978-3-642-39799-8_11.'
ieee: 'C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs
of Concurrent Objects with Cooperating Updates,” in Computer Aided Verification,
vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190.'
ista: 'Dragoi C, Gupta A, Henzinger TA. 2013.Automatic Linearizability Proofs of
Concurrent Objects with Cooperating Updates. In: Computer Aided Verification.
vol. 8044, 174–190.'
mla: Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects
with Cooperating Updates.” Computer Aided Verification, vol. 8044, Springer
Berlin Heidelberg, 2013, pp. 174–90, doi:10.1007/978-3-642-39799-8_11.
short: C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer
Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.
conference:
end_date: 2013-07-19
location: Saint Petersburg, Russia
name: CAV 2013
start_date: 2013-07-13
date_created: 2018-12-18T13:10:21Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2023-09-05T14:16:07Z
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39799-8_11
ec_funded: 1
file:
- access_level: open_access
checksum: a901cc6b71db08b61c0d4c0cbacc6287
content_type: application/pdf
creator: dernst
date_created: 2018-12-18T13:13:33Z
date_updated: 2020-07-14T12:47:10Z
file_id: '5748'
file_name: 2013_CAV_Dragoi.pdf
file_size: 236480
relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: ' 8044'
language:
- iso: eng
oa: 1
oa_version: None
page: 174-190
place: Berlin, Heidelberg
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783642397981'
- '9783642397998'
issn:
- 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
pubrep_id: '195'
quality_controlled: '1'
scopus_import: '1'
series_title: CAV
status: public
title: Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 8044
year: '2013'
...
---
_id: '6440'
abstract:
- lang: eng
text: In order to guarantee that each method of a data structure updates the logical
state exactly once, al-most all non-blocking implementations employ Compare-And-Swap
(CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods
competing among themselves to update the same variable, the tail or the head,
respectively, leading to high contention and poor scalability. Recent non-blocking
queue implementations try to alleviate high contentionby increasing the number
of contention points, all the while using CAS-based synchronization. Furthermore,
obtaining a wait-free implementation with competition is achieved by additional
synchronization which leads to further degradation of performance.In this paper
we formalize the notion of competitiveness of a synchronizing statement which
can beused as a measure for the scalability of concurrent implementations. We
present a new queue implementation, the Speculative Pairing (SP) queue, which,
as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead
of CAS. We prove that the SP queue is linearizable and lock-free.We also show
that replacing CAS with FAI leads to wait-freedom for dequeue methods without
an adverse effect on performance. In fact, our experiments suggest that the SP
queue can perform and scale better than the state-of-the-art queue implementations.
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: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation
to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1
apa: Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition
with cooperation to achieve scalable lock-free FIFO queues . IST Austria.
https://doi.org/10.15479/AT:IST-2013-124-v1-1
chicago: Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition
with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria,
2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1.
ieee: T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation
to achieve scalable lock-free FIFO queues . IST Austria, 2013.
ista: Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation
to achieve scalable lock-free FIFO queues , IST Austria, 23p.
mla: Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve
Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1.
short: T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation
to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013.
date_created: 2019-05-13T14:13:27Z
date_published: 2013-06-13T00:00:00Z
date_updated: 2020-07-14T23:06:19Z
day: '13'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2013-124-v1-1
file:
- access_level: open_access
checksum: a219ba4eada6cd62befed52262ee15d4
content_type: application/pdf
creator: dernst
date_created: 2019-05-13T14:11:39Z
date_updated: 2020-07-14T12:47:30Z
file_id: '6441'
file_name: 2013_TechRep_Henzinger.pdf
file_size: 549684
relation: main_file
file_date_updated: 2020-07-14T12:47:30Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '23'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '124'
status: public
title: 'Replacing competition with cooperation to achieve scalable lock-free FIFO
queues '
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '10898'
abstract:
- lang: eng
text: A prominent remedy to multicore scalability issues in concurrent data structure
implementations is to relax the sequential specification of the data structure.
We present distributed queues (DQ), a new family of relaxed concurrent queue implementations.
DQs implement relaxed queues with linearizable emptiness check and either configurable
or bounded out-of-order behavior or pool behavior. Our experiments show that DQs
outperform and outscale in micro- and macrobenchmarks all strict and relaxed queue
as well as pool implementations that we considered.
article_number: '17'
article_processing_charge: No
author:
- first_name: Andreas
full_name: Haas, Andreas
last_name: Haas
- first_name: Michael
full_name: Lippautz, Michael
last_name: Lippautz
- 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: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ana
full_name: Sokolova, Ana
last_name: Sokolova
- first_name: Christoph M.
full_name: Kirsch, Christoph M.
last_name: Kirsch
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: 'Haas A, Lippautz M, Henzinger TA, et al. Distributed queues in shared memory:
Multicore performance and scalability through quantitative relaxation. In: Proceedings
of the ACM International Conference on Computing Frontiers - CF ’13. ACM Press;
2013. doi:10.1145/2482767.2482789'
apa: 'Haas, A., Lippautz, M., Henzinger, T. A., Payer, H., Sokolova, A., Kirsch,
C. M., & Sezgin, A. (2013). Distributed queues in shared memory: Multicore
performance and scalability through quantitative relaxation. In Proceedings
of the ACM International Conference on Computing Frontiers - CF ’13. Ischia,
Italy: ACM Press. https://doi.org/10.1145/2482767.2482789'
chicago: 'Haas, Andreas, Michael Lippautz, Thomas A Henzinger, Hannes Payer, Ana
Sokolova, Christoph M. Kirsch, and Ali Sezgin. “Distributed Queues in Shared Memory:
Multicore Performance and Scalability through Quantitative Relaxation.” In Proceedings
of the ACM International Conference on Computing Frontiers - CF ’13. ACM Press,
2013. https://doi.org/10.1145/2482767.2482789.'
ieee: 'A. Haas et al., “Distributed queues in shared memory: Multicore performance
and scalability through quantitative relaxation,” in Proceedings of the ACM
International Conference on Computing Frontiers - CF ’13, Ischia, Italy, 2013,
no. 5.'
ista: 'Haas A, Lippautz M, Henzinger TA, Payer H, Sokolova A, Kirsch CM, Sezgin
A. 2013. Distributed queues in shared memory: Multicore performance and scalability
through quantitative relaxation. Proceedings of the ACM International Conference
on Computing Frontiers - CF ’13. CF: Conference on Computing Frontiers, 17.'
mla: 'Haas, Andreas, et al. “Distributed Queues in Shared Memory: Multicore Performance
and Scalability through Quantitative Relaxation.” Proceedings of the ACM International
Conference on Computing Frontiers - CF ’13, no. 5, 17, ACM Press, 2013, doi:10.1145/2482767.2482789.'
short: A. Haas, M. Lippautz, T.A. Henzinger, H. Payer, A. Sokolova, C.M. Kirsch,
A. Sezgin, in:, Proceedings of the ACM International Conference on Computing Frontiers
- CF ’13, ACM Press, 2013.
conference:
end_date: 2013-05-16
location: Ischia, Italy
name: 'CF: Conference on Computing Frontiers'
start_date: 2013-05-14
date_created: 2022-03-21T07:33:22Z
date_published: 2013-05-01T00:00:00Z
date_updated: 2022-06-21T08:01:19Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2482767.2482789
issue: '5'
language:
- iso: eng
month: '05'
oa_version: None
publication: Proceedings of the ACM International Conference on Computing Frontiers
- CF '13
publication_identifier:
isbn:
- 978-145032053-5
publication_status: published
publisher: ACM Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Distributed queues in shared memory: Multicore performance and scalability
through quantitative relaxation'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2181'
abstract:
- lang: eng
text: 'There is a trade-off between performance and correctness in implementing
concurrent data structures. Better performance may be achieved at the expense
of relaxing correctness, by redefining the semantics of data structures. We address
such a redefinition of data structure semantics and present a systematic and formal
framework for obtaining new data structures by quantitatively relaxing existing
ones. We view a data structure as a sequential specification S containing all
"legal" sequences over an alphabet of method calls. Relaxing the data
structure corresponds to defining a distance from any sequence over the alphabet
to the sequential specification: the k-relaxed sequential specification contains
all sequences over the alphabet within distance k from the original specification.
In contrast to other existing work, our relaxations are semantic (distance in
terms of data structure states). As an instantiation of our framework, we present
two simple yet generic relaxation schemes, called out-of-order and stuttering
relaxation, along with several ways of computing distances. We show that the out-of-order
relaxation, when further instantiated to stacks, queues, and priority queues,
amounts to tolerating bounded out-of-order behavior, which cannot be captured
by a purely syntactic relaxation (distance in terms of sequence manipulation,
e.g. edit distance). We give concurrent implementations of relaxed data structures
and demonstrate that bounded relaxations provide the means for trading correctness
for performance in a controlled way. The relaxations are monotonic which further
highlights the trade-off: increasing k increases the number of permitted sequences,
which as we demonstrate can lead to better performance. Finally, since a relaxed
stack or queue also implements a pool, we actually have new concurrent pool implementations
that outperform the state-of-the-art ones.'
acknowledgement: ' and an Elise Richter Fellowship (Austrian Science Fund V00125). '
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: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- first_name: Ana
full_name: Sokolova, Ana
last_name: Sokolova
citation:
ama: 'Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. Quantitative relaxation
of concurrent data structures. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Language. ACM; 2013:317-328. doi:10.1145/2429069.2429109'
apa: 'Henzinger, T. A., Kirsch, C., Payer, H., Sezgin, A., & Sokolova, A. (2013).
Quantitative relaxation of concurrent data structures. In Proceedings of the
40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language
(pp. 317–328). Rome, Italy: ACM. https://doi.org/10.1145/2429069.2429109'
chicago: Henzinger, Thomas A, Christoph Kirsch, Hannes Payer, Ali Sezgin, and Ana
Sokolova. “Quantitative Relaxation of Concurrent Data Structures.” In Proceedings
of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
317–28. ACM, 2013. https://doi.org/10.1145/2429069.2429109.
ieee: T. A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, and A. Sokolova, “Quantitative
relaxation of concurrent data structures,” in Proceedings of the 40th annual
ACM SIGPLAN-SIGACT symposium on Principles of programming language, Rome,
Italy, 2013, pp. 317–328.
ista: 'Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. 2013. Quantitative
relaxation of concurrent data structures. Proceedings of the 40th annual ACM SIGPLAN-SIGACT
symposium on Principles of programming language. POPL: Principles of Programming
Languages, 317–328.'
mla: Henzinger, Thomas A., et al. “Quantitative Relaxation of Concurrent Data Structures.”
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Language, ACM, 2013, pp. 317–28, doi:10.1145/2429069.2429109.
short: T.A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, A. Sokolova, in:, Proceedings
of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
ACM, 2013, pp. 317–328.
conference:
end_date: 2013-01-25
location: Rome, Italy
name: 'POPL: Principles of Programming Languages'
start_date: 2013-01-23
date_created: 2018-12-11T11:56:11Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2023-02-21T16:06:49Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1145/2429069.2429109
ec_funded: 1
file:
- access_level: open_access
checksum: adf465e70948f4e80e48057524516456
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:33Z
date_updated: 2020-07-14T12:45:31Z
file_id: '5086'
file_name: IST-2014-198-v1+1_popl128-henzinger-clean.pdf
file_size: 294689
relation: main_file
file_date_updated: 2020-07-14T12:45:31Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 317 - 328
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: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles
of programming language
publication_identifier:
isbn:
- 978-1-4503-1832-7
publication_status: published
publisher: ACM
publist_id: '4801'
pubrep_id: '198'
quality_controlled: '1'
related_material:
record:
- id: '10901'
relation: later_version
status: deleted
scopus_import: 1
status: public
title: Quantitative relaxation of concurrent data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2182'
abstract:
- lang: eng
text: We propose a general framework for abstraction with respect to quantitative
properties, such as worst-case execution time, or power consumption. Our framework
provides a systematic way for counter-example guided abstraction refinement for
quantitative properties. The salient aspect of the framework is that it allows
anytime verification, that is, verification algorithms that can be stopped at
any time (for example, due to exhaustion of memory), and report approximations
that improve monotonically when the algorithms are given more time. We instantiate
the framework with a number of quantitative abstractions and refinement schemes,
which differ in terms of how much quantitative information they keep from the
original system. We introduce both state-based and trace-based quantitative abstractions,
and we describe conditions that define classes of quantitative properties for
which the abstractions provide over-approximations. We give algorithms for evaluating
the quantitative properties on the abstract systems. We present algorithms for
counter-example based refinements for quantitative properties for both state-based
and segment-based abstractions. We perform a case study on worst-case execution
time of executables to evaluate the anytime verification aspect and the quantitative
abstractions we proposed.
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Quantitative abstraction refinement.
In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Language. ACM; 2013:115-128. doi:10.1145/2429069.2429085'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2013). Quantitative abstraction
refinement. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium
on Principles of programming language (pp. 115–128). Rome, Italy: ACM. https://doi.org/10.1145/2429069.2429085'
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative
Abstraction Refinement.” In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Language, 115–28. ACM, 2013. https://doi.org/10.1145/2429069.2429085.
ieee: P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative abstraction
refinement,” in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium
on Principles of programming language, Rome, Italy, 2013, pp. 115–128.
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2013. Quantitative abstraction refinement.
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming
language. POPL: Principles of Programming Languages, 115–128.'
mla: Cerny, Pavol, et al. “Quantitative Abstraction Refinement.” Proceedings
of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
ACM, 2013, pp. 115–28, doi:10.1145/2429069.2429085.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Proceedings of the 40th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, ACM, 2013,
pp. 115–128.
conference:
end_date: 2013-01-25
location: Rome, Italy
name: 'POPL: Principles of Programming Languages'
start_date: 2013-07-23
date_created: 2018-12-11T11:56:11Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:55:50Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2429069.2429085
ec_funded: 1
language:
- iso: eng
month: '01'
oa_version: None
page: 115 - 128
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: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles
of programming language
publication_status: published
publisher: ACM
publist_id: '4800'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative abstraction refinement
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_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'
...
---
_id: '2243'
abstract:
- lang: eng
text: We show that modal logic over universally first-order definable classes of
transitive frames is decidable. More precisely, let K be an arbitrary class of
transitive Kripke frames definable by a universal first-order sentence. We show
that the global and finite global satisfiability problems of modal logic over
K are decidable in NP, regardless of choice of K. We also show that the local
satisfiability and the finite local satisfiability problems of modal logic over
K are decidable in NEXPTIME.
alternative_title:
- LIPIcs
author:
- first_name: Jakub
full_name: Michaliszyn, Jakub
last_name: Michaliszyn
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Michaliszyn J, Otop J. Elementary modal logics over transitive structures.
2013;23:563-577. doi:10.4230/LIPIcs.CSL.2013.563
apa: 'Michaliszyn, J., & Otop, J. (2013). Elementary modal logics over transitive
structures. Presented at the CSL: Computer Science Logic, Torino, Italy: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.563'
chicago: Michaliszyn, Jakub, and Jan Otop. “Elementary Modal Logics over Transitive
Structures.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.563.
ieee: J. Michaliszyn and J. Otop, “Elementary modal logics over transitive structures,”
vol. 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 563–577, 2013.
ista: Michaliszyn J, Otop J. 2013. Elementary modal logics over transitive structures.
23, 563–577.
mla: Michaliszyn, Jakub, and Jan Otop. Elementary Modal Logics over Transitive
Structures. Vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013,
pp. 563–77, doi:10.4230/LIPIcs.CSL.2013.563.
short: J. Michaliszyn, J. Otop, 23 (2013) 563–577.
conference:
end_date: 2013-09-05
location: Torino, Italy
name: 'CSL: Computer Science Logic'
start_date: 2013-09-02
date_created: 2018-12-11T11:56:32Z
date_published: 2013-09-01T00:00:00Z
date_updated: 2020-08-11T10:09:42Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CSL.2013.563
ec_funded: 1
file:
- access_level: open_access
checksum: e0732e73a8b1e39483df7717d53e3e35
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:11Z
date_updated: 2020-07-14T12:45:34Z
file_id: '4929'
file_name: IST-2016-136-v1+2_39.pdf
file_size: 454915
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 23'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: 563 - 577
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4708'
pubrep_id: '136'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: Elementary modal logics over transitive structures
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: 23
year: '2013'
...
---
_id: '2288'
abstract:
- lang: eng
text: This book constitutes the proceedings of the 11th International Conference
on Computational Methods in Systems Biology, CMSB 2013, held in Klosterneuburg,
Austria, in September 2013. The 15 regular papers included in this volume were
carefully reviewed and selected from 27 submissions. They deal with computational
models for all levels, from molecular and cellular, to organs and entire organisms.
alternative_title:
- LNCS
citation:
ama: Gupta A, Henzinger TA, eds. Computational Methods in Systems Biology.
Vol 8130. Springer; 2013. doi:10.1007/978-3-642-40708-6
apa: 'Gupta, A., & Henzinger, T. A. (Eds.). (2013). Computational Methods
in Systems Biology (Vol. 8130). Presented at the CMSB: Computational Methods
in Systems Biology, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40708-6'
chicago: Gupta, Ashutosh, and Thomas A Henzinger, eds. Computational Methods
in Systems Biology. Vol. 8130. Springer, 2013. https://doi.org/10.1007/978-3-642-40708-6.
ieee: A. Gupta and T. A. Henzinger, Eds., Computational Methods in Systems Biology,
vol. 8130. Springer, 2013.
ista: Gupta A, Henzinger TA eds. 2013. Computational Methods in Systems Biology,
Springer,p.
mla: Gupta, Ashutosh, and Thomas A. Henzinger, editors. Computational Methods
in Systems Biology. Vol. 8130, Springer, 2013, doi:10.1007/978-3-642-40708-6.
short: A. Gupta, T.A. Henzinger, eds., Computational Methods in Systems Biology,
Springer, 2013.
conference:
end_date: 2013-09-24
location: Klosterneuburg, Austria
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2013-09-22
date_created: 2018-12-11T11:56:47Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2019-08-02T12:37:44Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40708-6
editor:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
intvolume: ' 8130'
language:
- iso: eng
month: '07'
oa_version: None
publication_identifier:
isbn:
- 978-3-642-40707-9
publication_status: published
publisher: Springer
publist_id: '4643'
quality_controlled: '1'
status: public
title: Computational Methods in Systems Biology
type: conference_editor
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8130
year: '2013'
...
---
_id: '2289'
abstract:
- lang: eng
text: Formal verification aims to improve the quality of software by detecting errors
before they do harm. At the basis of formal verification is the logical notion
of correctness, which purports to capture whether or not a program behaves as
desired. We suggest that the boolean partition of software into correct and incorrect
programs falls short of the practical need to assess the behavior of software
in a more nuanced fashion against multiple criteria. We therefore propose to introduce
quantitative fitness measures for programs, specifically for measuring the function,
performance, and robustness of reactive programs such as concurrent processes.
This article describes the goals of the ERC Advanced Investigator Project QUAREM.
The project aims to build and evaluate a theory of quantitative fitness measures
for reactive models. Such a theory must strive to obtain quantitative generalizations
of the paradigms that have been success stories in qualitative reactive modeling,
such as compositionality, property-preserving abstraction and abstraction refinement,
model checking, and synthesis. The theory will be evaluated not only in the context
of software and hardware engineering, but also in the context of systems biology.
In particular, we will use the quantitative reactive models and fitness measures
developed in this project for testing hypotheses about the mechanisms behind data
from biological experiments.
author:
- 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: Henzinger TA. Quantitative reactive modeling and verification. Computer
Science Research and Development. 2013;28(4):331-344. doi:10.1007/s00450-013-0251-7
apa: Henzinger, T. A. (2013). Quantitative reactive modeling and verification. Computer
Science Research and Development. Springer. https://doi.org/10.1007/s00450-013-0251-7
chicago: Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.”
Computer Science Research and Development. Springer, 2013. https://doi.org/10.1007/s00450-013-0251-7.
ieee: T. A. Henzinger, “Quantitative reactive modeling and verification,” Computer
Science Research and Development, vol. 28, no. 4. Springer, pp. 331–344, 2013.
ista: Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer
Science Research and Development. 28(4), 331–344.
mla: Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” Computer
Science Research and Development, vol. 28, no. 4, Springer, 2013, pp. 331–44,
doi:10.1007/s00450-013-0251-7.
short: T.A. Henzinger, Computer Science Research and Development 28 (2013) 331–344.
date_created: 2018-12-11T11:56:47Z
date_published: 2013-10-05T00:00:00Z
date_updated: 2021-01-12T06:56:33Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00450-013-0251-7
ec_funded: 1
file:
- access_level: open_access
checksum: f117a00f9f046165bfa95595681e08a0
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:51Z
date_updated: 2020-07-14T12:45:37Z
file_id: '5308'
file_name: IST-2016-626-v1+1_s00450-013-0251-7.pdf
file_size: 570361
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 28'
issue: '4'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 331 - 344
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Computer Science Research and Development
publication_status: published
publisher: Springer
publist_id: '4642'
pubrep_id: '626'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative reactive modeling and verification
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 28
year: '2013'
...
---
_id: '2298'
abstract:
- lang: eng
text: "We present a shape analysis for programs that manipulate overlaid data structures
which share sets of objects. The abstract domain contains Separation Logic formulas
that (1) combine a per-object separating conjunction with a per-field separating
conjunction and (2) constrain a set of variables interpreted as sets of objects.
The definition of the abstract domain operators is based on a notion of homomorphism
between formulas, viewed as graphs, used recently to define optimal decision procedures
for fragments of the Separation Logic. Based on a Frame Rule that supports the
two versions of the separating conjunction, the analysis is able to reason in
a modular manner about non-overlaid data structures and then, compose information
only at a few program points, e.g., procedure returns. We have implemented this
analysis in a prototype tool and applied it on several interesting case studies
that manipulate overlaid and nested linked lists.\r\n"
alternative_title:
- LNCS
author:
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- first_name: Constantin
full_name: Enea, Constantin
last_name: Enea
- first_name: Mihaela
full_name: Sighireanu, Mihaela
last_name: Sighireanu
citation:
ama: 'Dragoi C, Enea C, Sighireanu M. Local shape analysis for overlaid data structures.
In: Vol 7935. Springer; 2013:150-171. doi:10.1007/978-3-642-38856-9_10'
apa: 'Dragoi, C., Enea, C., & Sighireanu, M. (2013). Local shape analysis for
overlaid data structures (Vol. 7935, pp. 150–171). Presented at the SAS: Static
Analysis Symposium, Seattle, WA, United States: Springer. https://doi.org/10.1007/978-3-642-38856-9_10'
chicago: Dragoi, Cezara, Constantin Enea, and Mihaela Sighireanu. “Local Shape Analysis
for Overlaid Data Structures,” 7935:150–71. Springer, 2013. https://doi.org/10.1007/978-3-642-38856-9_10.
ieee: 'C. Dragoi, C. Enea, and M. Sighireanu, “Local shape analysis for overlaid
data structures,” presented at the SAS: Static Analysis Symposium, Seattle, WA,
United States, 2013, vol. 7935, pp. 150–171.'
ista: 'Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data
structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.'
mla: Dragoi, Cezara, et al. Local Shape Analysis for Overlaid Data Structures.
Vol. 7935, Springer, 2013, pp. 150–71, doi:10.1007/978-3-642-38856-9_10.
short: C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.
conference:
end_date: 2013-06-22
location: Seattle, WA, United States
name: 'SAS: Static Analysis Symposium'
start_date: 2013-06-20
date_created: 2018-12-11T11:56:50Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:56:36Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-38856-9_10
ec_funded: 1
file:
- access_level: open_access
checksum: 907edd33a5892e3af093365f1fd57ed7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:36Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4824'
file_name: IST-2014-196-v1+1_sas13.pdf
file_size: 299004
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 7935'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 150 - 171
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4630'
pubrep_id: '196'
quality_controlled: '1'
scopus_import: 1
status: public
title: Local shape analysis for overlaid data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7935
year: '2013'
...
---
_id: '2299'
abstract:
- lang: eng
text: 'The standard hardware design flow involves: (a) design of an integrated circuit
using a hardware description language, (b) extensive functional and formal verification,
and (c) logical synthesis. However, the above-mentioned processes consume significant
effort and time. An alternative approach is to use a formal specification language
as a high-level hardware description language and synthesize hardware from formal
specifications. Our work is a case study of the synthesis of the widely and industrially
used AMBA AHB protocol from formal specifications. Bloem et al. presented the
first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter
circuit. However, in the first formal specification some important assumptions
were missing. Our contributions are as follows: (a) We present detailed formal
specifications for the AHB Arbiter incorporating the missing details, and obtain
significant improvements in the synthesis results (both with respect to the number
of gates in the synthesized circuit and with respect to the time taken to synthesize
the circuit), and (b) we present formal specifications to generate compact circuits
for the remaining two main components of AMBA AHB, namely, AHB Master and AHB
Slave. Thus with systematic description we are able to automatically and completely
synthesize an important and widely used industrial protocol.'
author:
- first_name: Yashdeep
full_name: Godhal, Yashdeep
id: 5B547124-EB61-11E9-8887-89D9C04DBDF5
last_name: Godhal
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: 'Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification:
A case study. International Journal on Software Tools for Technology Transfer.
2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9'
apa: 'Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA
AHB from formal specification: A case study. International Journal on Software
Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9'
chicago: 'Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis
of AMBA AHB from Formal Specification: A Case Study.” International Journal
on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.'
ieee: 'Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from
formal specification: A case study,” International Journal on Software Tools
for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.'
ista: 'Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal
specification: A case study. International Journal on Software Tools for Technology
Transfer. 15(5–6), 585–601.'
mla: 'Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification:
A Case Study.” International Journal on Software Tools for Technology Transfer,
vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9.'
short: Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software
Tools for Technology Transfer 15 (2013) 585–601.
date_created: 2018-12-11T11:56:51Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2021-01-12T06:56:37Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10009-011-0207-9
file:
- access_level: open_access
checksum: 57b06a732dd8d6349190dba6b5b0d33b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:53Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4910'
file_name: IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf
file_size: 277372
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 15'
issue: 5-6
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 585 - 601
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '4629'
pubrep_id: '87'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Synthesis of AMBA AHB from formal specification: A case study'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2013'
...
---
_id: '2301'
abstract:
- lang: eng
text: We describe the design and implementation of P, a domain-specific language
to write asynchronous event driven code. P allows the programmer to specify the
system as a collection of interacting state machines, which communicate with each
other using events. P unifies modeling and programming into one activity for the
programmer. Not only can a P program be compiled into executable code, but it
can also be tested using model checking techniques. P allows the programmer to
specify the environment, used to "close" the system during testing,
as nondeterministic ghost machines. Ghost machines are erased during compilation
to executable code; a type system ensures that the erasure is semantics preserving.
The P language is designed so that a P program can be checked for responsiveness-the
ability to handle every event in a timely manner. By default, a machine needs
to handle every event that arrives in every state. But handling every event in
every state is impractical. The language provides a notion of deferred events
where the programmer can annotate when she wants to delay processing an event.
The default safety checker looks for presence of unhan-dled events. The language
also provides default liveness checks that an event cannot be potentially deferred
forever. P was used to implement and verify the core of the USB device driver
stack that ships with Microsoft Windows 8. The resulting driver is more reliable
and performs better than its prior incarnation (which did not use P); we have
more confidence in the robustness of its design due to the language abstractions
and verification provided by P.
author:
- first_name: Ankush
full_name: Desai, Ankush
last_name: Desai
- first_name: Vivek
full_name: Gupta, Vivek
last_name: Gupta
- first_name: Ethan
full_name: Jackson, Ethan
last_name: Jackson
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. P: Safe asynchronous
event-driven programming. In: Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation. ACM; 2013:321-331. doi:10.1145/2491956.2462184'
apa: 'Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., & Zufferey,
D. (2013). P: Safe asynchronous event-driven programming. In Proceedings of
the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
(pp. 321–331). Seattle, WA, United States: ACM. https://doi.org/10.1145/2491956.2462184'
chicago: 'Desai, Ankush, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani,
and Damien Zufferey. “P: Safe Asynchronous Event-Driven Programming.” In Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation,
321–31. ACM, 2013. https://doi.org/10.1145/2491956.2462184.'
ieee: 'A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, and D. Zufferey,
“P: Safe asynchronous event-driven programming,” in Proceedings of the 34th
ACM SIGPLAN Conference on Programming Language Design and Implementation,
Seattle, WA, United States, 2013, pp. 321–331.'
ista: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. 2013. P: Safe
asynchronous event-driven programming. Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation. PLDI: Programming Languages
Design and Implementation, 321–331.'
mla: 'Desai, Ankush, et al. “P: Safe Asynchronous Event-Driven Programming.” Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation,
ACM, 2013, pp. 321–31, doi:10.1145/2491956.2462184.'
short: A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:,
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design
and Implementation, ACM, 2013, pp. 321–331.
conference:
end_date: 2013-06-19
location: Seattle, WA, United States
name: 'PLDI: Programming Languages Design and Implementation'
start_date: 2013-06-16
date_created: 2018-12-11T11:56:52Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2491956.2462184
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: http://research.microsoft.com/pubs/191069/pldi212_desai.pdf
month: '06'
oa_version: None
page: 321 - 331
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language
Design and Implementation
publication_status: published
publisher: ACM
publist_id: '4626'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'P: Safe asynchronous event-driven programming'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2327'
abstract:
- lang: eng
text: 'We define the model-measuring problem: given a model M and specification
φ, what is the maximal distance ρ such that all models M′ within distance ρ from
M satisfy (or violate) φ. The model measuring problem presupposes a distance function
on models. We concentrate on automatic distance functions, which are defined by
weighted automata. The model-measuring problem subsumes several generalizations
of the classical model-checking problem, in particular, quantitative model-checking
problems that measure the degree of satisfaction of a specification, and robustness
problems that measure how much a model can be perturbed without violating the
specification. We show that for automatic distance functions, and ω-regular linear-time
and branching-time specifications, the model-measuring problem can be solved.
We use automata-theoretic model-checking methods for model measuring, replacing
the emptiness question for standard word and tree automata by the optimal-weight
question for the weighted versions of these automata. We consider weighted automata
that accumulate weights by maximizing, summing, discounting, and limit averaging.
We give several examples of using the model-measuring problem to compute various
notions of robustness and quantitative satisfaction for temporal specifications.'
alternative_title:
- LNCS
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Henzinger TA, Otop J. From model checking to model measuring. 2013;8052:273-287.
doi:10.1007/978-3-642-40184-8_20
apa: 'Henzinger, T. A., & Otop, J. (2013). From model checking to model measuring.
Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Springer.
https://doi.org/10.1007/978-3-642-40184-8_20'
chicago: Henzinger, Thomas A, and Jan Otop. “From Model Checking to Model Measuring.”
Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_20.
ieee: T. A. Henzinger and J. Otop, “From model checking to model measuring,” vol.
8052. Springer, pp. 273–287, 2013.
ista: Henzinger TA, Otop J. 2013. From model checking to model measuring. 8052,
273–287.
mla: Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring.
Vol. 8052, Springer, 2013, pp. 273–87, doi:10.1007/978-3-642-40184-8_20.
short: T.A. Henzinger, J. Otop, 8052 (2013) 273–287.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentina
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
date_created: 2018-12-11T11:57:00Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2023-02-23T12:25:26Z
day: '01'
ddc:
- '005'
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40184-8_20
file:
- access_level: open_access
checksum: 4c04695c4bfdf2119cd4f5d1babc3e8a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:45Z
date_updated: 2020-07-14T12:45:38Z
file_id: '5301'
file_name: IST-2013-129-v1+1_concur.pdf
file_size: 378587
relation: main_file
file_date_updated: 2020-07-14T12:45:38Z
has_accepted_license: '1'
intvolume: ' 8052'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 273 - 287
publication_status: published
publisher: Springer
publist_id: '4599'
pubrep_id: '129'
quality_controlled: '1'
related_material:
record:
- id: '5417'
relation: earlier_version
status: public
series_title: Lecture Notes in Computer Science
status: public
title: From model checking to model measuring
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...