---
_id: '5386'
abstract:
- lang: eng
text: 'We introduce TopoCut: a new way to integrate knowledge about topological
properties (TPs) into random field image segmentation model. Instead of including
TPs as additional constraints during minimization of the energy function, we devise
an efficient algorithm for modifying the unary potentials such that the resulting
segmentation is guaranteed with the desired properties. Our method is more flexible
in the sense that it handles more topology constraints than previous methods,
which were only able to enforce pairwise or global connectivity. In particular,
our method is very fast, making it for the first time possible to enforce global
topological properties in practical image segmentation tasks.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Chao
full_name: Chen, Chao
id: 3E92416E-F248-11E8-B48F-1D18A9856A87
last_name: Chen
- first_name: Daniel
full_name: Freedman, Daniel
last_name: Freedman
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: Chen C, Freedman D, Lampert C. Enforcing Topological Constraints in Random
Field Image Segmentation. IST Austria; 2011. doi:10.15479/AT:IST-2011-0002
apa: Chen, C., Freedman, D., & Lampert, C. (2011). Enforcing topological
constraints in random field image segmentation. IST Austria. https://doi.org/10.15479/AT:IST-2011-0002
chicago: Chen, Chao, Daniel Freedman, and Christoph Lampert. Enforcing Topological
Constraints in Random Field Image Segmentation. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0002.
ieee: C. Chen, D. Freedman, and C. Lampert, Enforcing topological constraints
in random field image segmentation. IST Austria, 2011.
ista: Chen C, Freedman D, Lampert C. 2011. Enforcing topological constraints in
random field image segmentation, IST Austria, 69p.
mla: Chen, Chao, et al. Enforcing Topological Constraints in Random Field Image
Segmentation. IST Austria, 2011, doi:10.15479/AT:IST-2011-0002.
short: C. Chen, D. Freedman, C. Lampert, Enforcing Topological Constraints in Random
Field Image Segmentation, IST Austria, 2011.
date_created: 2018-12-12T11:39:02Z
date_published: 2011-03-28T00:00:00Z
date_updated: 2023-02-23T11:22:48Z
day: '28'
ddc:
- '000'
department:
- _id: ChLa
doi: 10.15479/AT:IST-2011-0002
file:
- access_level: open_access
checksum: ad64c2add5fe2ad10e9d5c669f3f9526
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:34Z
date_updated: 2020-07-14T12:46:41Z
file_id: '5495'
file_name: IST-2011-0002_IST-2011-0002.pdf
file_size: 26390601
relation: main_file
file_date_updated: 2020-07-14T12:46:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '69'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '22'
related_material:
record:
- id: '3336'
relation: later_version
status: public
status: public
title: Enforcing topological constraints in random field image segmentation
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5383'
abstract:
- lang: eng
text: We present a new decidable logic called TREX for expressing constraints about
imperative tree data structures. In particular, TREX supports a transitive closure
operator that can express reachability constraints, which often appear in data
structure invariants. We show that our logic is closed under weakest precondition
computation, which enables its use for automated software verification. We further
show that satisfiability of formulas in TREX is decidable in NP. The low complexity
makes it an attractive alternative to more expensive logics such as monadic second-order
logic (MSOL) over trees, which have been traditionally used for reasoning about
tree data structures.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Marco
full_name: Muñiz, Marco
last_name: Muñiz
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: Wies T, Muñiz M, Kuncak V. On an Efficient Decision Procedure for Imperative
Tree Data Structures. IST Austria; 2011. doi:10.15479/AT:IST-2011-0005
apa: Wies, T., Muñiz, M., & Kuncak, V. (2011). On an efficient decision procedure
for imperative tree data structures. IST Austria. https://doi.org/10.15479/AT:IST-2011-0005
chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. On an Efficient Decision
Procedure for Imperative Tree Data Structures. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0005.
ieee: T. Wies, M. Muñiz, and V. Kuncak, On an efficient decision procedure for
imperative tree data structures. IST Austria, 2011.
ista: Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative
tree data structures, IST Austria, 25p.
mla: Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree
Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005.
short: T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative
Tree Data Structures, IST Austria, 2011.
date_created: 2018-12-12T11:39:01Z
date_published: 2011-04-26T00:00:00Z
date_updated: 2023-02-23T11:22:16Z
day: '26'
ddc:
- '000'
- '006'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2011-0005
file:
- access_level: open_access
checksum: b20029184c4a819c5f4466a4a3d238b5
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:01Z
date_updated: 2020-07-14T12:46:40Z
file_id: '5462'
file_name: IST-2011-0005_IST-2011-0005.pdf
file_size: 619053
relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '19'
related_material:
record:
- id: '3323'
relation: later_version
status: public
status: public
title: On an efficient decision procedure for imperative tree data structures
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5384'
abstract:
- lang: eng
text: 'We consider probabilistic automata on infinite words with acceptance defined
by parity conditions. We consider three qualitative decision problems: (i) the
positive decision problem asks whether there is a word that is accepted with positive
probability; (ii) the almost decision problem asks whether there is a word that
is accepted with probability 1; and (iii) the limit decision problem asks whether
for every ε > 0 there is a word that is accepted with probability at least 1 −
ε. We unify and generalize several decidability results for probabilistic automata
over infinite words, and identify a robust (closed under union and intersection)
subclass of probabilistic automata for which all the qualitative decision problems
are decidable for parity conditions. We also show that if the input words are
restricted to lasso shape words, then the positive and almost problems are decidable
for all probabilistic automata with parity conditions.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Mathieu
full_name: Tracol, Mathieu
id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
last_name: Tracol
citation:
ama: Chatterjee K, Tracol M. Decidable Problems for Probabilistic Automata on
Infinite Words. IST Austria; 2011. doi:10.15479/AT:IST-2011-0004
apa: Chatterjee, K., & Tracol, M. (2011). Decidable problems for probabilistic
automata on infinite words. IST Austria. https://doi.org/10.15479/AT:IST-2011-0004
chicago: Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic
Automata on Infinite Words. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0004.
ieee: K. Chatterjee and M. Tracol, Decidable problems for probabilistic automata
on infinite words. IST Austria, 2011.
ista: Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata
on infinite words, IST Austria, 30p.
mla: Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic
Automata on Infinite Words. IST Austria, 2011, doi:10.15479/AT:IST-2011-0004.
short: K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on
Infinite Words, IST Austria, 2011.
date_created: 2018-12-12T11:39:01Z
date_published: 2011-04-11T00:00:00Z
date_updated: 2023-02-23T11:05:53Z
day: '11'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0004
file:
- access_level: open_access
checksum: f5a0f664fadc335990f5fcf138df19f1
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:23Z
date_updated: 2020-07-14T12:46:40Z
file_id: '5545'
file_name: IST-2011-004_IST-2011-0004.pdf
file_size: 570827
relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '30'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '20'
related_material:
record:
- id: '2957'
relation: later_version
status: public
status: public
title: Decidable problems for probabilistic automata on infinite words
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3336'
abstract:
- lang: eng
text: 'We introduce TopoCut: a new way to integrate knowledge about topological
properties (TPs) into random field image segmentation model. Instead of including
TPs as additional constraints during minimization of the energy function, we devise
an efficient algorithm for modifying the unary potentials such that the resulting
segmentation is guaranteed with the desired properties. Our method is more flexible
in the sense that it handles more topology constraints than previous methods,
which were only able to enforce pairwise or global connectivity. In particular,
our method is very fast, making it for the first time possible to enforce global
topological properties in practical image segmentation tasks.'
acknowledgement: The first author is supported by the Austrian Science Fund (FWF)
grant No. P20134-N13. The authors would like to thank Sebastian Nowozin for helpful
discussions.
article_processing_charge: No
author:
- first_name: Chao
full_name: Chen, Chao
id: 3E92416E-F248-11E8-B48F-1D18A9856A87
last_name: Chen
- first_name: Daniel
full_name: Freedman, Daniel
last_name: Freedman
- first_name: Christoph
full_name: Lampert, Christoph
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: 'Chen C, Freedman D, Lampert C. Enforcing topological constraints in random
field image segmentation. In: CVPR: Computer Vision and Pattern Recognition.
IEEE; 2011:2089-2096. doi:10.1109/CVPR.2011.5995503'
apa: 'Chen, C., Freedman, D., & Lampert, C. (2011). Enforcing topological constraints
in random field image segmentation. In CVPR: Computer Vision and Pattern Recognition
(pp. 2089–2096). Colorado Springs, CO, United States: IEEE. https://doi.org/10.1109/CVPR.2011.5995503'
chicago: 'Chen, Chao, Daniel Freedman, and Christoph Lampert. “Enforcing Topological
Constraints in Random Field Image Segmentation.” In CVPR: Computer Vision and
Pattern Recognition, 2089–96. IEEE, 2011. https://doi.org/10.1109/CVPR.2011.5995503.'
ieee: 'C. Chen, D. Freedman, and C. Lampert, “Enforcing topological constraints
in random field image segmentation,” in CVPR: Computer Vision and Pattern Recognition,
Colorado Springs, CO, United States, 2011, pp. 2089–2096.'
ista: 'Chen C, Freedman D, Lampert C. 2011. Enforcing topological constraints in
random field image segmentation. CVPR: Computer Vision and Pattern Recognition.
CVPR: Conference on Computer Vision and Pattern Recognition, 2089–2096.'
mla: 'Chen, Chao, et al. “Enforcing Topological Constraints in Random Field Image
Segmentation.” CVPR: Computer Vision and Pattern Recognition, IEEE, 2011,
pp. 2089–96, doi:10.1109/CVPR.2011.5995503.'
short: 'C. Chen, D. Freedman, C. Lampert, in:, CVPR: Computer Vision and Pattern
Recognition, IEEE, 2011, pp. 2089–2096.'
conference:
end_date: 2011-06-25
location: Colorado Springs, CO, United States
name: 'CVPR: Conference on Computer Vision and Pattern Recognition'
start_date: 2011-06-20
date_created: 2018-12-11T12:02:45Z
date_published: 2011-07-22T00:00:00Z
date_updated: 2023-02-23T12:23:56Z
day: '22'
department:
- _id: HeEd
- _id: ChLa
doi: 10.1109/CVPR.2011.5995503
language:
- iso: eng
month: '07'
oa_version: None
page: 2089 - 2096
publication: 'CVPR: Computer Vision and Pattern Recognition'
publication_identifier:
eisbn:
- 978-1-4577-0395-9
isbn:
- 978-1-4577-0394-2
publication_status: published
publisher: IEEE
publist_id: '3294'
quality_controlled: '1'
related_material:
record:
- id: '5386'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Enforcing topological constraints in random field image segmentation
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3323'
abstract:
- lang: eng
text: We present a new decidable logic called TREX for expressing constraints about
imperative tree data structures. In particular, TREX supports a transitive closure
operator that can express reachability constraints, which often appear in data
structure invariants. We show that our logic is closed under weakest precondition
computation, which enables its use for automated software verification. We further
show that satisfiability of formulas in TREX is decidable in NP. The low complexity
makes it an attractive alternative to more expensive logics such as monadic second-order
logic (MSOL) over trees, which have been traditionally used for reasoning about
tree data structures.
alternative_title:
- 'LNAI '
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Marco
full_name: Muñiz, Marco
last_name: Muñiz
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: 'Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative
tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:10.1007/978-3-642-22438-6_36'
apa: 'Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure
for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the
CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36'
chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure
for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36.
ieee: 'T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative
tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław,
Poland, 2011, vol. 6803, pp. 476–491.'
ista: 'Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative
tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.'
mla: Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree
Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.
short: T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.
conference:
end_date: 2011-08-05
location: Wrocław, Poland
name: 'CADE 23: Automated Deduction '
start_date: 2011-07-31
date_created: 2018-12-11T12:02:40Z
date_published: 2011-07-19T00:00:00Z
date_updated: 2023-02-23T12:23:48Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-642-22438-6_36
intvolume: ' 6803'
language:
- iso: eng
month: '07'
oa_version: None
page: 476 - 491
publication_status: published
publisher: Springer
publist_id: '3312'
quality_controlled: '1'
related_material:
record:
- id: '5383'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: An efficient decision procedure for imperative tree data structures
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6803
year: '2011'
...