---
OA_place: publisher
_id: '1405'
abstract:
- lang: eng
  text: "Motivated by the analysis of highly dynamic message-passing systems, i.e.
    unbounded thread creation, mobility, etc. we present a framework for the analysis
    of depth-bounded systems. Depth-bounded systems are one of the most expressive
    known fragment of the π-calculus for which interesting verification problems are
    still decidable. Even though they are infinite state systems depth-bounded systems
    are well-structured, thus can be analyzed algorithmically. We give an interpretation
    of depth-bounded systems as graph-rewriting systems. This gives more flexibility
    and ease of use to apply depth-bounded systems to other type of systems like shared
    memory concurrency.\r\n\r\nFirst, we develop an adequate domain of limits for
    depth-bounded systems, a prerequisite for the effective representation of downward-closed
    sets. Downward-closed sets are needed by forward saturation-based algorithms to
    represent potentially infinite sets of states. Then, we present an abstract interpretation
    framework to compute the covering set of well-structured transition systems. Because,
    in general, the covering set is not computable, our abstraction over-approximates
    the actual covering set. Our abstraction captures the essence of acceleration
    based-algorithms while giving up enough precision to ensure convergence. We have
    implemented the analysis in the PICASSO tool and show that it is accurate in practice.
    Finally, we build some further analyses like termination using the covering set
    as starting point."
acknowledgement: "This work was supported in part by the Austrian Science Fund NFN
  RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative
  Reactve Modeling).\r\nChapter 2, 3, and 4 are joint work with Thomas A. Henzinger
  and Thomas Wies. Chapter 2 was published in FoSSaCS 2010 as “Forward Analysis of
  Depth-Bounded Processes” [112]. Chapter 3 was published in VMCAI 2012 as “Ideal
  Abstractions for Well-Structured Transition Systems” [114]. Chap- ter 5.1 is joint
  work with Kshitij Bansal, Eric Koskinen, and Thomas Wies. It was published in TACAS
  2013 as “Structural Counter Abstraction” [13]. The author’s contribution in this
  part is mostly related to the implementation. The theory required to understand
  the method and its implementation is quickly recalled to make the thesis self-contained,
  but should not be considered as a contribution. For the details of the methods,
  we refer the reader to the orig- inal publication [13] and the corresponding technical
  report [14]. Chapter 5.2 is ongoing work with Shahram Esmaeilsabzali, Rupak Majumdar,
  and Thomas Wies. I also would like to thank the people who supported over the past
  4 years. My advisor Thomas A. Henzinger who gave me a lot of freedom to work on
  projects I was interested in. My collaborators, especially Thomas Wies with whom
  I worked since the beginning. The members of my thesis committee, Viktor Kun- cak
  and Rupak Majumdar, who also agreed to advise me. Simon Aeschbacher, Pavol Cerny,
  Cezara Dragoi, Arjun Radhakrishna, my family, friends and col- leagues who created
  an enjoyable environment. "
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: Zufferey D. Analysis of dynamic message passing programs. 2013. doi:<a href="https://doi.org/10.15479/at:ista:1405">10.15479/at:ista:1405</a>
  apa: Zufferey, D. (2013). <i>Analysis of dynamic message passing programs</i>. Institute
    of Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:1405">https://doi.org/10.15479/at:ista:1405</a>
  chicago: Zufferey, Damien. “Analysis of Dynamic Message Passing Programs.” Institute
    of Science and Technology Austria, 2013. <a href="https://doi.org/10.15479/at:ista:1405">https://doi.org/10.15479/at:ista:1405</a>.
  ieee: D. Zufferey, “Analysis of dynamic message passing programs,” Institute of
    Science and Technology Austria, 2013.
  ista: Zufferey D. 2013. Analysis of dynamic message passing programs. Institute
    of Science and Technology Austria.
  mla: Zufferey, Damien. <i>Analysis of Dynamic Message Passing Programs</i>. Institute
    of Science and Technology Austria, 2013, doi:<a href="https://doi.org/10.15479/at:ista:1405">10.15479/at:ista:1405</a>.
  short: D. Zufferey, Analysis of Dynamic Message Passing Programs, Institute of Science
    and Technology Austria, 2013.
corr_author: '1'
date_created: 2018-12-11T11:51:50Z
date_published: 2013-09-05T00:00:00Z
date_updated: 2026-04-09T14:35:24Z
day: '05'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
- _id: GradSch
doi: 10.15479/at:ista:1405
ec_funded: 1
file:
- access_level: open_access
  checksum: ed2d7b52933d134e8dc69d569baa284e
  content_type: application/pdf
  creator: dernst
  date_created: 2021-02-22T11:28:36Z
  date_updated: 2021-02-22T11:28:36Z
  file_id: '9176'
  file_name: 2013_Zufferey_thesis_final.pdf
  file_size: 1514906
  relation: main_file
  success: 1
- access_level: closed
  checksum: cecc4c4b14225bee973d32e3dba91a55
  content_type: application/pdf
  creator: cchlebak
  date_created: 2021-11-16T14:42:52Z
  date_updated: 2021-11-17T13:47:58Z
  file_id: '10298'
  file_name: 2013_Zufferey_thesis_final_pdfa.pdf
  file_size: 1378313
  relation: main_file
file_date_updated: 2021-11-17T13:47:58Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- url: http://dzufferey.github.io/files/2013_thesis.pdf
month: '09'
oa: 1
oa_version: Published Version
page: '134'
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5802'
related_material:
  record:
  - id: '4361'
    relation: part_of_dissertation
    status: public
  - id: '3251'
    relation: part_of_dissertation
    status: public
  - id: '2847'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
title: Analysis of dynamic message passing programs
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2013'
...
---
OA_place: publisher
_id: '2964'
abstract:
- lang: eng
  text: 'CA3 pyramidal neurons are important for memory formation and pattern completion
    in the hippocampal network. These neurons receive multiple excitatory inputs from
    numerous sources. Therefore, the rules of spatiotemporal integration of multiple
    synaptic inputs and propagation of action potentials are important to understand
    how CA3 neurons contribute to higher brain functions at cellular level. By using
    confocally targeted patch-clamp recording techniques, we investigated the biophysical
    properties of rat CA3 pyramidal neuron dendrites. We found two distinct dendritic
    domains critical for action potential initiation and propagation: In the proximal
    domain, action potentials initiated in the axon backpropagate actively with large
    amplitude and fast time course. In the distal domain, Na+-channel mediated dendritic
    spikes are efficiently evoked by local dendritic depolarization or waveforms mimicking
    synaptic events. These findings can be explained by a high Na+-to-K+ conductance
    density ratio of CA3 pyramidal neuron dendrites. The results challenge the prevailing
    view that proximal mossy fiber inputs activate CA3 pyramidal neurons more efficiently
    than distal perforant inputs by showing that the distal synapses trigger a different
    form of activity represented by dendritic spikes. The high probability of dendritic
    spike initiation in the distal area may enhance the computational power of CA3
    pyramidal neurons in the hippocampal network.  '
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Sooyun
  full_name: Kim, Sooyun
  id: 394AB1C8-F248-11E8-B48F-1D18A9856A87
  last_name: Kim
citation:
  ama: Kim S. Active properties of hippocampal CA3 pyramidal neuron dendrites. 2012.
  apa: Kim, S. (2012). <i>Active properties of hippocampal CA3 pyramidal neuron dendrites</i>.
    Institute of Science and Technology Austria.
  chicago: Kim, Sooyun. “Active Properties of Hippocampal CA3 Pyramidal Neuron Dendrites.”
    Institute of Science and Technology Austria, 2012.
  ieee: S. Kim, “Active properties of hippocampal CA3 pyramidal neuron dendrites,”
    Institute of Science and Technology Austria, 2012.
  ista: Kim S. 2012. Active properties of hippocampal CA3 pyramidal neuron dendrites.
    Institute of Science and Technology Austria.
  mla: Kim, Sooyun. <i>Active Properties of Hippocampal CA3 Pyramidal Neuron Dendrites</i>.
    Institute of Science and Technology Austria, 2012.
  short: S. Kim, Active Properties of Hippocampal CA3 Pyramidal Neuron Dendrites,
    Institute of Science and Technology Austria, 2012.
corr_author: '1'
date_created: 2018-12-11T12:00:35Z
date_published: 2012-06-01T00:00:00Z
date_updated: 2026-06-18T18:41:53Z
day: '01'
degree_awarded: PhD
department:
- _id: PeJo
- _id: GradSch
language:
- iso: eng
month: '06'
oa_version: None
page: '65'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '3755'
related_material:
  record:
  - id: '3258'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Peter M
  full_name: Jonas, Peter M
  id: 353C1B58-F248-11E8-B48F-1D18A9856A87
  last_name: Jonas
  orcid: 0000-0001-5001-4804
title: Active properties of hippocampal CA3 pyramidal neuron dendrites
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2012'
...
---
OA_place: publisher
_id: '3962'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Holger
  full_name: Pflicke, Holger
  id: CAA57A9A-5B61-11E9-B130-E0C1E1F2C83D
  last_name: Pflicke
citation:
  ama: Pflicke H.   Dendritic cell migration across basement membranes in the skin.
    2010.
  apa: Pflicke, H. (2010). <i>  Dendritic cell migration across basement membranes
    in the skin</i>. Institute of Science and Technology Austria.
  chicago: Pflicke, Holger. “  Dendritic Cell Migration across Basement Membranes
    in the Skin.” Institute of Science and Technology Austria, 2010.
  ieee: H. Pflicke, “  Dendritic cell migration across basement membranes in the skin,”
    Institute of Science and Technology Austria, 2010.
  ista: Pflicke H. 2010.   Dendritic cell migration across basement membranes in the
    skin. Institute of Science and Technology Austria.
  mla: Pflicke, Holger. <i>  Dendritic Cell Migration across Basement Membranes in
    the Skin</i>. Institute of Science and Technology Austria, 2010.
  short: H. Pflicke,   Dendritic Cell Migration across Basement Membranes in the Skin,
    Institute of Science and Technology Austria, 2010.
corr_author: '1'
date_created: 2018-12-11T12:06:08Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2026-04-09T14:37:07Z
day: '01'
degree_awarded: PhD
department:
- _id: CaHe
- _id: GradSch
language:
- iso: eng
month: '07'
oa_version: None
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '2165'
status: public
supervisor:
- first_name: Carl-Philipp J
  full_name: Heisenberg, Carl-Philipp J
  id: 39427864-F248-11E8-B48F-1D18A9856A87
  last_name: Heisenberg
  orcid: 0000-0002-0912-4566
title: "\uFEFF\uFEFFDendritic cell migration across basement membranes in the skin"
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2010'
...
