---
_id: '140'
abstract:
- lang: eng
text: Reachability analysis is difficult for hybrid automata with affine differential
equations, because the reach set needs to be approximated. Promising abstraction
techniques usually employ interval methods or template polyhedra. Interval methods
account for dense time and guarantee soundness, and there are interval-based tools
that overapproximate affine flowpipes. But interval methods impose bounded and
rigid shapes, which make refinement expensive and fixpoint detection difficult.
Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded,
but sound template refinement for unbounded reachability analysis has been implemented
only for systems with piecewise constant dynamics. We capitalize on the advantages
of both techniques, combining interval arithmetic and template polyhedra, using
the former to abstract time and the latter to abstract space. During a CEGAR loop,
whenever a spurious error trajectory is found, we compute additional space constraints
and split time intervals, and use these space-time interpolants to eliminate the
counterexample. Space-time interpolation offers a lazy, flexible framework for
increasing precision while guaranteeing soundness, both for error avoidance and
fixpoint detection. To the best of out knowledge, this is the first abstraction
refinement scheme for the reachability analysis over unbounded and dense time
of affine hybrid systems, which is both sound and automatic. We demonstrate the
effectiveness of our algorithm with several benchmark examples, which cannot be
handled by other tools.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Mirco
full_name: Giacobbe, Mirco
id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
last_name: Giacobbe
orcid: 0000-0001-8180-0904
- 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: 'Frehse G, Giacobbe M, Henzinger TA. Space-time interpolants. In: Vol 10981.
Springer; 2018:468-486. doi:10.1007/978-3-319-96145-3_25'
apa: 'Frehse, G., Giacobbe, M., & Henzinger, T. A. (2018). Space-time interpolants
(Vol. 10981, pp. 468–486). Presented at the CAV: Computer Aided Verification,
Oxford, United Kingdom: Springer. https://doi.org/10.1007/978-3-319-96145-3_25'
chicago: Frehse, Goran, Mirco Giacobbe, and Thomas A Henzinger. “Space-Time Interpolants,”
10981:468–86. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_25.
ieee: 'G. Frehse, M. Giacobbe, and T. A. Henzinger, “Space-time interpolants,” presented
at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10981,
pp. 468–486.'
ista: 'Frehse G, Giacobbe M, Henzinger TA. 2018. Space-time interpolants. CAV: Computer
Aided Verification, LNCS, vol. 10981, 468–486.'
mla: Frehse, Goran, et al. Space-Time Interpolants. Vol. 10981, Springer,
2018, pp. 468–86, doi:10.1007/978-3-319-96145-3_25.
short: G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, pp. 468–486.
conference:
end_date: 2018-07-17
location: Oxford, United Kingdom
name: 'CAV: Computer Aided Verification'
start_date: 2018-07-14
date_created: 2018-12-11T11:44:50Z
date_published: 2018-07-18T00:00:00Z
date_updated: 2023-09-19T09:30:43Z
day: '18'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-96145-3_25
external_id:
isi:
- '000491481600025'
file:
- access_level: open_access
checksum: 6dca832f575d6b3f0ea9dff56f579142
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:53Z
date_updated: 2020-07-14T12:44:50Z
file_id: '5310'
file_name: IST-2018-1010-v1+1_space-time_interpolants.pdf
file_size: 563710
relation: main_file
file_date_updated: 2020-07-14T12:44:50Z
has_accepted_license: '1'
intvolume: ' 10981'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '07'
oa: 1
oa_version: Published Version
page: 468 - 486
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '7783'
pubrep_id: '1010'
quality_controlled: '1'
related_material:
record:
- id: '6894'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Space-time interpolants
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10981
year: '2018'
...
---
_id: '1116'
abstract:
- lang: eng
text: "Time-triggered switched networks are a deterministic communication infrastructure
used by real-time distributed embedded systems. Due to the criticality of the
applications running over them, developers need to ensure that end-to-end communication
is dependable and predictable. Traditional approaches assume static networks that
are not flexible to changes caused by reconfigurations or, more importantly, faults,
which are dealt with in the application using redundancy. We adopt the concept
of handling faults in the switches from non-real-time networks while maintaining
the required predictability. \r\n\r\nWe study a class of forwarding schemes that
can handle various types of failures. We consider probabilistic failures. We study
a class of forwarding schemes that can handle various types of failures. We consider
probabilistic failures. For a given network with a forwarding scheme and a constant
ℓ, we compute the {\\em score} of the scheme, namely the probability (induced
by faults) that at least ℓ messages arrive on time. We reduce the scoring problem
to a reachability problem on a Markov chain with a "product-like" structure.
Its special structure allows us to reason about it symbolically, and reduce the
scoring problem to #SAT. Our solution is generic and can be adapted to different
networks and other contexts. Also, we show the computational complexity of the
scoring problem is #P-complete, and we study methods to estimate the score. We
evaluate the effectiveness of our techniques with an implementation. "
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Shubham
full_name: Goel, Shubham
last_name: Goel
- 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: Guillermo
full_name: Rodríguez Navas, Guillermo
last_name: Rodríguez Navas
citation:
ama: 'Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding
schemes in switched networks with probabilistic faults. In: Vol 10206. Springer;
2017:169-187. doi:10.1007/978-3-662-54580-5_10'
apa: 'Avni, G., Goel, S., Henzinger, T. A., & Rodríguez Navas, G. (2017). Computing
scores of forwarding schemes in switched networks with probabilistic faults (Vol.
10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54580-5_10'
chicago: Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas.
“Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic
Faults,” 10206:169–87. Springer, 2017. https://doi.org/10.1007/978-3-662-54580-5_10.
ieee: 'G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores
of forwarding schemes in switched networks with probabilistic faults,” presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
Uppsala, Sweden, 2017, vol. 10206, pp. 169–187.'
ista: 'Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of
forwarding schemes in switched networks with probabilistic faults. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206,
169–187.'
mla: Avni, Guy, et al. Computing Scores of Forwarding Schemes in Switched Networks
with Probabilistic Faults. Vol. 10206, Springer, 2017, pp. 169–87, doi:10.1007/978-3-662-54580-5_10.
short: G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017,
pp. 169–187.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2018-12-11T11:50:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-09-20T11:32:43Z
day: '31'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-54580-5_10
external_id:
isi:
- '000440733400010'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:37Z
date_updated: 2018-12-12T10:08:37Z
file_id: '4698'
file_name: IST-2017-758-v1+1_tacas-cr.pdf
file_size: 321800
relation: main_file
file_date_updated: 2018-12-12T10:08:37Z
has_accepted_license: '1'
intvolume: ' 10206'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 169 - 187
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:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6246'
pubrep_id: '758'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing scores of forwarding schemes in switched networks with probabilistic
faults
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10206
year: '2017'
...
---
_id: '833'
abstract:
- lang: eng
text: We present an efficient algorithm to compute Euler characteristic curves of
gray scale images of arbitrary dimension. In various applications the Euler characteristic
curve is used as a descriptor of an image. Our algorithm is the first streaming
algorithm for Euler characteristic curves. The usage of streaming removes the
necessity to store the entire image in RAM. Experiments show that our implementation
handles terabyte scale images on commodity hardware. Due to lock-free parallelism,
it scales well with the number of processor cores. Additionally, we put the concept
of the Euler characteristic curve in the wider context of computational topology.
In particular, we explain the connection with persistence diagrams.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Teresa
full_name: Heiss, Teresa
id: 4879BB4E-F248-11E8-B48F-1D18A9856A87
last_name: Heiss
orcid: 0000-0002-1780-2689
- first_name: Hubert
full_name: Wagner, Hubert
id: 379CA8B8-F248-11E8-B48F-1D18A9856A87
last_name: Wagner
citation:
ama: 'Heiss T, Wagner H. Streaming algorithm for Euler characteristic curves of
multidimensional images. In: Felsberg M, Heyden A, Krüger N, eds. Vol 10424. Springer;
2017:397-409. doi:10.1007/978-3-319-64689-3_32'
apa: 'Heiss, T., & Wagner, H. (2017). Streaming algorithm for Euler characteristic
curves of multidimensional images. In M. Felsberg, A. Heyden, & N. Krüger
(Eds.) (Vol. 10424, pp. 397–409). Presented at the CAIP: Computer Analysis of
Images and Patterns, Ystad, Sweden: Springer. https://doi.org/10.1007/978-3-319-64689-3_32'
chicago: Heiss, Teresa, and Hubert Wagner. “Streaming Algorithm for Euler Characteristic
Curves of Multidimensional Images.” edited by Michael Felsberg, Anders Heyden,
and Norbert Krüger, 10424:397–409. Springer, 2017. https://doi.org/10.1007/978-3-319-64689-3_32.
ieee: 'T. Heiss and H. Wagner, “Streaming algorithm for Euler characteristic curves
of multidimensional images,” presented at the CAIP: Computer Analysis of Images
and Patterns, Ystad, Sweden, 2017, vol. 10424, pp. 397–409.'
ista: 'Heiss T, Wagner H. 2017. Streaming algorithm for Euler characteristic curves
of multidimensional images. CAIP: Computer Analysis of Images and Patterns, LNCS,
vol. 10424, 397–409.'
mla: Heiss, Teresa, and Hubert Wagner. Streaming Algorithm for Euler Characteristic
Curves of Multidimensional Images. Edited by Michael Felsberg et al., vol.
10424, Springer, 2017, pp. 397–409, doi:10.1007/978-3-319-64689-3_32.
short: T. Heiss, H. Wagner, in:, M. Felsberg, A. Heyden, N. Krüger (Eds.), Springer,
2017, pp. 397–409.
conference:
end_date: 2017-08-24
location: Ystad, Sweden
name: 'CAIP: Computer Analysis of Images and Patterns'
start_date: 2017-08-22
date_created: 2018-12-11T11:48:45Z
date_published: 2017-07-28T00:00:00Z
date_updated: 2023-09-26T16:10:03Z
day: '28'
department:
- _id: HeEd
doi: 10.1007/978-3-319-64689-3_32
editor:
- first_name: Michael
full_name: Felsberg, Michael
last_name: Felsberg
- first_name: Anders
full_name: Heyden, Anders
last_name: Heyden
- first_name: Norbert
full_name: Krüger, Norbert
last_name: Krüger
external_id:
isi:
- '000432085900032'
intvolume: ' 10424'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.02045
month: '07'
oa: 1
oa_version: Submitted Version
page: 397 - 409
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6815'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Streaming algorithm for Euler characteristic curves of multidimensional images
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10424
year: '2017'
...
---
_id: '650'
abstract:
- lang: eng
text: 'In this work we present a short and unified proof for the Strong and Weak
Regularity Lemma, based on the cryptographic tech-nique called low-complexity
approximations. In short, both problems reduce to a task of finding constructively
an approximation for a certain target function under a class of distinguishers
(test functions), where dis-tinguishers are combinations of simple rectangle-indicators.
In our case these approximations can be learned by a simple iterative procedure,
which yields a unified and simple proof, achieving for any graph with density
d and any approximation parameter the partition size. The novelty in our proof
is: (a) a simple approach which yields both strong and weaker variant, and (b)
improvements when d = o(1). At an abstract level, our proof can be seen a refinement
and simplification of the “analytic” proof given by Lovasz and Szegedy.'
alternative_title:
- LNCS
author:
- first_name: Maciej
full_name: Skórski, Maciej
id: EC09FA6A-02D0-11E9-8223-86B7C91467DD
last_name: Skórski
citation:
ama: 'Skórski M. A cryptographic view of regularity lemmas: Simpler unified proofs
and refined bounds. In: Jäger G, Steila S, eds. Vol 10185. Springer; 2017:586-599.
doi:10.1007/978-3-319-55911-7_42'
apa: 'Skórski, M. (2017). A cryptographic view of regularity lemmas: Simpler unified
proofs and refined bounds. In G. Jäger & S. Steila (Eds.) (Vol. 10185, pp.
586–599). Presented at the TAMC: Theory and Applications of Models of Computation,
Bern, Switzerland: Springer. https://doi.org/10.1007/978-3-319-55911-7_42'
chicago: 'Skórski, Maciej. “A Cryptographic View of Regularity Lemmas: Simpler Unified
Proofs and Refined Bounds.” edited by Gerhard Jäger and Silvia Steila, 10185:586–99.
Springer, 2017. https://doi.org/10.1007/978-3-319-55911-7_42.'
ieee: 'M. Skórski, “A cryptographic view of regularity lemmas: Simpler unified proofs
and refined bounds,” presented at the TAMC: Theory and Applications of Models
of Computation, Bern, Switzerland, 2017, vol. 10185, pp. 586–599.'
ista: 'Skórski M. 2017. A cryptographic view of regularity lemmas: Simpler unified
proofs and refined bounds. TAMC: Theory and Applications of Models of Computation,
LNCS, vol. 10185, 586–599.'
mla: 'Skórski, Maciej. A Cryptographic View of Regularity Lemmas: Simpler Unified
Proofs and Refined Bounds. Edited by Gerhard Jäger and Silvia Steila, vol.
10185, Springer, 2017, pp. 586–99, doi:10.1007/978-3-319-55911-7_42.'
short: M. Skórski, in:, G. Jäger, S. Steila (Eds.), Springer, 2017, pp. 586–599.
conference:
end_date: 2017-04-22
location: Bern, Switzerland
name: 'TAMC: Theory and Applications of Models of Computation'
start_date: 2017-04-20
date_created: 2018-12-11T11:47:42Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:07:46Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-319-55911-7_42
editor:
- first_name: Gerhard
full_name: Jäger, Gerhard
last_name: Jäger
- first_name: Silvia
full_name: Steila, Silvia
last_name: Steila
intvolume: ' 10185'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://eprint.iacr.org/2016/965.pdf
month: '01'
oa: 1
oa_version: Submitted Version
page: 586 - 599
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '7119'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'A cryptographic view of regularity lemmas: Simpler unified proofs and refined
bounds'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10185
year: '2017'
...
---
_id: '949'
abstract:
- lang: eng
text: The notion of treewidth of graphs has been exploited for faster algorithms
for several problems arising in verification and program analysis. Moreover, various
notions of balanced tree decompositions have been used for improved algorithms
supporting dynamic updates and analysis of concurrent programs. In this work,
we present a tool for constructing tree-decompositions of CFGs obtained from Java
methods, which is implemented as an extension to the widely used Soot framework.
The experimental results show that our implementation on real-world Java benchmarks
is very efficient. Our tool also provides the first implementation for balancing
tree-decompositions. In summary, we present the first tool support for exploiting
treewidth in the static analysis problems on Java programs.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- 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, Goharshady AK, Pavlogiannis A. JTDec: A tool for tree decompositions
in soot. In: D’Souza D, ed. Vol 10482. Springer; 2017:59-66. doi:10.1007/978-3-319-68167-2_4'
apa: 'Chatterjee, K., Goharshady, A. K., & Pavlogiannis, A. (2017). JTDec: A
tool for tree decompositions in soot. In D. D’Souza (Ed.) (Vol. 10482, pp. 59–66).
Presented at the ATVA: Automated Technology for Verification and Analysis, Pune,
India: Springer. https://doi.org/10.1007/978-3-319-68167-2_4'
chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis.
“JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66.
Springer, 2017. https://doi.org/10.1007/978-3-319-68167-2_4.'
ieee: 'K. Chatterjee, A. K. Goharshady, and A. Pavlogiannis, “JTDec: A tool for
tree decompositions in soot,” presented at the ATVA: Automated Technology for
Verification and Analysis, Pune, India, 2017, vol. 10482, pp. 59–66.'
ista: 'Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree
decompositions in soot. ATVA: Automated Technology for Verification and Analysis,
LNCS, vol. 10482, 59–66.'
mla: 'Chatterjee, Krishnendu, et al. JTDec: A Tool for Tree Decompositions in
Soot. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:10.1007/978-3-319-68167-2_4.'
short: K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer,
2017, pp. 59–66.
conference:
end_date: 2017-10-06
location: Pune, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2017-10-03
date_created: 2018-12-11T11:49:22Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2024-03-25T23:30:19Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.1007/978-3-319-68167-2_4
ec_funded: 1
editor:
- first_name: Deepak
full_name: D'Souza, Deepak
last_name: D'Souza
external_id:
isi:
- '000723567800004'
file:
- access_level: open_access
checksum: a0d9f5f94dc594c4e71e78525c9942f1
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:45Z
date_updated: 2020-07-14T12:48:16Z
file_id: '4835'
file_name: IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf
file_size: 948514
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 10482'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 59 - 66
project:
- _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:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6468'
pubrep_id: '845'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: 'JTDec: A tool for tree decompositions in soot'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10482
year: '2017'
...
---
_id: '962'
abstract:
- lang: eng
text: 'We present a new algorithm for model counting of a class of string constraints.
In addition to the classic operation of concatenation, our class includes some
recursively defined operations such as Kleene closure, and replacement of substrings.
Additionally, our class also includes length constraints on the string expressions,
which means, by requiring reasoning about numbers, that we face a multi-sorted
logic. In the end, our string constraints are motivated by their use in programming
for web applications. Our algorithm comprises two novel features: the ability
to use a technique of (1) partial derivatives for constraints that are already
in a solved form, i.e. a form where its (string) satisfiability is clearly displayed,
and (2) non-progression, where cyclic reasoning in the reduction process may be
terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally
compare our model counter with two recent works on model counting of similar constraints,
SMC [18] and ABC [5], to demonstrate its superior performance.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Minh
full_name: Trinh, Minh
last_name: Trinh
- first_name: Duc Hiep
full_name: Chu, Duc Hiep
id: 3598E630-F248-11E8-B48F-1D18A9856A87
last_name: Chu
- first_name: Joxan
full_name: Jaffar, Joxan
last_name: Jaffar
citation:
ama: 'Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings.
In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21'
apa: 'Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined
strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented
at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21'
chicago: Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined
Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer,
2017. https://doi.org/10.1007/978-3-319-63390-9_21.
ieee: 'M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined
strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany,
2017, vol. 10427, pp. 399–418.'
ista: 'Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings.
CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.'
mla: Trinh, Minh, et al. Model Counting for Recursively-Defined Strings.
Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418,
doi:10.1007/978-3-319-63390-9_21.
short: M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer,
2017, pp. 399–418.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:49:26Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2023-09-22T09:58:02Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-63390-9_21
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
external_id:
isi:
- '000431900900021'
intvolume: ' 10427'
isi: 1
language:
- iso: eng
month: '01'
oa_version: None
page: 399 - 418
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:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6443'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model counting for recursively-defined strings
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10427
year: '2017'
...
---
_id: '1011'
abstract:
- lang: eng
text: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly
equivalent, are standard models for interprocedural analysis. Yet RSMs are more
convenient as they (a) explicitly model function calls and returns, and (b) specify
many natural parameters for algorithmic analysis, e.g., the number of entries
and exits. We consider a general framework where RSM transitions are labeled from
a semiring and path properties are algebraic with semiring operations, which can
model, e.g., interprocedural reachability and dataflow analysis problems. Our
main contributions are new algorithms for several fundamental problems. As compared
to a direct translation of RSMs to PDSs and the best-known existing bounds of
PDSs, our analysis algorithm improves the complexity for finite-height semirings
(that subsumes reachability and standard dataflow properties). We further consider
the problem of extracting distance values from the representation structures computed
by our algorithm, and give efficient algorithms that distinguish the complexity
of a one-time preprocessing from the complexity of each individual query. Another
advantage of our algorithm is that our improvements carry over to the concurrent
setting, where we improve the bestknown complexity for the context-bounded analysis
of concurrent RSMs. Finally, we provide a prototype implementation that gives
a significant speed-up on several benchmarks from the SLAM/SDV project.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
- first_name: Samarth
full_name: Mishra, Samarth
last_name: Mishra
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted
recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11'
apa: 'Chatterjee, K., Kragl, B., Mishra, S., & Pavlogiannis, A. (2017). Faster
algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201,
pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala,
Sweden: Springer. https://doi.org/10.1007/978-3-662-54434-1_11'
chicago: Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis.
“Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok
Yang, 10201:287–313. Springer, 2017. https://doi.org/10.1007/978-3-662-54434-1_11.
ieee: 'K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms
for weighted recursive state machines,” presented at the ESOP: European Symposium
on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.'
ista: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms
for weighted recursive state machines. ESOP: European Symposium on Programming,
LNCS, vol. 10201, 287–313.'
mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive
State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
doi:10.1007/978-3-662-54434-1_11.
short: K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.),
Springer, 2017, pp. 287–313.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'ESOP: European Symposium on Programming'
start_date: 2017-04-22
date_created: 2018-12-11T11:49:41Z
date_published: 2017-03-19T00:00:00Z
date_updated: 2023-09-22T09:44:50Z
day: '19'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-54434-1_11
ec_funded: 1
editor:
- first_name: Hongseok
full_name: Yang, Hongseok
last_name: Yang
external_id:
isi:
- '000681702400011'
intvolume: ' 10201'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1701.04914
month: '03'
oa: 1
oa_version: Submitted Version
page: 287 - 313
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6384'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for weighted recursive state machines
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10201
year: '2017'
...
---
_id: '989'
abstract:
- lang: eng
text: We present a generalized optimal transport model in which the mass-preserving
constraint for the L2-Wasserstein distance is relaxed by introducing a source
term in the continuity equation. The source term is also incorporated in the path
energy by means of its squared L2-norm in time of a functional with linear growth
in space. This extension of the original transport model enables local density
modulations, which is a desirable feature in applications such as image warping
and blending. A key advantage of the use of a functional with linear growth in
space is that it allows for singular sources and sinks, which can be supported
on points or lines. On a technical level, the L2-norm in time ensures a disintegration
of the source in time, which we use to obtain the well-posedness of the model
and the existence of geodesic paths. The numerical discretization is based on
the proximal splitting approach [18] and selected numerical test cases show the
potential of the proposed approach. Furthermore, the approach is applied to the
warping and blending of textures.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jan
full_name: Maas, Jan
id: 4C5696CE-F248-11E8-B48F-1D18A9856A87
last_name: Maas
orcid: 0000-0002-0845-1338
- first_name: Martin
full_name: Rumpf, Martin
last_name: Rumpf
- first_name: Stefan
full_name: Simon, Stefan
last_name: Simon
citation:
ama: 'Maas J, Rumpf M, Simon S. Transport based image morphing with intensity modulation.
In: Lauze F, Dong Y, Bjorholm Dahl A, eds. Vol 10302. Springer; 2017:563-577.
doi:10.1007/978-3-319-58771-4_45'
apa: 'Maas, J., Rumpf, M., & Simon, S. (2017). Transport based image morphing
with intensity modulation. In F. Lauze, Y. Dong, & A. Bjorholm Dahl (Eds.)
(Vol. 10302, pp. 563–577). 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_45'
chicago: Maas, Jan, Martin Rumpf, and Stefan Simon. “Transport Based Image Morphing
with Intensity Modulation.” edited by François Lauze, Yiqiu Dong, and Anders Bjorholm
Dahl, 10302:563–77. Springer, 2017. https://doi.org/10.1007/978-3-319-58771-4_45.
ieee: J. Maas, M. Rumpf, and S. Simon, “Transport based image morphing with intensity
modulation,” presented at the SSVM: Scale Space and Variational Methods in Computer
Vision, Kolding, Denmark, 2017, vol. 10302, pp. 563–577.
ista: Maas J, Rumpf M, Simon S. 2017. Transport based image morphing with intensity
modulation. SSVM: Scale Space and Variational Methods in Computer Vision, LNCS,
vol. 10302, 563–577.
mla: Maas, Jan, et al. Transport Based Image Morphing with Intensity Modulation.
Edited by François Lauze et al., vol. 10302, Springer, 2017, pp. 563–77, doi:10.1007/978-3-319-58771-4_45.
short: J. Maas, M. Rumpf, S. Simon, in:, F. Lauze, Y. Dong, A. Bjorholm Dahl (Eds.),
Springer, 2017, pp. 563–577.
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:49:34Z
date_published: 2017-05-18T00:00:00Z
date_updated: 2023-09-22T09:55:50Z
day: '18'
department:
- _id: JaMa
doi: 10.1007/978-3-319-58771-4_45
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
external_id:
isi:
- '000432210900045'
intvolume: ' 10302'
isi: 1
language:
- iso: eng
month: '05'
oa_version: None
page: 563 - 577
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6410'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Transport based image morphing with intensity modulation
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10302
year: '2017'
...
---
_id: '9648'
abstract:
- lang: eng
text: In this paper, we establish a correspondence between the incremental algorithm
for computing AT-models [8,9] and the one for computing persistent homology [6,14,15].
We also present a decremental algorithm for computing AT-models that allows to
extend the persistence computation to a wider setting. Finally, we show how to
combine incremental and decremental techniques for persistent homology computation.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rocio
full_name: Gonzalez-Diaz, Rocio
last_name: Gonzalez-Diaz
- first_name: Adrian
full_name: Ion, Adrian
id: 29F89302-F248-11E8-B48F-1D18A9856A87
last_name: Ion
- first_name: Maria Jose
full_name: Jimenez, Maria Jose
last_name: Jimenez
- first_name: Regina
full_name: Poyatos, Regina
last_name: Poyatos
citation:
ama: 'Gonzalez-Diaz R, Ion A, Jimenez MJ, Poyatos R. Incremental-decremental algorithm
for computing AT-models and persistent homology. In: Computer Analysis of Images
and Patterns. Vol 6854. Springer Nature; 2011:286-293. doi:10.1007/978-3-642-23672-3_35'
apa: 'Gonzalez-Diaz, R., Ion, A., Jimenez, M. J., & Poyatos, R. (2011). Incremental-decremental
algorithm for computing AT-models and persistent homology. In Computer Analysis
of Images and Patterns (Vol. 6854, pp. 286–293). Seville, Spain: Springer
Nature. https://doi.org/10.1007/978-3-642-23672-3_35'
chicago: Gonzalez-Diaz, Rocio, Adrian Ion, Maria Jose Jimenez, and Regina Poyatos.
“Incremental-Decremental Algorithm for Computing AT-Models and Persistent Homology.”
In Computer Analysis of Images and Patterns, 6854:286–93. Springer Nature,
2011. https://doi.org/10.1007/978-3-642-23672-3_35.
ieee: R. Gonzalez-Diaz, A. Ion, M. J. Jimenez, and R. Poyatos, “Incremental-decremental
algorithm for computing AT-models and persistent homology,” in Computer Analysis
of Images and Patterns, Seville, Spain, 2011, vol. 6854, pp. 286–293.
ista: 'Gonzalez-Diaz R, Ion A, Jimenez MJ, Poyatos R. 2011. Incremental-decremental
algorithm for computing AT-models and persistent homology. Computer Analysis of
Images and Patterns. CAIP: International Conference on Computer Analysis of Images
and Patterns, LNCS, vol. 6854, 286–293.'
mla: Gonzalez-Diaz, Rocio, et al. “Incremental-Decremental Algorithm for Computing
AT-Models and Persistent Homology.” Computer Analysis of Images and Patterns,
vol. 6854, Springer Nature, 2011, pp. 286–93, doi:10.1007/978-3-642-23672-3_35.
short: R. Gonzalez-Diaz, A. Ion, M.J. Jimenez, R. Poyatos, in:, Computer Analysis
of Images and Patterns, Springer Nature, 2011, pp. 286–293.
conference:
end_date: 2011-08-31
location: Seville, Spain
name: 'CAIP: International Conference on Computer Analysis of Images and Patterns'
start_date: 2011-08-29
date_created: 2021-07-11T22:01:19Z
date_published: 2011-08-01T00:00:00Z
date_updated: 2021-08-12T13:53:17Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-642-23672-3_35
intvolume: ' 6854'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://hdl.handle.net/11441/30766
month: '08'
oa: 1
oa_version: Published Version
page: 286-293
publication: Computer Analysis of Images and Patterns
publication_identifier:
eissn:
- '16113349'
isbn:
- '9783642236716'
issn:
- '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Incremental-decremental algorithm for computing AT-models and persistent homology
type: conference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
volume: 6854
year: '2011'
...