---
_id: '5801'
abstract:
- lang: eng
text: Space filling circles and spheres have various applications in mathematical
imaging and physical modeling. In this paper, we first show how the thinnest (i.e.,
2-minimal) model of digital sphere can be augmented to a space filling model by
fixing certain “simple voxels” and “filler voxels” associated with it. Based on
elementary number-theoretic properties of such voxels, we design an efficient
incremental algorithm for generation of these space filling spheres with successively
increasing radius. The novelty of the proposed technique is established further
through circular space filling on 3D digital plane. As evident from a preliminary
set of experimental result, this can particularly be useful for parallel computing
of 3D Voronoi diagrams in the digital space.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Shivam
full_name: Dwivedi, Shivam
last_name: Dwivedi
- first_name: Aniket
full_name: Gupta, Aniket
last_name: Gupta
- first_name: Siddhant
full_name: Roy, Siddhant
last_name: Roy
- first_name: Ranita
full_name: Biswas, Ranita
id: 3C2B033E-F248-11E8-B48F-1D18A9856A87
last_name: Biswas
orcid: 0000-0002-5372-7890
- first_name: Partha
full_name: Bhowmick, Partha
last_name: Bhowmick
citation:
ama: 'Dwivedi S, Gupta A, Roy S, Biswas R, Bhowmick P. Fast and Efficient Incremental
Algorithms for Circular and Spherical Propagation in Integer Space. In: 20th
IAPR International Conference. Vol 10502. Cham: Springer Nature; 2017:347-359.
doi:10.1007/978-3-319-66272-5_28'
apa: 'Dwivedi, S., Gupta, A., Roy, S., Biswas, R., & Bhowmick, P. (2017). Fast
and Efficient Incremental Algorithms for Circular and Spherical Propagation in
Integer Space. In 20th IAPR International Conference (Vol. 10502, pp. 347–359).
Cham: Springer Nature. https://doi.org/10.1007/978-3-319-66272-5_28'
chicago: 'Dwivedi, Shivam, Aniket Gupta, Siddhant Roy, Ranita Biswas, and Partha
Bhowmick. “Fast and Efficient Incremental Algorithms for Circular and Spherical
Propagation in Integer Space.” In 20th IAPR International Conference, 10502:347–59.
Cham: Springer Nature, 2017. https://doi.org/10.1007/978-3-319-66272-5_28.'
ieee: S. Dwivedi, A. Gupta, S. Roy, R. Biswas, and P. Bhowmick, “Fast and Efficient
Incremental Algorithms for Circular and Spherical Propagation in Integer Space,”
in 20th IAPR International Conference, Vienna, Austria, 2017, vol. 10502,
pp. 347–359.
ista: 'Dwivedi S, Gupta A, Roy S, Biswas R, Bhowmick P. 2017. Fast and Efficient
Incremental Algorithms for Circular and Spherical Propagation in Integer Space.
20th IAPR International Conference. DGCI: International Conference on Discrete
Geometry for Computer Imagery, LNCS, vol. 10502, 347–359.'
mla: Dwivedi, Shivam, et al. “Fast and Efficient Incremental Algorithms for Circular
and Spherical Propagation in Integer Space.” 20th IAPR International Conference,
vol. 10502, Springer Nature, 2017, pp. 347–59, doi:10.1007/978-3-319-66272-5_28.
short: S. Dwivedi, A. Gupta, S. Roy, R. Biswas, P. Bhowmick, in:, 20th IAPR International
Conference, Springer Nature, Cham, 2017, pp. 347–359.
conference:
end_date: 2017-09-21
location: Vienna, Austria
name: 'DGCI: International Conference on Discrete Geometry for Computer Imagery'
start_date: 2017-09-19
date_created: 2019-01-08T20:42:22Z
date_published: 2017-08-22T00:00:00Z
date_updated: 2022-01-27T15:34:25Z
day: '22'
doi: 10.1007/978-3-319-66272-5_28
extern: '1'
intvolume: ' 10502'
language:
- iso: eng
month: '08'
oa_version: None
page: 347-359
place: Cham
publication: 20th IAPR International Conference
publication_identifier:
eisbn:
- 978-3-319-66272-5
eissn:
- 1611-3349
isbn:
- 978-3-319-66271-8
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation
in Integer Space
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 10502
year: '2017'
...
---
_id: '5802'
abstract:
- lang: eng
text: This papers introduces a definition of digital primitives based on focal points
and weighted distances (with positive weights). The proposed definition is applicable
to general dimensions and covers in its gamut various regular curves and surfaces
like circles, ellipses, digital spheres and hyperspheres, ellipsoids and k-ellipsoids,
Cartesian k-ovals, etc. Several interesting properties are presented for this
class of digital primitives such as space partitioning, topological separation,
and connectivity properties. To demonstrate further the potential of this new
way of defining digital primitives, we propose, as extension, another class of
digital conics defined by focus-directrix combination.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Eric
full_name: Andres, Eric
last_name: Andres
- first_name: Ranita
full_name: Biswas, Ranita
id: 3C2B033E-F248-11E8-B48F-1D18A9856A87
last_name: Biswas
orcid: 0000-0002-5372-7890
- first_name: Partha
full_name: Bhowmick, Partha
last_name: Bhowmick
citation:
ama: 'Andres E, Biswas R, Bhowmick P. Digital primitives defined by weighted focal
set. In: 20th IAPR International Conference. Vol 10502. Cham: Springer
Nature; 2017:388-398. doi:10.1007/978-3-319-66272-5_31'
apa: 'Andres, E., Biswas, R., & Bhowmick, P. (2017). Digital primitives defined
by weighted focal set. In 20th IAPR International Conference (Vol. 10502,
pp. 388–398). Cham: Springer Nature. https://doi.org/10.1007/978-3-319-66272-5_31'
chicago: 'Andres, Eric, Ranita Biswas, and Partha Bhowmick. “Digital Primitives
Defined by Weighted Focal Set.” In 20th IAPR International Conference,
10502:388–98. Cham: Springer Nature, 2017. https://doi.org/10.1007/978-3-319-66272-5_31.'
ieee: E. Andres, R. Biswas, and P. Bhowmick, “Digital primitives defined by weighted
focal set,” in 20th IAPR International Conference, Vienna, Austria, 2017,
vol. 10502, pp. 388–398.
ista: 'Andres E, Biswas R, Bhowmick P. 2017. Digital primitives defined by weighted
focal set. 20th IAPR International Conference. DGCI: International Conference
on Discrete Geometry for Computer Imagery, LNCS, vol. 10502, 388–398.'
mla: Andres, Eric, et al. “Digital Primitives Defined by Weighted Focal Set.” 20th
IAPR International Conference, vol. 10502, Springer Nature, 2017, pp. 388–98,
doi:10.1007/978-3-319-66272-5_31.
short: E. Andres, R. Biswas, P. Bhowmick, in:, 20th IAPR International Conference,
Springer Nature, Cham, 2017, pp. 388–398.
conference:
end_date: 2017-09-21
location: Vienna, Austria
name: 'DGCI: International Conference on Discrete Geometry for Computer Imagery'
start_date: 2017-09-19
date_created: 2019-01-08T20:42:39Z
date_published: 2017-08-22T00:00:00Z
date_updated: 2022-01-27T15:38:35Z
day: '22'
doi: 10.1007/978-3-319-66272-5_31
extern: '1'
intvolume: ' 10502'
language:
- iso: eng
month: '08'
oa_version: None
page: 388-398
place: Cham
publication: 20th IAPR International Conference
publication_identifier:
eisbn:
- 978-3-319-66272-5
eissn:
- 1611-3349
isbn:
- 978-3-319-66271-8
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: Digital primitives defined by weighted focal set
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 10502
year: '2017'
...
---
_id: '5805'
abstract:
- lang: eng
text: Discretization of sphere in the integer space follows a particular discretization
scheme, which, in principle, conforms to some topological model. This eventually
gives rise to interesting topological properties of a discrete spherical surface,
which need to be investigated for its analytical characterization. This paper
presents some novel results on the local topological properties of the naive model
of discrete sphere. They follow from the bijection of each quadraginta octant
of naive sphere with its projection map called f -map on the corresponding functional
plane and from the characterization of certain jumps in the f-map. As an application,
we have shown how these properties can be used in designing an efficient reconstruction
algorithm for a naive spherical surface from an input voxel set when it is sparse
or noisy.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Nabhasmita
full_name: Sen, Nabhasmita
last_name: Sen
- first_name: Ranita
full_name: Biswas, Ranita
id: 3C2B033E-F248-11E8-B48F-1D18A9856A87
last_name: Biswas
orcid: 0000-0002-5372-7890
- first_name: Partha
full_name: Bhowmick, Partha
last_name: Bhowmick
citation:
ama: 'Sen N, Biswas R, Bhowmick P. On some local topological properties of naive
discrete sphere. In: Computational Topology in Image Context. Vol 9667.
Cham: Springer Nature; 2016:253-264. doi:10.1007/978-3-319-39441-1_23'
apa: 'Sen, N., Biswas, R., & Bhowmick, P. (2016). On some local topological
properties of naive discrete sphere. In Computational Topology in Image Context
(Vol. 9667, pp. 253–264). Cham: Springer Nature. https://doi.org/10.1007/978-3-319-39441-1_23'
chicago: 'Sen, Nabhasmita, Ranita Biswas, and Partha Bhowmick. “On Some Local Topological
Properties of Naive Discrete Sphere.” In Computational Topology in Image Context,
9667:253–64. Cham: Springer Nature, 2016. https://doi.org/10.1007/978-3-319-39441-1_23.'
ieee: 'N. Sen, R. Biswas, and P. Bhowmick, “On some local topological properties
of naive discrete sphere,” in Computational Topology in Image Context,
vol. 9667, Cham: Springer Nature, 2016, pp. 253–264.'
ista: 'Sen N, Biswas R, Bhowmick P. 2016.On some local topological properties of
naive discrete sphere. In: Computational Topology in Image Context. LNCS, vol.
9667, 253–264.'
mla: Sen, Nabhasmita, et al. “On Some Local Topological Properties of Naive Discrete
Sphere.” Computational Topology in Image Context, vol. 9667, Springer Nature,
2016, pp. 253–64, doi:10.1007/978-3-319-39441-1_23.
short: N. Sen, R. Biswas, P. Bhowmick, in:, Computational Topology in Image Context,
Springer Nature, Cham, 2016, pp. 253–264.
conference:
end_date: 2016-06-17
location: Marseille, France
name: 'CTIC: Computational Topology in Image Context'
start_date: 2016-06-15
date_created: 2019-01-08T20:44:24Z
date_published: 2016-06-02T00:00:00Z
date_updated: 2022-01-28T08:01:22Z
day: '02'
department:
- _id: HeEd
doi: 10.1007/978-3-319-39441-1_23
extern: '1'
intvolume: ' 9667'
language:
- iso: eng
month: '06'
oa_version: None
page: 253-264
place: Cham
publication: Computational Topology in Image Context
publication_identifier:
eisbn:
- 978-3-319-39441-1
eissn:
- 1611-3349
isbn:
- 978-3-319-39440-4
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: On some local topological properties of naive discrete sphere
type: book_chapter
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9667
year: '2016'
...
---
_id: '5809'
abstract:
- lang: eng
text: A discrete spherical circle is a topologically well-connected 3D circle in
the integer space, which belongs to a discrete sphere as well as a discrete plane.
It is one of the most important 3D geometric primitives, but has not possibly
yet been studied up to its merit. This paper is a maiden exposition of some of
its elementary properties, which indicates a sense of its profound theoretical
prospects in the framework of digital geometry. We have shown how different types
of discretization can lead to forbidden and admissible classes, when one attempts
to define the discretization of a spherical circle in terms of intersection between
a discrete sphere and a discrete plane. Several fundamental theoretical results
have been presented, the algorithm for construction of discrete spherical circles
has been discussed, and some test results have been furnished to demonstrate its
practicality and usefulness.
article_processing_charge: No
author:
- first_name: Ranita
full_name: Biswas, Ranita
id: 3C2B033E-F248-11E8-B48F-1D18A9856A87
last_name: Biswas
orcid: 0000-0002-5372-7890
- first_name: Partha
full_name: Bhowmick, Partha
last_name: Bhowmick
- first_name: Valentin E.
full_name: Brimkov, Valentin E.
last_name: Brimkov
citation:
ama: 'Biswas R, Bhowmick P, Brimkov VE. On the connectivity and smoothness of discrete
spherical circles. In: Combinatorial Image Analysis. Vol 9448. Cham: Springer
Nature; 2016:86-100. doi:10.1007/978-3-319-26145-4_7'
apa: 'Biswas, R., Bhowmick, P., & Brimkov, V. E. (2016). On the connectivity
and smoothness of discrete spherical circles. In Combinatorial image analysis
(Vol. 9448, pp. 86–100). Cham: Springer Nature. https://doi.org/10.1007/978-3-319-26145-4_7'
chicago: 'Biswas, Ranita, Partha Bhowmick, and Valentin E. Brimkov. “On the Connectivity
and Smoothness of Discrete Spherical Circles.” In Combinatorial Image Analysis,
9448:86–100. Cham: Springer Nature, 2016. https://doi.org/10.1007/978-3-319-26145-4_7.'
ieee: 'R. Biswas, P. Bhowmick, and V. E. Brimkov, “On the connectivity and smoothness
of discrete spherical circles,” in Combinatorial image analysis, vol. 9448,
Cham: Springer Nature, 2016, pp. 86–100.'
ista: 'Biswas R, Bhowmick P, Brimkov VE. 2016.On the connectivity and smoothness
of discrete spherical circles. In: Combinatorial image analysis. vol. 9448, 86–100.'
mla: Biswas, Ranita, et al. “On the Connectivity and Smoothness of Discrete Spherical
Circles.” Combinatorial Image Analysis, vol. 9448, Springer Nature, 2016,
pp. 86–100, doi:10.1007/978-3-319-26145-4_7.
short: R. Biswas, P. Bhowmick, V.E. Brimkov, in:, Combinatorial Image Analysis,
Springer Nature, Cham, 2016, pp. 86–100.
conference:
end_date: 2015-11-27
location: Kolkata, India
name: 'IWCIA: International Workshop on Combinatorial Image Analysis'
start_date: 2015-11-24
date_created: 2019-01-08T20:45:19Z
date_published: 2016-01-06T00:00:00Z
date_updated: 2022-01-28T08:13:03Z
day: '06'
department:
- _id: HeEd
doi: 10.1007/978-3-319-26145-4_7
extern: '1'
intvolume: ' 9448'
language:
- iso: eng
month: '01'
oa_version: None
page: 86-100
place: Cham
publication: Combinatorial image analysis
publication_identifier:
eisbn:
- 978-3-319-26145-4
eissn:
- 1611-3349
isbn:
- 978-3-319-26144-7
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
status: public
title: On the connectivity and smoothness of discrete spherical circles
type: book_chapter
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9448
year: '2016'
...
---
_id: '1094'
abstract:
- lang: eng
text: Immunogold labeling of freeze-fracture replicas has recently been used for
high-resolution visualization of protein localization in electron microscopy.
This method has higher labeling efficiency than conventional immunogold methods
for membrane molecules allowing precise quantitative measurements. However, one
of the limitations of freeze-fracture replica immunolabeling is difficulty in
keeping structural orientation and identifying labeled profiles in complex tissues
like brain. The difficulty is partly due to fragmentation of freeze-fracture replica
preparations during labeling procedures and limited morphological clues on the
replica surface. To overcome these issues, we introduce here a grid-glued replica
method combined with SEM observation. This method allows histological staining
before dissolving the tissue and easy handling of replicas during immunogold labeling,
and keeps the whole replica surface intact without fragmentation. The procedure
described here is also useful for matched double-replica analysis allowing further
identification of labeled profiles in corresponding P-face and E-face.
acknowledged_ssus:
- _id: EM-Fac
acknowledgement: 'We thank Prof. Elek Molnár for providing us a pan-AMPAR anti-body
used in Fig.2 and Dr. Ludek Lovicar for technical assistance in scanning electron
microscope imaging. This work was supported by the European Union (HBP—Project Ref.
604102). '
alternative_title:
- Methods in Molecular Biology
article_processing_charge: No
author:
- first_name: Harumi
full_name: Harada, Harumi
id: 2E55CDF2-F248-11E8-B48F-1D18A9856A87
last_name: Harada
orcid: 0000-0001-7429-7896
- first_name: Ryuichi
full_name: Shigemoto, Ryuichi
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
citation:
ama: 'Harada H, Shigemoto R. Immunogold protein localization on grid-glued freeze-fracture
replicas. In: High-Resolution Imaging of Cellular Proteins. Vol 1474. Springer;
2016:203-216. doi:10.1007/978-1-4939-6352-2_12'
apa: Harada, H., & Shigemoto, R. (2016). Immunogold protein localization on
grid-glued freeze-fracture replicas. In High-Resolution Imaging of Cellular
Proteins (Vol. 1474, pp. 203–216). Springer. https://doi.org/10.1007/978-1-4939-6352-2_12
chicago: Harada, Harumi, and Ryuichi Shigemoto. “Immunogold Protein Localization
on Grid-Glued Freeze-Fracture Replicas.” In High-Resolution Imaging of Cellular
Proteins, 1474:203–16. Springer, 2016. https://doi.org/10.1007/978-1-4939-6352-2_12.
ieee: H. Harada and R. Shigemoto, “Immunogold protein localization on grid-glued
freeze-fracture replicas,” in High-Resolution Imaging of Cellular Proteins,
vol. 1474, Springer, 2016, pp. 203–216.
ista: 'Harada H, Shigemoto R. 2016.Immunogold protein localization on grid-glued
freeze-fracture replicas. In: High-Resolution Imaging of Cellular Proteins. Methods
in Molecular Biology, vol. 1474, 203–216.'
mla: Harada, Harumi, and Ryuichi Shigemoto. “Immunogold Protein Localization on
Grid-Glued Freeze-Fracture Replicas.” High-Resolution Imaging of Cellular Proteins,
vol. 1474, Springer, 2016, pp. 203–16, doi:10.1007/978-1-4939-6352-2_12.
short: H. Harada, R. Shigemoto, in:, High-Resolution Imaging of Cellular Proteins,
Springer, 2016, pp. 203–216.
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-12T00:00:00Z
date_updated: 2023-09-05T14:09:01Z
day: '12'
department:
- _id: RySh
doi: 10.1007/978-1-4939-6352-2_12
ec_funded: 1
intvolume: ' 1474'
language:
- iso: eng
month: '08'
oa_version: None
page: 203 - 216
project:
- _id: 25CD3DD2-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '604102'
name: Localization of ion channels and receptors by two and three-dimensional immunoelectron
microscopic approaches
publication: High-Resolution Imaging of Cellular Proteins
publication_identifier:
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer
publist_id: '6281'
quality_controlled: '1'
status: public
title: Immunogold protein localization on grid-glued freeze-fracture replicas
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 1474
year: '2016'
...
---
_id: '10884'
abstract:
- lang: eng
text: "We revisit the parameterized model checking problem for token-passing systems
and specifications in indexed CTL ∗ \\X. Emerson and Namjoshi (1995, 2003) have
shown that parameterized model checking of indexed CTL ∗ \\X in uni-directional
token rings can be reduced to checking rings up to some cutoff size. Clarke et
al. (2004) have shown a similar result for general topologies and indexed LTL
\\X, provided processes cannot choose the directions for sending or receiving
the token.\r\nWe unify and substantially extend these results by systematically
exploring fragments of indexed CTL ∗ \\X with respect to general topologies.
For each fragment we establish whether a cutoff exists, and for some concrete
topologies, such as rings, cliques and stars, we infer small cutoffs. Finally,
we show that the problem becomes undecidable, and thus no cutoffs exist, if processes
are allowed to choose the directions in which they send or from which they receive
the token."
acknowledgement: "This work was supported by the Austrian Science Fund through grant
P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23);
ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants
PROSEED, ICT12-059, and VRG11-005."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Benjamin
full_name: Aminof, Benjamin
id: 4A55BD00-F248-11E8-B48F-1D18A9856A87
last_name: Aminof
- first_name: Swen
full_name: Jacobs, Swen
last_name: Jacobs
- first_name: Ayrat
full_name: Khalimov, Ayrat
last_name: Khalimov
- first_name: Sasha
full_name: Rubin, Sasha
id: 2EC51194-F248-11E8-B48F-1D18A9856A87
last_name: Rubin
citation:
ama: 'Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing
systems. In: Verification, Model Checking, and Abstract Interpretation.
Vol 8318. Springer Nature; 2014:262-281. doi:10.1007/978-3-642-54013-4_15'
apa: 'Aminof, B., Jacobs, S., Khalimov, A., & Rubin, S. (2014). Parameterized
model checking of token-passing systems. In Verification, Model Checking, and
Abstract Interpretation (Vol. 8318, pp. 262–281). San Diego, CA, United States:
Springer Nature. https://doi.org/10.1007/978-3-642-54013-4_15'
chicago: Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized
Model Checking of Token-Passing Systems.” In Verification, Model Checking,
and Abstract Interpretation, 8318:262–81. Springer Nature, 2014. https://doi.org/10.1007/978-3-642-54013-4_15.
ieee: B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking
of token-passing systems,” in Verification, Model Checking, and Abstract Interpretation,
San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.
ista: 'Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking
of token-passing systems. Verification, Model Checking, and Abstract Interpretation.
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318,
262–281.'
mla: Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.”
Verification, Model Checking, and Abstract Interpretation, vol. 8318, Springer
Nature, 2014, pp. 262–81, doi:10.1007/978-3-642-54013-4_15.
short: B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking,
and Abstract Interpretation, Springer Nature, 2014, pp. 262–281.
conference:
end_date: 2014-01-21
location: San Diego, CA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2014-01-19
date_created: 2022-03-18T13:01:22Z
date_published: 2014-01-30T00:00:00Z
date_updated: 2022-05-17T08:36:01Z
day: '30'
department:
- _id: KrCh
doi: 10.1007/978-3-642-54013-4_15
ec_funded: 1
external_id:
arxiv:
- '1311.4425'
intvolume: ' 8318'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ' https://doi.org/10.48550/arXiv.1311.4425'
month: '01'
oa: 1
oa_version: Preprint
page: 262-281
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal 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: Verification, Model Checking, and Abstract Interpretation
publication_identifier:
eisbn:
- '9783642540134'
eissn:
- 1611-3349
isbn:
- '9783642540127'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Parameterized model checking of token-passing systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...
---
_id: '10885'
abstract:
- lang: eng
text: "Two-player games on graphs provide the theoretical framework for many important
problems such as reactive synthesis. While the traditional study of two-player
zero-sum games has been extended to multi-player games with several notions of
equilibria, they are decidable only for perfect-information games, whereas several
applications require imperfect-information games.\r\nIn this paper we propose
a new notion of equilibria, called doomsday equilibria, which is a strategy profile
such that all players satisfy their own objective, and if any coalition of players
deviates and violates even one of the players objective, then the objective of
every player is violated.\r\nWe present algorithms and complexity results for
deciding the existence of doomsday equilibria for various classes of ω-regular
objectives, both for imperfect-information games, and for perfect-information
games.We provide optimal complexity bounds for imperfect-information games, and
in most cases for perfect-information games."
acknowledgement: " Supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF
NFN Grant No\r\nS11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft
faculty fellows award."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Emmanuel
full_name: Filiot, Emmanuel
last_name: Filiot
- first_name: Jean-François
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: 'Chatterjee K, Doyen L, Filiot E, Raskin J-F. Doomsday equilibria for omega-regular
games. In: VMCAI 2014: Verification, Model Checking, and Abstract Interpretation.
Vol 8318. Springer Nature; 2014:78-97. doi:10.1007/978-3-642-54013-4_5'
apa: 'Chatterjee, K., Doyen, L., Filiot, E., & Raskin, J.-F. (2014). Doomsday
equilibria for omega-regular games. In VMCAI 2014: Verification, Model Checking,
and Abstract Interpretation (Vol. 8318, pp. 78–97). San Diego, CA, United
States: Springer Nature. https://doi.org/10.1007/978-3-642-54013-4_5'
chicago: 'Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean-François
Raskin. “Doomsday Equilibria for Omega-Regular Games.” In VMCAI 2014: Verification,
Model Checking, and Abstract Interpretation, 8318:78–97. Springer Nature,
2014. https://doi.org/10.1007/978-3-642-54013-4_5.'
ieee: 'K. Chatterjee, L. Doyen, E. Filiot, and J.-F. Raskin, “Doomsday equilibria
for omega-regular games,” in VMCAI 2014: Verification, Model Checking, and
Abstract Interpretation, San Diego, CA, United States, 2014, vol. 8318, pp.
78–97.'
ista: 'Chatterjee K, Doyen L, Filiot E, Raskin J-F. 2014. Doomsday equilibria for
omega-regular games. VMCAI 2014: Verification, Model Checking, and Abstract Interpretation.
VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318,
78–97.'
mla: 'Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.”
VMCAI 2014: Verification, Model Checking, and Abstract Interpretation,
vol. 8318, Springer Nature, 2014, pp. 78–97, doi:10.1007/978-3-642-54013-4_5.'
short: 'K. Chatterjee, L. Doyen, E. Filiot, J.-F. Raskin, in:, VMCAI 2014: Verification,
Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 78–97.'
conference:
end_date: 2014-01-21
location: San Diego, CA, United States
name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
start_date: 2014-01-19
date_created: 2022-03-18T13:03:15Z
date_published: 2014-01-30T00:00:00Z
date_updated: 2023-02-23T12:52:24Z
day: '30'
department:
- _id: KrCh
doi: 10.1007/978-3-642-54013-4_5
ec_funded: 1
external_id:
arxiv:
- '1311.3238'
intvolume: ' 8318'
language:
- iso: eng
month: '01'
oa_version: Preprint
page: 78-97
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal 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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 'VMCAI 2014: Verification, Model Checking, and Abstract Interpretation'
publication_identifier:
eisbn:
- '9783642540134'
eissn:
- 1611-3349
isbn:
- '9783642540127'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '681'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Doomsday equilibria for omega-regular games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...
---
_id: '10892'
abstract:
- lang: eng
text: "In this paper, we introduce planar matchings on directed pseudo-line arrangements,
which yield a planar set of pseudo-line segments such that only matching-partners
are adjacent. By translating the planar matching problem into a corresponding
stable roommates problem we show that such matchings always exist.\r\nUsing our
new framework, we establish, for the first time, a complete, rigorous definition
of weighted straight skeletons, which are based on a so-called wavefront propagation
process. We present a generalized and unified approach to treat structural changes
in the wavefront that focuses on the restoration of weak planarity by finding
planar matchings."
acknowledgement: 'T. Biedl was supported by NSERC and the Ross and Muriel Cheriton
Fellowship. P. Palfrader was supported by Austrian Science Fund (FWF): P25816-N15.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Therese
full_name: Biedl, Therese
last_name: Biedl
- first_name: Stefan
full_name: Huber, Stefan
id: 4700A070-F248-11E8-B48F-1D18A9856A87
last_name: Huber
orcid: 0000-0002-8871-5814
- first_name: Peter
full_name: Palfrader, Peter
last_name: Palfrader
citation:
ama: 'Biedl T, Huber S, Palfrader P. Planar matchings for weighted straight skeletons.
In: 25th International Symposium, ISAAC 2014. Vol 8889. Springer Nature;
2014:117-127. doi:10.1007/978-3-319-13075-0_10'
apa: 'Biedl, T., Huber, S., & Palfrader, P. (2014). Planar matchings for weighted
straight skeletons. In 25th International Symposium, ISAAC 2014 (Vol. 8889,
pp. 117–127). Jeonju, Korea: Springer Nature. https://doi.org/10.1007/978-3-319-13075-0_10'
chicago: Biedl, Therese, Stefan Huber, and Peter Palfrader. “Planar Matchings for
Weighted Straight Skeletons.” In 25th International Symposium, ISAAC 2014,
8889:117–27. Springer Nature, 2014. https://doi.org/10.1007/978-3-319-13075-0_10.
ieee: T. Biedl, S. Huber, and P. Palfrader, “Planar matchings for weighted straight
skeletons,” in 25th International Symposium, ISAAC 2014, Jeonju, Korea,
2014, vol. 8889, pp. 117–127.
ista: 'Biedl T, Huber S, Palfrader P. 2014. Planar matchings for weighted straight
skeletons. 25th International Symposium, ISAAC 2014. ISAAC: International Symposium
on Algorithms and Computation, LNCS, vol. 8889, 117–127.'
mla: Biedl, Therese, et al. “Planar Matchings for Weighted Straight Skeletons.”
25th International Symposium, ISAAC 2014, vol. 8889, Springer Nature, 2014,
pp. 117–27, doi:10.1007/978-3-319-13075-0_10.
short: T. Biedl, S. Huber, P. Palfrader, in:, 25th International Symposium, ISAAC
2014, Springer Nature, 2014, pp. 117–127.
conference:
end_date: 2014-12-17
location: Jeonju, Korea
name: 'ISAAC: International Symposium on Algorithms and Computation'
start_date: 2014-12-15
date_created: 2022-03-21T07:09:03Z
date_published: 2014-11-08T00:00:00Z
date_updated: 2023-02-23T12:20:55Z
day: '08'
department:
- _id: HeEd
doi: 10.1007/978-3-319-13075-0_10
intvolume: ' 8889'
language:
- iso: eng
month: '11'
oa_version: None
page: 117-127
publication: 25th International Symposium, ISAAC 2014
publication_identifier:
eisbn:
- '9783319130750'
eissn:
- 1611-3349
isbn:
- '9783319130743'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '481'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Planar matchings for weighted straight skeletons
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8889
year: '2014'
...
---
_id: '10894'
abstract:
- lang: eng
text: PHAT is a C++ library for the computation of persistent homology by matrix
reduction. We aim for a simple generic design that decouples algorithms from data
structures without sacrificing efficiency or user-friendliness. This makes PHAT
a versatile platform for experimenting with algorithmic ideas and comparing them
to state of the art implementations.
article_processing_charge: No
author:
- first_name: Ulrich
full_name: Bauer, Ulrich
id: 2ADD483A-F248-11E8-B48F-1D18A9856A87
last_name: Bauer
orcid: 0000-0002-9683-0724
- first_name: Michael
full_name: Kerber, Michael
last_name: Kerber
- first_name: Jan
full_name: Reininghaus, Jan
id: 4505473A-F248-11E8-B48F-1D18A9856A87
last_name: Reininghaus
- first_name: Hubert
full_name: Wagner, Hubert
last_name: Wagner
citation:
ama: 'Bauer U, Kerber M, Reininghaus J, Wagner H. PHAT – Persistent Homology Algorithms
Toolbox. In: ICMS 2014: International Congress on Mathematical Software.
Vol 8592. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2014:137-143.
doi:10.1007/978-3-662-44199-2_24'
apa: 'Bauer, U., Kerber, M., Reininghaus, J., & Wagner, H. (2014). PHAT – Persistent
Homology Algorithms Toolbox. In ICMS 2014: International Congress on Mathematical
Software (Vol. 8592, pp. 137–143). Berlin, Heidelberg: Springer Berlin Heidelberg.
https://doi.org/10.1007/978-3-662-44199-2_24'
chicago: 'Bauer, Ulrich, Michael Kerber, Jan Reininghaus, and Hubert Wagner. “PHAT
– Persistent Homology Algorithms Toolbox.” In ICMS 2014: International Congress
on Mathematical Software, 8592:137–43. LNCS. Berlin, Heidelberg: Springer
Berlin Heidelberg, 2014. https://doi.org/10.1007/978-3-662-44199-2_24.'
ieee: 'U. Bauer, M. Kerber, J. Reininghaus, and H. Wagner, “PHAT – Persistent Homology
Algorithms Toolbox,” in ICMS 2014: International Congress on Mathematical Software,
Seoul, South Korea, 2014, vol. 8592, pp. 137–143.'
ista: 'Bauer U, Kerber M, Reininghaus J, Wagner H. 2014. PHAT – Persistent Homology
Algorithms Toolbox. ICMS 2014: International Congress on Mathematical Software.
ICMS: International Congress on Mathematical SoftwareLNCS vol. 8592, 137–143.'
mla: 'Bauer, Ulrich, et al. “PHAT – Persistent Homology Algorithms Toolbox.” ICMS
2014: International Congress on Mathematical Software, vol. 8592, Springer
Berlin Heidelberg, 2014, pp. 137–43, doi:10.1007/978-3-662-44199-2_24.'
short: 'U. Bauer, M. Kerber, J. Reininghaus, H. Wagner, in:, ICMS 2014: International
Congress on Mathematical Software, Springer Berlin Heidelberg, Berlin, Heidelberg,
2014, pp. 137–143.'
conference:
end_date: 2014-08-09
location: Seoul, South Korea
name: 'ICMS: International Congress on Mathematical Software'
start_date: 2014-08-05
date_created: 2022-03-21T07:12:16Z
date_published: 2014-09-01T00:00:00Z
date_updated: 2023-09-20T09:42:40Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-662-44199-2_24
intvolume: ' 8592'
language:
- iso: eng
month: '09'
oa_version: None
page: 137-143
place: Berlin, Heidelberg
publication: 'ICMS 2014: International Congress on Mathematical Software'
publication_identifier:
eisbn:
- '9783662441992'
eissn:
- 1611-3349
isbn:
- '9783662441985'
issn:
- 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
quality_controlled: '1'
related_material:
record:
- id: '1433'
relation: later_version
status: public
scopus_import: '1'
series_title: LNCS
status: public
title: PHAT – Persistent Homology Algorithms Toolbox
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 8592
year: '2014'
...
---
_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: '10897'
abstract:
- lang: eng
text: Taking images is an efficient way to collect data about the physical world.
It can be done fast and in exquisite detail. By definition, image processing is
the field that concerns itself with the computation aimed at harnessing the information
contained in images [10]. This talk is concerned with topological information.
Our main thesis is that persistent homology [5] is a useful method to quantify
and summarize topological information, building a bridge that connects algebraic
topology with applications. We provide supporting evidence for this thesis by
touching upon four technical developments in the overlap between persistent homology
and image processing.
acknowledgement: This research is partially supported by the European Science Foundation
(ESF) under the Research Network Programme, the European Union under the Toposys
Project FP7-ICT-318493-STREP, the Russian Government under the Mega Project 11.G34.31.0053.
article_processing_charge: No
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
citation:
ama: 'Edelsbrunner H. Persistent homology in image processing. In: Graph-Based
Representations in Pattern Recognition. Vol 7877. LNCS. Berlin, Heidelberg:
Springer Nature; 2013:182-183. doi:10.1007/978-3-642-38221-5_19'
apa: 'Edelsbrunner, H. (2013). Persistent homology in image processing. In Graph-Based
Representations in Pattern Recognition (Vol. 7877, pp. 182–183). Berlin, Heidelberg:
Springer Nature. https://doi.org/10.1007/978-3-642-38221-5_19'
chicago: 'Edelsbrunner, Herbert. “Persistent Homology in Image Processing.” In Graph-Based
Representations in Pattern Recognition, 7877:182–83. LNCS. Berlin, Heidelberg:
Springer Nature, 2013. https://doi.org/10.1007/978-3-642-38221-5_19.'
ieee: H. Edelsbrunner, “Persistent homology in image processing,” in Graph-Based
Representations in Pattern Recognition, Vienna, Austria, 2013, vol. 7877,
pp. 182–183.
ista: 'Edelsbrunner H. 2013. Persistent homology in image processing. Graph-Based
Representations in Pattern Recognition. GbRPR: Graph-based Representations in
Pattern RecognitionLNCS vol. 7877, 182–183.'
mla: Edelsbrunner, Herbert. “Persistent Homology in Image Processing.” Graph-Based
Representations in Pattern Recognition, vol. 7877, Springer Nature, 2013,
pp. 182–83, doi:10.1007/978-3-642-38221-5_19.
short: H. Edelsbrunner, in:, Graph-Based Representations in Pattern Recognition,
Springer Nature, Berlin, Heidelberg, 2013, pp. 182–183.
conference:
end_date: 2013-05-17
location: Vienna, Austria
name: 'GbRPR: Graph-based Representations in Pattern Recognition'
start_date: 2013-05-15
date_created: 2022-03-21T07:30:33Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2023-09-05T15:10:20Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-642-38221-5_19
ec_funded: 1
intvolume: ' 7877'
language:
- iso: eng
month: '06'
oa_version: None
page: 182-183
place: Berlin, Heidelberg
project:
- _id: 255D761E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '318493'
name: Topological Complex Systems
publication: Graph-Based Representations in Pattern Recognition
publication_identifier:
eisbn:
- '9783642382215'
eissn:
- 1611-3349
isbn:
- '9783642382208'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Persistent homology in image processing
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7877
year: '2013'
...
---
_id: '10902'
abstract:
- lang: eng
text: We consider how to edit strings from a source language so that the edited
strings belong to a target language, where the languages are given as deterministic
finite automata. Non-streaming (or offline) transducers perform edits given the
whole source string. We show that the class of deterministic one-pass transducers
with registers along with increment and min operation suffices for computing optimal
edit distance, whereas the same class of transducers without the min operation
is not sufficient. Streaming (or online) transducers perform edits as the letters
of the source string are received. We present a polynomial time algorithm for
the partial-repair problem that given a bound α asks for the construction of a
deterministic streaming transducer (if one exists) that ensures that the ‘maximum
fraction’ η of the strings of the source language are edited, within cost α, to
the target language.
acknowledgement: 'The research was supported by Austrian Science Fund (FWF) Grant
No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph
Games), and Microsoft faculty fellows award. Thanks to Gabriele Puppis for suggesting
the problem of identifying a deterministic transducer to compute the optimal cost,
and to Martin Chmelik for his comments on the introduction.'
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: Siddhesh
full_name: Chaubal, Siddhesh
last_name: Chaubal
- first_name: Sasha
full_name: Rubin, Sasha
id: 2EC51194-F248-11E8-B48F-1D18A9856A87
last_name: Rubin
citation:
ama: 'Chatterjee K, Chaubal S, Rubin S. How to travel between languages. In: 7th
International Conference on Language and Automata Theory and Applications.
Vol 7810. LNCS. Berlin, Heidelberg: Springer Nature; 2013:214-225. doi:10.1007/978-3-642-37064-9_20'
apa: 'Chatterjee, K., Chaubal, S., & Rubin, S. (2013). How to travel between
languages. In 7th International Conference on Language and Automata Theory
and Applications (Vol. 7810, pp. 214–225). Berlin, Heidelberg: Springer Nature.
https://doi.org/10.1007/978-3-642-37064-9_20'
chicago: 'Chatterjee, Krishnendu, Siddhesh Chaubal, and Sasha Rubin. “How to Travel
between Languages.” In 7th International Conference on Language and Automata
Theory and Applications, 7810:214–25. LNCS. Berlin, Heidelberg: Springer Nature,
2013. https://doi.org/10.1007/978-3-642-37064-9_20.'
ieee: K. Chatterjee, S. Chaubal, and S. Rubin, “How to travel between languages,”
in 7th International Conference on Language and Automata Theory and Applications,
Bilbao, Spain, 2013, vol. 7810, pp. 214–225.
ista: 'Chatterjee K, Chaubal S, Rubin S. 2013. How to travel between languages.
7th International Conference on Language and Automata Theory and Applications.
LATA: Conference on Language and Automata Theory and ApplicationsLNCS, LNCS, vol.
7810, 214–225.'
mla: Chatterjee, Krishnendu, et al. “How to Travel between Languages.” 7th International
Conference on Language and Automata Theory and Applications, vol. 7810, Springer
Nature, 2013, pp. 214–25, doi:10.1007/978-3-642-37064-9_20.
short: K. Chatterjee, S. Chaubal, S. Rubin, in:, 7th International Conference on
Language and Automata Theory and Applications, Springer Nature, Berlin, Heidelberg,
2013, pp. 214–225.
conference:
end_date: 2013-04-05
location: Bilbao, Spain
name: 'LATA: Conference on Language and Automata Theory and Applications'
start_date: 2013-04-02
date_created: 2022-03-21T07:56:21Z
date_published: 2013-04-15T00:00:00Z
date_updated: 2023-09-05T15:10:38Z
day: '15'
department:
- _id: KrCh
doi: 10.1007/978-3-642-37064-9_20
ec_funded: 1
intvolume: ' 7810'
language:
- iso: eng
month: '04'
oa_version: None
page: 214-225
place: Berlin, Heidelberg
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal 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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 7th International Conference on Language and Automata Theory and Applications
publication_identifier:
eisbn:
- '9783642370649'
eissn:
- 1611-3349
isbn:
- '9783642370632'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: How to travel between languages
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7810
year: '2013'
...
---
_id: '5745'
article_processing_charge: No
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
last_name: Gupta
citation:
ama: 'Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In:
Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin,
Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:10.1007/978-3-642-33386-6_10'
apa: 'Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction.
In Automated Technology for Verification and Analysis (Vol. 7561, pp. 107–121).
Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_10'
chicago: 'Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof
Reduction.” In Automated Technology for Verification and Analysis, 7561:107–21.
LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. https://doi.org/10.1007/978-3-642-33386-6_10.'
ieee: 'A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,”
in Automated Technology for Verification and Analysis, vol. 7561, Berlin,
Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.'
ista: 'Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction.
In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.'
mla: Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.”
Automated Technology for Verification and Analysis, vol. 7561, Springer
Berlin Heidelberg, 2012, pp. 107–21, doi:10.1007/978-3-642-33386-6_10.
short: A. Gupta, in:, Automated Technology for Verification and Analysis, Springer
Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121.
conference:
end_date: 2012-10-06
location: Thiruvananthapuram, Kerala, India
name: ATVA 2012
start_date: 2012-10-03
date_created: 2018-12-18T13:01:46Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2023-09-05T14:15:29Z
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_10
ec_funded: 1
file:
- access_level: open_access
checksum: 68415837a315de3cc4d120f6019d752c
content_type: application/pdf
creator: dernst
date_created: 2018-12-18T13:07:35Z
date_updated: 2020-07-14T12:47:10Z
file_id: '5746'
file_name: 2012_ATVA_Gupta.pdf
file_size: 465502
relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: ' 7561'
language:
- iso: eng
oa: 1
oa_version: None
page: 107-121
place: Berlin, Heidelberg
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Automated Technology for Verification and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783642333859'
- '9783642333866'
issn:
- 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
pubrep_id: '180'
quality_controlled: '1'
series_title: LNCS
status: public
title: Improved Single Pass Algorithms for Resolution Proof Reduction
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '10903'
abstract:
- lang: eng
text: We propose a logic-based framework for automated reasoning about sequential
programs manipulating singly-linked lists and arrays with unbounded data. We introduce
the logic SLAD, which allows combining shape constraints, written in a fragment
of Separation Logic, with data and size constraints. We address the problem of
checking the entailment between SLAD formulas, which is crucial in performing
pre-post condition reasoning. Although this problem is undecidable in general
for SLAD, we propose a sound and powerful procedure that is able to solve this
problem for a large class of formulas, beyond the capabilities of existing techniques
and tools. We prove that this procedure is complete, i.e., it is actually a decision
procedure for this problem, for an important fragment of SLAD including known
decidable logics. We implemented this procedure and shown its preciseness and
its efficiency on a significant benchmark of formulas.
acknowledgement: This work has been partially supported by the French ANR project
Veridyc
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ahmed
full_name: Bouajjani, Ahmed
last_name: Bouajjani
- 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: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for
programs manipulating lists and arrays with infinite data. In: Automated Technology
for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer;
2012:167-182. doi:10.1007/978-3-642-33386-6_14'
apa: 'Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate
invariant checking for programs manipulating lists and arrays with infinite data.
In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182).
Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14'
chicago: 'Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
“Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite
Data.” In Automated Technology for Verification and Analysis, 7561:167–82.
LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.'
ieee: A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking
for programs manipulating lists and arrays with infinite data,” in Automated
Technology for Verification and Analysis, Thiruvananthapuram, India, 2012,
vol. 7561, pp. 167–182.
ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking
for programs manipulating lists and arrays with infinite data. Automated Technology
for Verification and Analysis. ATVA: Automated Technology for Verification and
AnalysisLNCS, LNCS, vol. 7561, 167–182.'
mla: Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating
Lists and Arrays with Infinite Data.” Automated Technology for Verification
and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14.
short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology
for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.
conference:
end_date: 2012-10-06
location: Thiruvananthapuram, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2012-10-03
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2023-09-05T14:07:24Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_14
intvolume: ' 7561'
language:
- iso: eng
month: '10'
oa_version: None
page: 167-182
place: Berlin, Heidelberg
publication: Automated Technology for Verification and Analysis
publication_identifier:
eisbn:
- '9783642333866'
eissn:
- 1611-3349
isbn:
- '9783642333859'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Accurate invariant checking for programs manipulating lists and arrays with
infinite data
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '10905'
abstract:
- lang: eng
text: "Energy games belong to a class of turn-based two-player infinite-duration
games played on a weighted directed graph. It is one of the rare and intriguing
combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While
the existence of polynomial-time algorithms has been a major open problem for
decades, there is no algorithm that solves any non-trivial subclass in polynomial
time.\r\nIn this paper, we give several results based on the weight structures
of the graph. First, we identify a notion of penalty and present a polynomial-time
algorithm when the penalty is large. Our algorithm is the first polynomial-time
algorithm on a large class of weighted graphs. It includes several counter examples
that show that many previous algorithms, such as value iteration and random facet
algorithms, require at least sub-exponential time. Our main technique is developing
the first non-trivial approximation algorithm and showing how to convert it to
an exact algorithm. Moreover, we show that in a practical case in verification
where weights are clustered around a constant number of values, the energy game
problem can be solved in polynomial time. We also show that the problem is still
as hard as in general when the clique-width is bounded or the graph is strongly
ergodic, suggesting that restricting graph structures need not help."
acknowledgement: 'Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian
Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games),
and a Microsoft Faculty Fellows Award'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Sebastian
full_name: Krinninger, Sebastian
last_name: Krinninger
- first_name: Danupon
full_name: Nanongkai, Danupon
last_name: Nanongkai
citation:
ama: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms
for energy games with special weight structures. In: Algorithms – ESA 2012.
Vol 7501. Springer; 2012:301-312. doi:10.1007/978-3-642-33090-2_27'
apa: 'Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2012).
Polynomial-time algorithms for energy games with special weight structures. In
Algorithms – ESA 2012 (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer.
https://doi.org/10.1007/978-3-642-33090-2_27'
chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon
Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.”
In Algorithms – ESA 2012, 7501:301–12. Springer, 2012. https://doi.org/10.1007/978-3-642-33090-2_27.
ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time
algorithms for energy games with special weight structures,” in Algorithms
– ESA 2012, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.
ista: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time
algorithms for energy games with special weight structures. Algorithms – ESA 2012.
ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.'
mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games
with Special Weight Structures.” Algorithms – ESA 2012, vol. 7501, Springer,
2012, pp. 301–12, doi:10.1007/978-3-642-33090-2_27.
short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms
– ESA 2012, Springer, 2012, pp. 301–312.
conference:
end_date: 2012-09-12
location: Ljubljana, Slovenia
name: 'ESA: European Symposium on Algorithms'
start_date: 2012-09-10
date_created: 2022-03-21T08:01:45Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2023-09-05T14:09:30Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-33090-2_27
ec_funded: 1
external_id:
arxiv:
- '1604.08234'
intvolume: ' 7501'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.08234
month: '10'
oa: 1
oa_version: Preprint
page: 301-312
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'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Algorithms – ESA 2012
publication_identifier:
eisbn:
- '9783642330902'
eissn:
- 1611-3349
isbn:
- '9783642330896'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
record:
- id: '535'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Polynomial-time algorithms for energy games with special weight structures
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7501
year: '2012'
...
---
_id: '10906'
abstract:
- lang: eng
text: HSF(C) is a tool that automates verification of safety and liveness properties
for C programs. This paper describes the verification approach taken by HSF(C)
and provides instructions on how to install and use the tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergey
full_name: Grebenshchikov, Sergey
last_name: Grebenshchikov
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Nuno P.
full_name: Lopes, Nuno P.
last_name: Lopes
- first_name: Corneliu
full_name: Popeea, Corneliu
last_name: Popeea
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
citation:
ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software
verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms
for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg:
Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46'
apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko,
A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &
B. König (Eds.), Tools and Algorithms for the Construction and Analysis of
Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46'
chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea,
and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In
Tools and Algorithms for the Construction and Analysis of Systems, edited
by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer,
2012. https://doi.org/10.1007/978-3-642-28756-5_46.'
ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko,
“HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms
for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol.
7214, pp. 549–551.'
ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C):
A software verifier based on Horn clauses. Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.'
mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn
Clauses.” Tools and Algorithms for the Construction and Analysis of Systems,
edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51,
doi:10.1007/978-3-642-28756-5_46.'
short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:,
C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis
of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.
conference:
end_date: 2012-04-01
location: Tallinn, Estonia
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2012-03-24
date_created: 2022-03-21T08:03:30Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2023-09-05T14:09:54Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-28756-5_46
editor:
- first_name: Cormac
full_name: Flanagan, Cormac
last_name: Flanagan
- first_name: Barbara
full_name: König, Barbara
last_name: König
intvolume: ' 7214'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/978-3-642-28756-5_46
month: '04'
oa: 1
oa_version: Published Version
page: 549-551
place: Berlin, Heidelberg
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783642287565'
eissn:
- 1611-3349
isbn:
- '9783642287558'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'HSF(C): A software verifier based on Horn clauses'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7214
year: '2012'
...
---
_id: '10907'
abstract:
- lang: eng
text: This paper presents a method to create a model of an articulated object using
the planar motion in an initialization video. The model consists of rigid parts
connected by points of articulation. The rigid parts are described by the positions
of salient feature-points tracked throughout the video. Following a filtering
step that identifies points that belong to different objects, rigid parts are
found by a grouping process in a graph pyramid. Valid articulation points are
selected by verifying multiple hypotheses for each pair of parts.
acknowledgement: This work has been partially supported by the Austrian Science Fund
under grants S9103-N13 and P18716-N13.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Nicole M.
full_name: Artner, Nicole M.
last_name: Artner
- first_name: Adrian
full_name: Ion, Adrian
id: 29F89302-F248-11E8-B48F-1D18A9856A87
last_name: Ion
- first_name: Walter G.
full_name: Kropatsch, Walter G.
last_name: Kropatsch
citation:
ama: 'Artner NM, Ion A, Kropatsch WG. Spatio-temporal extraction of articulated
models in a graph pyramid. In: Jiang X, Ferrer M, Torsello A, eds. Graph-Based
Representations in Pattern Recognition. Vol 6658. LNIP. Berlin, Heidelberg:
Springer; 2011:215-224. doi:10.1007/978-3-642-20844-7_22'
apa: 'Artner, N. M., Ion, A., & Kropatsch, W. G. (2011). Spatio-temporal extraction
of articulated models in a graph pyramid. In X. Jiang, M. Ferrer, & A. Torsello
(Eds.), Graph-Based Representations in Pattern Recognition (Vol. 6658,
pp. 215–224). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-20844-7_22'
chicago: 'Artner, Nicole M., Adrian Ion, and Walter G. Kropatsch. “Spatio-Temporal
Extraction of Articulated Models in a Graph Pyramid.” In Graph-Based Representations
in Pattern Recognition, edited by Xiaoyi Jiang, Miquel Ferrer, and Andrea
Torsello, 6658:215–24. LNIP. Berlin, Heidelberg: Springer, 2011. https://doi.org/10.1007/978-3-642-20844-7_22.'
ieee: N. M. Artner, A. Ion, and W. G. Kropatsch, “Spatio-temporal extraction of
articulated models in a graph pyramid,” in Graph-Based Representations in Pattern
Recognition, Münster, Germany, 2011, vol. 6658, pp. 215–224.
ista: 'Artner NM, Ion A, Kropatsch WG. 2011. Spatio-temporal extraction of articulated
models in a graph pyramid. Graph-Based Representations in Pattern Recognition.
GbRPR: Graph-based Representations in Pattern RecognitionLNIP, LNCS, vol. 6658,
215–224.'
mla: Artner, Nicole M., et al. “Spatio-Temporal Extraction of Articulated Models
in a Graph Pyramid.” Graph-Based Representations in Pattern Recognition,
edited by Xiaoyi Jiang et al., vol. 6658, Springer, 2011, pp. 215–24, doi:10.1007/978-3-642-20844-7_22.
short: N.M. Artner, A. Ion, W.G. Kropatsch, in:, X. Jiang, M. Ferrer, A. Torsello
(Eds.), Graph-Based Representations in Pattern Recognition, Springer, Berlin,
Heidelberg, 2011, pp. 215–224.
conference:
end_date: 2011-05-20
location: Münster, Germany
name: 'GbRPR: Graph-based Representations in Pattern Recognition'
start_date: 2011-05-18
date_created: 2022-03-21T08:08:35Z
date_published: 2011-06-01T00:00:00Z
date_updated: 2023-09-05T14:10:15Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-642-20844-7_22
editor:
- first_name: Xiaoyi
full_name: Jiang, Xiaoyi
last_name: Jiang
- first_name: Miquel
full_name: Ferrer, Miquel
last_name: Ferrer
- first_name: Andrea
full_name: Torsello, Andrea
last_name: Torsello
intvolume: ' 6658'
language:
- iso: eng
month: '06'
oa_version: None
page: 215-224
place: Berlin, Heidelberg
publication: Graph-Based Representations in Pattern Recognition
publication_identifier:
eisbn:
- '9783642208447'
eissn:
- 1611-3349
isbn:
- '9783642208430'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNIP
status: public
title: Spatio-temporal extraction of articulated models in a graph pyramid
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 6658
year: '2011'
...
---
_id: '10908'
abstract:
- lang: eng
text: We present ABC, a software tool for automatically computing symbolic upper
bounds on the number of iterations of nested program loops. The system combines
static analysis of programs with symbolic summation techniques to derive loop
invariant relations between program variables. Iteration bounds are obtained from
the inferred invariants, by replacing variables with bounds on their greatest
values. We have successfully applied ABC to a large number of examples. The derived
symbolic bounds express non-trivial polynomial relations over loop variables.
We also report on results to automatically infer symbolic expressions over harmonic
numbers as upper bounds on loop iteration counts.
acknowledgement: This work was supported in part by the Swiss NSF. The fourth author
is supported by an FWF Hertha Firnberg Research grant (T425-N23).
article_processing_charge: No
author:
- first_name: Régis
full_name: Blanc, Régis
last_name: Blanc
- 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: Thibaud
full_name: Hottelier, Thibaud
last_name: Hottelier
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
citation:
ama: 'Blanc R, Henzinger TA, Hottelier T, Kovács L. ABC: Algebraic Bound Computation
for loops. In: Clarke EM, Voronkov A, eds. Logic for Programming, Artificial
Intelligence, and Reasoning. Vol 6355. LNCS. Berlin, Heidelberg: Springer
Nature; 2010:103-118. doi:10.1007/978-3-642-17511-4_7'
apa: 'Blanc, R., Henzinger, T. A., Hottelier, T., & Kovács, L. (2010). ABC:
Algebraic Bound Computation for loops. In E. M. Clarke & A. Voronkov (Eds.),
Logic for Programming, Artificial Intelligence, and Reasoning (Vol. 6355,
pp. 103–118). Berlin, Heidelberg: Springer Nature. https://doi.org/10.1007/978-3-642-17511-4_7'
chicago: 'Blanc, Régis, Thomas A Henzinger, Thibaud Hottelier, and Laura Kovács.
“ABC: Algebraic Bound Computation for Loops.” In Logic for Programming, Artificial
Intelligence, and Reasoning, edited by Edmund M Clarke and Andrei Voronkov,
6355:103–18. LNCS. Berlin, Heidelberg: Springer Nature, 2010. https://doi.org/10.1007/978-3-642-17511-4_7.'
ieee: 'R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, “ABC: Algebraic Bound
Computation for loops,” in Logic for Programming, Artificial Intelligence,
and Reasoning, Dakar, Senegal, 2010, vol. 6355, pp. 103–118.'
ista: 'Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound
Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning.
LPAR: Conference on Logic for Programming, Artificial Intelligence and ReasoningLNCS
vol. 6355, 103–118.'
mla: 'Blanc, Régis, et al. “ABC: Algebraic Bound Computation for Loops.” Logic
for Programming, Artificial Intelligence, and Reasoning, edited by Edmund
M Clarke and Andrei Voronkov, vol. 6355, Springer Nature, 2010, pp. 103–18, doi:10.1007/978-3-642-17511-4_7.'
short: R. Blanc, T.A. Henzinger, T. Hottelier, L. Kovács, in:, E.M. Clarke, A. Voronkov
(Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer
Nature, Berlin, Heidelberg, 2010, pp. 103–118.
conference:
end_date: 2010-05-01
location: Dakar, Senegal
name: 'LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning'
start_date: 2010-04-25
date_created: 2022-03-21T08:14:35Z
date_published: 2010-05-01T00:00:00Z
date_updated: 2022-06-13T07:44:21Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-17511-4_7
editor:
- first_name: Edmund M
full_name: Clarke, Edmund M
last_name: Clarke
- first_name: Andrei
full_name: Voronkov, Andrei
last_name: Voronkov
intvolume: ' 6355'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://infoscience.epfl.ch/record/186096
month: '05'
oa: 1
oa_version: Submitted Version
page: 103-118
place: Berlin, Heidelberg
publication: Logic for Programming, Artificial Intelligence, and Reasoning
publication_identifier:
eisbn:
- '9783642175114'
eissn:
- 1611-3349
isbn:
- '9783642175107'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'ABC: Algebraic Bound Computation for loops'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6355
year: '2010'
...
---
_id: '11800'
abstract:
- lang: eng
text: "Web search engines have emerged as one of the central applications on the
Internet. In fact, search has become one of the most important activities that
people engage in on the the Internet. Even beyond becoming the number one source
of information, a growing number of businesses are depending on web search engines
for customer acquisition.\r\n\r\nThe first generation of web search engines used
text-only retrieval techniques. Google revolutionized the field by deploying the
PageRank technology – an eigenvector-based analysis of the hyperlink structure
– to analyze the web in order to produce relevant results. Moving forward, our
goal is to achieve a better understanding of a page with a view towards producing
even more relevant results."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: 'Henzinger MH. The past, present, and future of web search engines. In: 31st
International Colloquium on Automata, Languages and Programming. Vol 3142.
Springer Nature; 2004:3. doi:10.1007/978-3-540-27836-8_2'
apa: 'Henzinger, M. H. (2004). The past, present, and future of web search engines.
In 31st International Colloquium on Automata, Languages and Programming
(Vol. 3142, p. 3). Turku, Finland: Springer Nature. https://doi.org/10.1007/978-3-540-27836-8_2'
chicago: Henzinger, Monika H. “The Past, Present, and Future of Web Search Engines.”
In 31st International Colloquium on Automata, Languages and Programming,
3142:3. Springer Nature, 2004. https://doi.org/10.1007/978-3-540-27836-8_2.
ieee: M. H. Henzinger, “The past, present, and future of web search engines,” in
31st International Colloquium on Automata, Languages and Programming, Turku,
Finland, 2004, vol. 3142, p. 3.
ista: 'Henzinger MH. 2004. The past, present, and future of web search engines.
31st International Colloquium on Automata, Languages and Programming. ICALP: International
Colloquium on Automata, Languages, and Programming, LNCS, vol. 3142, 3.'
mla: Henzinger, Monika H. “The Past, Present, and Future of Web Search Engines.”
31st International Colloquium on Automata, Languages and Programming, vol.
3142, Springer Nature, 2004, p. 3, doi:10.1007/978-3-540-27836-8_2.
short: M.H. Henzinger, in:, 31st International Colloquium on Automata, Languages
and Programming, Springer Nature, 2004, p. 3.
conference:
end_date: 2004-07-16
location: Turku, Finland
name: 'ICALP: International Colloquium on Automata, Languages, and Programming'
start_date: 2004-07-12
date_created: 2022-08-11T12:38:58Z
date_published: 2004-07-01T00:00:00Z
date_updated: 2023-02-13T11:45:25Z
day: '01'
doi: 10.1007/978-3-540-27836-8_2
extern: '1'
intvolume: ' 3142'
language:
- iso: eng
month: '07'
oa_version: None
page: '3'
publication: 31st International Colloquium on Automata, Languages and Programming
publication_identifier:
eissn:
- 1611-3349
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: The past, present, and future of web search engines
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 3142
year: '2004'
...
---
_id: '11801'
abstract:
- lang: eng
text: "Web search engines have emerged as one of the central applications on the
internet. In fact, search has become one of the most important activities that
people engage in on the Internet. Even beyond becoming the number one source of
information, a growing number of businesses are depending on web search engines
for customer acquisition. In this talk I will brief review the history of web
search engines: The first generation of web search engines used text-only retrieval
techniques. Google revolutionized the field by deploying the PageRank technology
– an eigenvector-based analysis of the hyperlink structure- to analyze the web
in order to produce relevant results. Moving forward, our goal is to achieve a
better understanding of a page with a view towards producing even more relevant
results.\r\n\r\nGoogle is powered by a large number of PCs. Using this infrastructure
and striving to be as efficient as possible poses challenging systems problems
but also various algorithmic challenges. I will discuss some of them in my talk."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: 'Henzinger MH. Algorithmic aspects of web search engines. In: 2th Annual
European Symposium on Algorithms. Vol 3221. Springer Nature; 2004:3. doi:10.1007/978-3-540-30140-0_2'
apa: 'Henzinger, M. H. (2004). Algorithmic aspects of web search engines. In 2th
Annual European Symposium on Algorithms (Vol. 3221, p. 3). Bergen, Norway:
Springer Nature. https://doi.org/10.1007/978-3-540-30140-0_2'
chicago: Henzinger, Monika H. “Algorithmic Aspects of Web Search Engines.” In 2th
Annual European Symposium on Algorithms, 3221:3. Springer Nature, 2004. https://doi.org/10.1007/978-3-540-30140-0_2.
ieee: M. H. Henzinger, “Algorithmic aspects of web search engines,” in 2th Annual
European Symposium on Algorithms, Bergen, Norway, 2004, vol. 3221, p. 3.
ista: 'Henzinger MH. 2004. Algorithmic aspects of web search engines. 2th Annual
European Symposium on Algorithms. ESA: European Symposium on Algorithms, LNCS,
vol. 3221, 3.'
mla: Henzinger, Monika H. “Algorithmic Aspects of Web Search Engines.” 2th Annual
European Symposium on Algorithms, vol. 3221, Springer Nature, 2004, p. 3,
doi:10.1007/978-3-540-30140-0_2.
short: M.H. Henzinger, in:, 2th Annual European Symposium on Algorithms, Springer
Nature, 2004, p. 3.
conference:
end_date: 2004-09-17
location: Bergen, Norway
name: 'ESA: European Symposium on Algorithms'
start_date: 2004-09-14
date_created: 2022-08-11T13:18:05Z
date_published: 2004-09-01T00:00:00Z
date_updated: 2023-02-13T11:47:26Z
day: '01'
doi: 10.1007/978-3-540-30140-0_2
extern: '1'
intvolume: ' 3221'
language:
- iso: eng
month: '09'
oa_version: None
page: '3'
publication: 2th Annual European Symposium on Algorithms
publication_identifier:
eissn:
- 1611-3349
isbn:
- ' 3540230254'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Algorithmic aspects of web search engines
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 3221
year: '2004'
...