---
_id: '635'
abstract:
- lang: eng
text: Memory-hard functions (MHFs) are hash algorithms whose evaluation cost is
dominated by memory cost. As memory, unlike computation, costs about the same
across different platforms, MHFs cannot be evaluated at significantly lower cost
on dedicated hardware like ASICs. MHFs have found widespread applications including
password hashing, key derivation, and proofs-of-work. This paper focuses on scrypt,
a simple candidate MHF designed by Percival, and described in RFC 7914. It has
been used within a number of cryptocurrencies (e.g., Litecoin and Dogecoin) and
has been an inspiration for Argon2d, one of the winners of the recent password-hashing
competition. Despite its popularity, no rigorous lower bounds on its memory complexity
are known. We prove that scrypt is optimally memory-hard, i.e., its cumulative
memory complexity (cmc) in the parallel random oracle model is Ω(n2w), where w
and n are the output length and number of invocations of the underlying hash function,
respectively. High cmc is a strong security target for MHFs introduced by Alwen
and Serbinenko (STOC’15) which implies high memory cost even for adversaries who
can amortize the cost over many evaluations and evaluate the underlying hash functions
many times in parallel. Our proof is the first showing optimal memory-hardness
for any MHF. Our result improves both quantitatively and qualitatively upon the
recent work by Alwen et al. (EUROCRYPT’16) who proved a weaker lower bound of
Ω(n2w/ log2 n) for a restricted class of adversaries.
alternative_title:
- LNCS
author:
- first_name: Joel F
full_name: Alwen, Joel F
id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87
last_name: Alwen
- first_name: Binchi
full_name: Chen, Binchi
last_name: Chen
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
- first_name: Leonid
full_name: Reyzin, Leonid
last_name: Reyzin
- first_name: Stefano
full_name: Tessaro, Stefano
last_name: Tessaro
citation:
ama: 'Alwen JF, Chen B, Pietrzak KZ, Reyzin L, Tessaro S. Scrypt is maximally memory
hard. In: Coron J-S, Buus Nielsen J, eds. Vol 10212. Springer; 2017:33-62. doi:10.1007/978-3-319-56617-7_2'
apa: 'Alwen, J. F., Chen, B., Pietrzak, K. Z., Reyzin, L., & Tessaro, S. (2017).
Scrypt is maximally memory hard. In J.-S. Coron & J. Buus Nielsen (Eds.) (Vol.
10212, pp. 33–62). Presented at the EUROCRYPT: Theory and Applications of Cryptographic
Techniques, Paris, France: Springer. https://doi.org/10.1007/978-3-319-56617-7_2'
chicago: Alwen, Joel F, Binchi Chen, Krzysztof Z Pietrzak, Leonid Reyzin, and Stefano
Tessaro. “Scrypt Is Maximally Memory Hard.” edited by Jean-Sébastien Coron and
Jesper Buus Nielsen, 10212:33–62. Springer, 2017. https://doi.org/10.1007/978-3-319-56617-7_2.
ieee: 'J. F. Alwen, B. Chen, K. Z. Pietrzak, L. Reyzin, and S. Tessaro, “Scrypt
is maximally memory hard,” presented at the EUROCRYPT: Theory and Applications
of Cryptographic Techniques, Paris, France, 2017, vol. 10212, pp. 33–62.'
ista: 'Alwen JF, Chen B, Pietrzak KZ, Reyzin L, Tessaro S. 2017. Scrypt is maximally
memory hard. EUROCRYPT: Theory and Applications of Cryptographic Techniques, LNCS,
vol. 10212, 33–62.'
mla: Alwen, Joel F., et al. Scrypt Is Maximally Memory Hard. Edited by Jean-Sébastien
Coron and Jesper Buus Nielsen, vol. 10212, Springer, 2017, pp. 33–62, doi:10.1007/978-3-319-56617-7_2.
short: J.F. Alwen, B. Chen, K.Z. Pietrzak, L. Reyzin, S. Tessaro, in:, J.-S. Coron,
J. Buus Nielsen (Eds.), Springer, 2017, pp. 33–62.
conference:
end_date: 2017-05-04
location: Paris, France
name: 'EUROCRYPT: Theory and Applications of Cryptographic Techniques'
start_date: 2017-04-30
date_created: 2018-12-11T11:47:37Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:07:10Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-319-56617-7_2
ec_funded: 1
editor:
- first_name: Jean-Sébastien
full_name: Coron, Jean-Sébastien
last_name: Coron
- first_name: Jesper
full_name: Buus Nielsen, Jesper
last_name: Buus Nielsen
intvolume: ' 10212'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2016/989
month: '01'
oa: 1
oa_version: Submitted Version
page: 33 - 62
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication_identifier:
isbn:
- 978-331956616-0
publication_status: published
publisher: Springer
publist_id: '7154'
quality_controlled: '1'
scopus_import: 1
status: public
title: Scrypt is maximally memory hard
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 10212
year: '2017'
...
---
_id: '636'
abstract:
- lang: eng
text: Signal regular expressions can specify sequential properties of real-valued
signals based on threshold conditions, regular operations, and duration constraints.
In this paper we endow them with a quantitative semantics which indicates how
robustly a signal matches or does not match a given expression. First, we show
that this semantics is a safe approximation of a distance between the signal and
the language defined by the expression. Then, we consider the robust matching
problem, that is, computing the quantitative semantics of every segment of a given
signal relative to an expression. We present an algorithm that solves this problem
for piecewise-constant and piecewise-linear signals and show that for such signals
the robustness map is a piecewise-linear function. The availability of an indicator
describing how robustly a signal segment matches some regular pattern provides
a general framework for quantitative monitoring of cyber-physical systems.
alternative_title:
- LNCS
author:
- first_name: Alexey
full_name: Bakhirkin, Alexey
last_name: Bakhirkin
- first_name: Thomas
full_name: Ferrere, Thomas
id: 40960E6E-F248-11E8-B48F-1D18A9856A87
last_name: Ferrere
orcid: 0000-0001-5199-3143
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dogan
full_name: Ulus, Dogan
last_name: Ulus
citation:
ama: 'Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of
regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol
10419. Springer; 2017:189-206. doi:10.1007/978-3-319-65765-3_11'
apa: 'Bakhirkin, A., Ferrere, T., Maler, O., & Ulus, D. (2017). On the quantitative
semantics of regular expressions over real-valued signals. In A. Abate & G.
Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling
and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_11'
chicago: Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the
Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited
by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_11.
ieee: 'A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics
of regular expressions over real-valued signals,” presented at the FORMATS: Formal
Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp.
189–206.'
ista: 'Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics
of regular expressions over real-valued signals. FORMATS: Formal Modelling and
Analysis of Timed Systems, LNCS, vol. 10419, 189–206.'
mla: Bakhirkin, Alexey, et al. On the Quantitative Semantics of Regular Expressions
over Real-Valued Signals. Edited by Alessandro Abate and Gilles Geeraerts,
vol. 10419, Springer, 2017, pp. 189–206, doi:10.1007/978-3-319-65765-3_11.
short: A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts
(Eds.), Springer, 2017, pp. 189–206.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'FORMATS: Formal Modelling and Analysis of Timed Systems'
start_date: 2017-09-05
date_created: 2018-12-11T11:47:38Z
date_published: 2017-08-03T00:00:00Z
date_updated: 2021-01-12T08:07:14Z
day: '03'
department:
- _id: ToHe
doi: 10.1007/978-3-319-65765-3_11
editor:
- first_name: Alessandro
full_name: Abate, Alessandro
last_name: Abate
- first_name: Gilles
full_name: Geeraerts, Gilles
last_name: Geeraerts
intvolume: ' 10419'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://hal.archives-ouvertes.fr/hal-01552132
month: '08'
oa: 1
oa_version: Submitted Version
page: 189 - 206
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-331965764-6
publication_status: published
publisher: Springer
publist_id: '7152'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the quantitative semantics of regular expressions over real-valued signals
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10419
year: '2017'
...
---
_id: '638'
abstract:
- lang: eng
text: "This book constitutes the refereed proceedings of the 9th InternationalWorkshop
on Numerical Software Verification, NSV 2016, held in Toronto, ON, Canada in July
2011 - colocated with CAV 2016, the 28th International Conference on Computer
Aided Verification.\r\nThe NSV workshop is dedicated to the development of logical
and mathematical techniques for the reasoning about programmability and reliability."
article_processing_charge: No
citation:
ama: Bogomolov S, Martel M, Prabhakar P, eds. Numerical Software Verification.
Vol 10152. Springer; 2017. doi:10.1007/978-3-319-54292-8
apa: 'Bogomolov, S., Martel, M., & Prabhakar, P. (Eds.). (2017). Numerical
Software Verification (Vol. 10152). Presented at the NSV: Numerical Software
Verification, Toronto, ON, Canada: Springer. https://doi.org/10.1007/978-3-319-54292-8'
chicago: Bogomolov, Sergiy, Matthieu Martel, and Pavithra Prabhakar, eds. Numerical
Software Verification. Vol. 10152. LNCS. Springer, 2017. https://doi.org/10.1007/978-3-319-54292-8.
ieee: S. Bogomolov, M. Martel, and P. Prabhakar, Eds., Numerical Software Verification,
vol. 10152. Springer, 2017.
ista: Bogomolov S, Martel M, Prabhakar P eds. 2017. Numerical Software Verification,
Springer,p.
mla: Bogomolov, Sergiy, et al., editors. Numerical Software Verification.
Vol. 10152, Springer, 2017, doi:10.1007/978-3-319-54292-8.
short: S. Bogomolov, M. Martel, P. Prabhakar, eds., Numerical Software Verification,
Springer, 2017.
conference:
end_date: 2016-07-18
location: Toronto, ON, Canada
name: 'NSV: Numerical Software Verification'
start_date: 2016-07-17
date_created: 2018-12-11T11:47:38Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2022-05-24T07:09:52Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-54292-8
editor:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Matthieu
full_name: Martel, Matthieu
last_name: Martel
- first_name: Pavithra
full_name: Prabhakar, Pavithra
last_name: Prabhakar
intvolume: ' 10152'
language:
- iso: eng
month: '01'
oa_version: None
publication_identifier:
eisbn:
- 978-3-319-54292-8
issn:
- 0302-9743
publication_status: published
publisher: Springer
publist_id: '7150'
quality_controlled: '1'
series_title: LNCS
status: public
title: Numerical Software Verification
type: conference_editor
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10152
year: '2017'
...
---
_id: '640'
abstract:
- lang: eng
text: 'Data-independent Memory Hard Functions (iMHFS) are finding a growing number
of applications in security; especially in the domain of password hashing. An
important property of a concrete iMHF is specified by fixing a directed acyclic
graph (DAG) Gn on n nodes. The quality of that iMHF is then captured by the following
two pebbling complexities of Gn: – The parallel cumulative pebbling complexity
Π∥cc(Gn) must be as high as possible (to ensure that the amortized cost of computing
the function on dedicated hardware is dominated by the cost of memory). – The
sequential space-time pebbling complexity Πst(Gn) should be as close as possible
to Π∥cc(Gn) (to ensure that using many cores in parallel and amortizing over many
instances does not give much of an advantage). In this paper we construct a family
of DAGs with best possible parameters in an asymptotic sense, i.e., where Π∥cc(Gn)
= Ω(n2/ log(n)) (which matches a known upper bound) and Πst(Gn) is within a constant
factor of Π∥cc(Gn). Our analysis relies on a new connection between the pebbling
complexity of a DAG and its depth-robustness (DR) – a well studied combinatorial
property. We show that high DR is sufficient for high Π∥cc. Alwen and Blocki (CRYPTO’16)
showed that high DR is necessary and so, together, these results fully characterize
DAGs with high Π∥cc in terms of DR. Complementing these results, we provide new
upper and lower bounds on the Π∥cc of several important candidate iMHFs from the
literature. We give the first lower bounds on the memory hardness of the Catena
and Balloon Hashing functions in a parallel model of computation and we give the
first lower bounds of any kind for (a version) of Argon2i. Finally we describe
a new class of pebbling attacks improving on those of Alwen and Blocki (CRYPTO’16).
By instantiating these attacks we upperbound the Π∥cc of the Password Hashing
Competition winner Argon2i and one of the Balloon Hashing functions by O (n1.71).
We also show an upper bound of O(n1.625) for the Catena functions and the two
remaining Balloon Hashing functions.'
alternative_title:
- LNCS
author:
- first_name: Joel F
full_name: Alwen, Joel F
id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87
last_name: Alwen
- first_name: Jeremiah
full_name: Blocki, Jeremiah
last_name: Blocki
- first_name: Krzysztof Z
full_name: Pietrzak, Krzysztof Z
id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
last_name: Pietrzak
orcid: 0000-0002-9139-1654
citation:
ama: 'Alwen JF, Blocki J, Pietrzak KZ. Depth-robust graphs and their cumulative
memory complexity. In: Coron J-S, Buus Nielsen J, eds. Vol 10212. Springer; 2017:3-32.
doi:10.1007/978-3-319-56617-7_1'
apa: 'Alwen, J. F., Blocki, J., & Pietrzak, K. Z. (2017). Depth-robust graphs
and their cumulative memory complexity. In J.-S. Coron & J. Buus Nielsen (Eds.)
(Vol. 10212, pp. 3–32). Presented at the EUROCRYPT: Theory and Applications of
Cryptographic Techniques, Paris, France: Springer. https://doi.org/10.1007/978-3-319-56617-7_1'
chicago: Alwen, Joel F, Jeremiah Blocki, and Krzysztof Z Pietrzak. “Depth-Robust
Graphs and Their Cumulative Memory Complexity.” edited by Jean-Sébastien Coron
and Jesper Buus Nielsen, 10212:3–32. Springer, 2017. https://doi.org/10.1007/978-3-319-56617-7_1.
ieee: 'J. F. Alwen, J. Blocki, and K. Z. Pietrzak, “Depth-robust graphs and their
cumulative memory complexity,” presented at the EUROCRYPT: Theory and Applications
of Cryptographic Techniques, Paris, France, 2017, vol. 10212, pp. 3–32.'
ista: 'Alwen JF, Blocki J, Pietrzak KZ. 2017. Depth-robust graphs and their cumulative
memory complexity. EUROCRYPT: Theory and Applications of Cryptographic Techniques,
LNCS, vol. 10212, 3–32.'
mla: Alwen, Joel F., et al. Depth-Robust Graphs and Their Cumulative Memory Complexity.
Edited by Jean-Sébastien Coron and Jesper Buus Nielsen, vol. 10212, Springer,
2017, pp. 3–32, doi:10.1007/978-3-319-56617-7_1.
short: J.F. Alwen, J. Blocki, K.Z. Pietrzak, in:, J.-S. Coron, J. Buus Nielsen (Eds.),
Springer, 2017, pp. 3–32.
conference:
end_date: 2017-05-04
location: Paris, France
name: 'EUROCRYPT: Theory and Applications of Cryptographic Techniques'
start_date: 2017-04-30
date_created: 2018-12-11T11:47:39Z
date_published: 2017-04-01T00:00:00Z
date_updated: 2021-01-12T08:07:22Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-319-56617-7_1
ec_funded: 1
editor:
- first_name: Jean-Sébastien
full_name: Coron, Jean-Sébastien
last_name: Coron
- first_name: Jesper
full_name: Buus Nielsen, Jesper
last_name: Buus Nielsen
intvolume: ' 10212'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2016/875
month: '04'
oa: 1
oa_version: Submitted Version
page: 3 - 32
project:
- _id: 258AA5B2-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '682815'
name: Teaching Old Crypto New Tricks
publication_identifier:
isbn:
- 978-331956616-0
publication_status: published
publisher: Springer
publist_id: '7148'
quality_controlled: '1'
scopus_import: 1
status: public
title: Depth-robust graphs and their cumulative memory complexity
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10212
year: '2017'
...
---
_id: '641'
abstract:
- lang: eng
text: 'We introduce two novel methods for learning parameters of graphical models
for image labelling. The following two tasks underline both methods: (i) perturb
model parameters based on given features and ground truth labelings, so as to
exactly reproduce these labelings as optima of the local polytope relaxation of
the labelling problem; (ii) train a predictor for the perturbed model parameters
so that improved model parameters can be applied to the labelling of novel data.
Our first method implements task (i) by inverse linear programming and task (ii)
using a regressor e.g. a Gaussian process. Our second approach simultaneously
solves tasks (i) and (ii) in a joint manner, while being restricted to linearly
parameterised predictors. Experiments demonstrate the merits of both approaches.'
alternative_title:
- LNCS
author:
- first_name: Vera
full_name: Trajkovska, Vera
last_name: Trajkovska
- first_name: Paul
full_name: Swoboda, Paul
id: 446560C6-F248-11E8-B48F-1D18A9856A87
last_name: Swoboda
- first_name: Freddie
full_name: Åström, Freddie
last_name: Åström
- first_name: Stefanie
full_name: Petra, Stefanie
last_name: Petra
citation:
ama: 'Trajkovska V, Swoboda P, Åström F, Petra S. Graphical model parameter learning
by inverse linear programming. In: Lauze F, Dong Y, Bjorholm Dahl A, eds. Vol
10302. Springer; 2017:323-334. doi:10.1007/978-3-319-58771-4_26'
apa: 'Trajkovska, V., Swoboda, P., Åström, F., & Petra, S. (2017). Graphical
model parameter learning by inverse linear programming. In F. Lauze, Y. Dong,
& A. Bjorholm Dahl (Eds.) (Vol. 10302, pp. 323–334). Presented at the SSVM:
Scale Space and Variational Methods in Computer Vision, Kolding, Denmark: Springer.
https://doi.org/10.1007/978-3-319-58771-4_26'
chicago: Trajkovska, Vera, Paul Swoboda, Freddie Åström, and Stefanie Petra. “Graphical
Model Parameter Learning by Inverse Linear Programming.” edited by François Lauze,
Yiqiu Dong, and Anders Bjorholm Dahl, 10302:323–34. Springer, 2017. https://doi.org/10.1007/978-3-319-58771-4_26.
ieee: 'V. Trajkovska, P. Swoboda, F. Åström, and S. Petra, “Graphical model parameter
learning by inverse linear programming,” presented at the SSVM: Scale Space and
Variational Methods in Computer Vision, Kolding, Denmark, 2017, vol. 10302, pp.
323–334.'
ista: 'Trajkovska V, Swoboda P, Åström F, Petra S. 2017. Graphical model parameter
learning by inverse linear programming. SSVM: Scale Space and Variational Methods
in Computer Vision, LNCS, vol. 10302, 323–334.'
mla: Trajkovska, Vera, et al. Graphical Model Parameter Learning by Inverse Linear
Programming. Edited by François Lauze et al., vol. 10302, Springer, 2017,
pp. 323–34, doi:10.1007/978-3-319-58771-4_26.
short: V. Trajkovska, P. Swoboda, F. Åström, S. Petra, in:, F. Lauze, Y. Dong, A.
Bjorholm Dahl (Eds.), Springer, 2017, pp. 323–334.
conference:
end_date: 2017-06-08
location: Kolding, Denmark
name: 'SSVM: Scale Space and Variational Methods in Computer Vision'
start_date: 2017-06-04
date_created: 2018-12-11T11:47:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:07:23Z
day: '01'
department:
- _id: VlKo
doi: 10.1007/978-3-319-58771-4_26
editor:
- first_name: François
full_name: Lauze, François
last_name: Lauze
- first_name: Yiqiu
full_name: Dong, Yiqiu
last_name: Dong
- first_name: Anders
full_name: Bjorholm Dahl, Anders
last_name: Bjorholm Dahl
intvolume: ' 10302'
language:
- iso: eng
month: '01'
oa_version: None
page: 323 - 334
publication_identifier:
isbn:
- 978-331958770-7
publication_status: published
publisher: Springer
publist_id: '7147'
quality_controlled: '1'
scopus_import: 1
status: public
title: Graphical model parameter learning by inverse linear programming
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10302
year: '2017'
...
---
_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: '643'
abstract:
- lang: eng
text: It has been reported that nicotinamide-overload induces oxidative stress associated
with insulin resistance, the key feature of type 2 diabetes mellitus (T2DM). This
study aimed to investigate the effects of B vitamins in T2DM. Glucose tolerance
tests (GTT) were carried out in adult Sprague-Dawley rats treated with or without
cumulative doses of B vitamins. More specifically, insulin tolerance tests (ITT)
were also carried out in adult Sprague-Dawley rats treated with or without cumulative
doses of Vitamin B3. We found that cumulative Vitamin B1 and Vitamin B3 administration
significantly increased the plasma H2O2 levels associated with high insulin levels.
Only Vitamin B3 reduced muscular and hepatic glycogen contents. Cumulative administration
of nicotinic acid, another form of Vitamin B3, also significantly increased plasma
insulin level and H2O2 generation. Moreover, cumulative administration of nicotinic
acid or nicotinamide impaired glucose metabolism. This study suggested that excess
Vitamin B1 and Vitamin B3 caused oxidative stress and insulin resistance.
article_processing_charge: No
article_type: original
author:
- first_name: Wuping
full_name: Sun, Wuping
last_name: Sun
- first_name: Ming-Zhu
full_name: Zhai, Ming-Zhu
id: 34009CFA-F248-11E8-B48F-1D18A9856A87
last_name: Zhai
- first_name: Qian
full_name: Zhou, Qian
last_name: Zhou
- first_name: Chengrui
full_name: Qian, Chengrui
last_name: Qian
- first_name: Changyu
full_name: Jiang, Changyu
last_name: Jiang
citation:
ama: Sun W, Zhai M-Z, Zhou Q, Qian C, Jiang C. Effects of B vitamins overload on
plasma insulin level and hydrogen peroxide generation in rats. Chinese Journal
of Physiology. 2017;60(4):207-214. doi:10.4077/CJP.2017.BAF469
apa: Sun, W., Zhai, M.-Z., Zhou, Q., Qian, C., & Jiang, C. (2017). Effects of
B vitamins overload on plasma insulin level and hydrogen peroxide generation in
rats. Chinese Journal of Physiology. Chinese Physiological Society. https://doi.org/10.4077/CJP.2017.BAF469
chicago: Sun, Wuping, Ming-Zhu Zhai, Qian Zhou, Chengrui Qian, and Changyu Jiang.
“Effects of B Vitamins Overload on Plasma Insulin Level and Hydrogen Peroxide
Generation in Rats.” Chinese Journal of Physiology. Chinese Physiological
Society, 2017. https://doi.org/10.4077/CJP.2017.BAF469.
ieee: W. Sun, M.-Z. Zhai, Q. Zhou, C. Qian, and C. Jiang, “Effects of B vitamins
overload on plasma insulin level and hydrogen peroxide generation in rats,” Chinese
Journal of Physiology, vol. 60, no. 4. Chinese Physiological Society, pp.
207–214, 2017.
ista: Sun W, Zhai M-Z, Zhou Q, Qian C, Jiang C. 2017. Effects of B vitamins overload
on plasma insulin level and hydrogen peroxide generation in rats. Chinese Journal
of Physiology. 60(4), 207–214.
mla: Sun, Wuping, et al. “Effects of B Vitamins Overload on Plasma Insulin Level
and Hydrogen Peroxide Generation in Rats.” Chinese Journal of Physiology,
vol. 60, no. 4, Chinese Physiological Society, 2017, pp. 207–14, doi:10.4077/CJP.2017.BAF469.
short: W. Sun, M.-Z. Zhai, Q. Zhou, C. Qian, C. Jiang, Chinese Journal of Physiology
60 (2017) 207–214.
date_created: 2018-12-11T11:47:40Z
date_published: 2017-08-31T00:00:00Z
date_updated: 2021-01-12T08:07:28Z
day: '31'
ddc:
- '570'
department:
- _id: RySh
doi: 10.4077/CJP.2017.BAF469
external_id:
pmid:
- '28847140'
intvolume: ' 60'
issue: '4'
language:
- iso: eng
month: '08'
oa_version: Published Version
page: 207 - 214
pmid: 1
publication: Chinese Journal of Physiology
publication_identifier:
issn:
- '03044920'
publication_status: published
publisher: Chinese Physiological Society
publist_id: '7142'
quality_controlled: '1'
scopus_import: 1
status: public
title: Effects of B vitamins overload on plasma insulin level and hydrogen peroxide
generation in rats
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 60
year: '2017'
...
---
_id: '642'
abstract:
- lang: eng
text: Cauchy problems with SPDEs on the whole space are localized to Cauchy problems
on a ball of radius R. This localization reduces various kinds of spatial approximation
schemes to finite dimensional problems. The error is shown to be exponentially
small. As an application, a numerical scheme is presented which combines the localization
and the space and time discretization, and thus is fully implementable.
author:
- first_name: Mate
full_name: Gerencser, Mate
id: 44ECEDF2-F248-11E8-B48F-1D18A9856A87
last_name: Gerencser
- first_name: István
full_name: Gyöngy, István
last_name: Gyöngy
citation:
ama: Gerencser M, Gyöngy I. Localization errors in solving stochastic partial differential
equations in the whole space. Mathematics of Computation. 2017;86(307):2373-2397.
doi:10.1090/mcom/3201
apa: Gerencser, M., & Gyöngy, I. (2017). Localization errors in solving stochastic
partial differential equations in the whole space. Mathematics of Computation.
American Mathematical Society. https://doi.org/10.1090/mcom/3201
chicago: Gerencser, Mate, and István Gyöngy. “Localization Errors in Solving Stochastic
Partial Differential Equations in the Whole Space.” Mathematics of Computation.
American Mathematical Society, 2017. https://doi.org/10.1090/mcom/3201.
ieee: M. Gerencser and I. Gyöngy, “Localization errors in solving stochastic partial
differential equations in the whole space,” Mathematics of Computation,
vol. 86, no. 307. American Mathematical Society, pp. 2373–2397, 2017.
ista: Gerencser M, Gyöngy I. 2017. Localization errors in solving stochastic partial
differential equations in the whole space. Mathematics of Computation. 86(307),
2373–2397.
mla: Gerencser, Mate, and István Gyöngy. “Localization Errors in Solving Stochastic
Partial Differential Equations in the Whole Space.” Mathematics of Computation,
vol. 86, no. 307, American Mathematical Society, 2017, pp. 2373–97, doi:10.1090/mcom/3201.
short: M. Gerencser, I. Gyöngy, Mathematics of Computation 86 (2017) 2373–2397.
date_created: 2018-12-11T11:47:40Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:07:26Z
day: '01'
department:
- _id: JaMa
doi: 10.1090/mcom/3201
intvolume: ' 86'
issue: '307'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1508.05535
month: '01'
oa: 1
oa_version: Submitted Version
page: 2373 - 2397
publication: Mathematics of Computation
publication_identifier:
issn:
- '00255718'
publication_status: published
publisher: American Mathematical Society
publist_id: '7144'
quality_controlled: '1'
scopus_import: 1
status: public
title: Localization errors in solving stochastic partial differential equations in
the whole space
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 86
year: '2017'
...
---
_id: '645'
abstract:
- lang: eng
text: Markov decision processes (MDPs) are standard models for probabilistic systems
with non-deterministic behaviours. Long-run average rewards provide a mathematically
elegant formalism for expressing long term performance. Value iteration (VI) is
one of the simplest and most efficient algorithmic approaches to MDPs with other
properties, such as reachability objectives. Unfortunately, a naive extension
of VI does not work for MDPs with long-run average rewards, as there is no known
stopping criterion. In this work our contributions are threefold. (1) We refute
a conjecture related to stopping criteria for MDPs with long-run average rewards.
(2) We present two practical algorithms for MDPs with long-run average rewards
based on VI. First, we show that a combination of applying VI locally for each
maximal end-component (MEC) and VI for reachability objectives can provide approximation
guarantees. Second, extending the above approach with a simulation-guided on-demand
variant of VI, we present an anytime algorithm that is able to deal with very
large models. (3) Finally, we present experimental results showing that our methods
significantly outperform the standard approaches on several benchmarks.
alternative_title:
- LNCS
author:
- first_name: Pranav
full_name: Ashok, Pranav
last_name: Ashok
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
last_name: Meggendorfer
citation:
ama: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration
for long run average reward in markov decision processes. In: Majumdar R, Kunčak
V, eds. Vol 10426. Springer; 2017:201-221. doi:10.1007/978-3-319-63387-9_10'
apa: 'Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., & Meggendorfer, T.
(2017). Value iteration for long run average reward in markov decision processes.
In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at
the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_10'
chicago: Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and
Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision
Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer,
2017. https://doi.org/10.1007/978-3-319-63387-9_10.
ieee: 'P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value
iteration for long run average reward in markov decision processes,” presented
at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426,
pp. 201–221.'
ista: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration
for long run average reward in markov decision processes. CAV: Computer Aided
Verification, LNCS, vol. 10426, 201–221.'
mla: Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov
Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426,
Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.
short: P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R.
Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:47:41Z
date_published: 2017-07-13T00:00:00Z
date_updated: 2021-01-12T08:07:32Z
day: '13'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_10
ec_funded: 1
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
intvolume: ' 10426'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.02326
month: '07'
oa: 1
oa_version: Submitted Version
page: 201 - 221
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
isbn:
- 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7135'
quality_controlled: '1'
scopus_import: 1
status: public
title: Value iteration for long run average reward in markov decision processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10426
year: '2017'
...
---
_id: '644'
abstract:
- lang: eng
text: An instance of the valued constraint satisfaction problem (VCSP) is given
by a finite set of variables, a finite domain of labels, and a sum of functions,
each function depending on a subset of the variables. Each function can take finite
values specifying costs of assignments of labels to its variables or the infinite
value, which indicates an infeasible assignment. The goal is to find an assignment
of labels to the variables that minimizes the sum. We study, assuming that P 6=
NP, how the complexity of this very general problem depends on the set of functions
allowed in the instances, the so-called constraint language. The case when all
allowed functions take values in f0;1g corresponds to ordinary CSPs, where one
deals only with the feasibility issue, and there is no optimization. This case
is the subject of the algebraic CSP dichotomy conjecture predicting for which
constraint languages CSPs are tractable (i.e., solvable in polynomial time) and
for which they are NP-hard. The case when all allowed functions take only finite
values corresponds to a finitevalued CSP, where the feasibility aspect is trivial
and one deals only with the optimization issue. The complexity of finite-valued
CSPs was fully classified by Thapper and Živný. An algebraic necessary condition
for tractability of a general-valued CSP with a fixed constraint language was
recently given by Kozik and Ochremiak. As our main result, we prove that if a
constraint language satisfies this algebraic necessary condition, and the feasibility
CSP (i.e., the problem of deciding whether a given instance has a feasible solution)
corresponding to the VCSP with this language is tractable, then the VCSP is tractable.
The algorithm is a simple combination of the assumed algorithm for the feasibility
CSP and the standard LP relaxation. As a corollary, we obtain that a dichotomy
for ordinary CSPs would imply a dichotomy for general-valued CSPs.
author:
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
- first_name: Andrei
full_name: Krokhin, Andrei
last_name: Krokhin
- first_name: Michal
full_name: Rolinek, Michal
id: 3CB3BC06-F248-11E8-B48F-1D18A9856A87
last_name: Rolinek
citation:
ama: Kolmogorov V, Krokhin A, Rolinek M. The complexity of general-valued CSPs.
SIAM Journal on Computing. 2017;46(3):1087-1110. doi:10.1137/16M1091836
apa: Kolmogorov, V., Krokhin, A., & Rolinek, M. (2017). The complexity of general-valued
CSPs. SIAM Journal on Computing. SIAM. https://doi.org/10.1137/16M1091836
chicago: Kolmogorov, Vladimir, Andrei Krokhin, and Michal Rolinek. “The Complexity
of General-Valued CSPs.” SIAM Journal on Computing. SIAM, 2017. https://doi.org/10.1137/16M1091836.
ieee: V. Kolmogorov, A. Krokhin, and M. Rolinek, “The complexity of general-valued
CSPs,” SIAM Journal on Computing, vol. 46, no. 3. SIAM, pp. 1087–1110,
2017.
ista: Kolmogorov V, Krokhin A, Rolinek M. 2017. The complexity of general-valued
CSPs. SIAM Journal on Computing. 46(3), 1087–1110.
mla: Kolmogorov, Vladimir, et al. “The Complexity of General-Valued CSPs.” SIAM
Journal on Computing, vol. 46, no. 3, SIAM, 2017, pp. 1087–110, doi:10.1137/16M1091836.
short: V. Kolmogorov, A. Krokhin, M. Rolinek, SIAM Journal on Computing 46 (2017)
1087–1110.
date_created: 2018-12-11T11:47:40Z
date_published: 2017-06-29T00:00:00Z
date_updated: 2023-02-23T10:07:49Z
day: '29'
department:
- _id: VlKo
doi: 10.1137/16M1091836
ec_funded: 1
intvolume: ' 46'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1502.07327
month: '06'
oa: 1
oa_version: Preprint
page: 1087 - 1110
project:
- _id: 25FBA906-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '616160'
name: 'Discrete Optimization in Computer Vision: Theory and Practice'
publication: SIAM Journal on Computing
publication_status: published
publisher: SIAM
publist_id: '7138'
quality_controlled: '1'
related_material:
record:
- id: '1637'
relation: other
status: public
scopus_import: 1
status: public
title: The complexity of general-valued CSPs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 46
year: '2017'
...