---
_id: '2373'
abstract:
- lang: eng
text: For the BCS equation with local two-body interaction λV(x), we give a rigorous
analysis of the asymptotic behavior of the critical temperature as γ"0. We
derive necessary and sufficient conditions onV(x) for the existence of a nontrivial
solution for all values of γ>0.
author:
- first_name: Rupert
full_name: Frank, Rupert L
last_name: Frank
- first_name: Christian
full_name: Hainzl, Christian
last_name: Hainzl
- first_name: Serguei
full_name: Naboko, Serguei N
last_name: Naboko
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Frank R, Hainzl C, Naboko S, Seiringer R. The critical temperature for the
BCS equation at weak coupling. Journal of Geometric Analysis. 2007;17(4):559-567.
doi:10.1007/BF02937429
apa: Frank, R., Hainzl, C., Naboko, S., & Seiringer, R. (2007). The critical
temperature for the BCS equation at weak coupling. Journal of Geometric Analysis.
Springer. https://doi.org/10.1007/BF02937429
chicago: Frank, Rupert, Christian Hainzl, Serguei Naboko, and Robert Seiringer.
“The Critical Temperature for the BCS Equation at Weak Coupling.” Journal of
Geometric Analysis. Springer, 2007. https://doi.org/10.1007/BF02937429.
ieee: R. Frank, C. Hainzl, S. Naboko, and R. Seiringer, “The critical temperature
for the BCS equation at weak coupling,” Journal of Geometric Analysis,
vol. 17, no. 4. Springer, pp. 559–567, 2007.
ista: Frank R, Hainzl C, Naboko S, Seiringer R. 2007. The critical temperature for
the BCS equation at weak coupling. Journal of Geometric Analysis. 17(4), 559–567.
mla: Frank, Rupert, et al. “The Critical Temperature for the BCS Equation at Weak
Coupling.” Journal of Geometric Analysis, vol. 17, no. 4, Springer, 2007,
pp. 559–67, doi:10.1007/BF02937429.
short: R. Frank, C. Hainzl, S. Naboko, R. Seiringer, Journal of Geometric Analysis
17 (2007) 559–567.
date_created: 2018-12-11T11:57:17Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T06:57:05Z
day: '01'
doi: 10.1007/BF02937429
extern: 1
intvolume: ' 17'
issue: '4'
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/0704.3564
month: '01'
oa: 1
page: 559 - 567
publication: Journal of Geometric Analysis
publication_status: published
publisher: Springer
publist_id: '4553'
quality_controlled: 0
status: public
title: The critical temperature for the BCS equation at weak coupling
type: journal_article
volume: 17
year: '2007'
...
---
_id: '2375'
abstract:
- lang: eng
text: We give a Cwikel-Lieb-Rozenblum type bound on the number of bound states of
Schrödinger operators with matrix-valued potentials using the functional integral
method of Lieb. This significantly improves the constant in this inequality obtained
earlier by Hundertmark.
author:
- first_name: Rupert
full_name: Frank, Rupert L
last_name: Frank
- first_name: Élliott
full_name: Lieb, Élliott H
last_name: Lieb
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Frank R, Lieb É, Seiringer R. Number of bound states of Schrödinger operators
with matrix-valued potentials. Letters in Mathematical Physics. 2007;82(2-3):107-116.
doi:10.1007/s11005-007-0211-x
apa: Frank, R., Lieb, É., & Seiringer, R. (2007). Number of bound states of
Schrödinger operators with matrix-valued potentials. Letters in Mathematical
Physics. Springer. https://doi.org/10.1007/s11005-007-0211-x
chicago: Frank, Rupert, Élliott Lieb, and Robert Seiringer. “Number of Bound States
of Schrödinger Operators with Matrix-Valued Potentials.” Letters in Mathematical
Physics. Springer, 2007. https://doi.org/10.1007/s11005-007-0211-x.
ieee: R. Frank, É. Lieb, and R. Seiringer, “Number of bound states of Schrödinger
operators with matrix-valued potentials,” Letters in Mathematical Physics,
vol. 82, no. 2–3. Springer, pp. 107–116, 2007.
ista: Frank R, Lieb É, Seiringer R. 2007. Number of bound states of Schrödinger
operators with matrix-valued potentials. Letters in Mathematical Physics. 82(2–3),
107–116.
mla: Frank, Rupert, et al. “Number of Bound States of Schrödinger Operators with
Matrix-Valued Potentials.” Letters in Mathematical Physics, vol. 82, no.
2–3, Springer, 2007, pp. 107–16, doi:10.1007/s11005-007-0211-x.
short: R. Frank, É. Lieb, R. Seiringer, Letters in Mathematical Physics 82 (2007)
107–116.
date_created: 2018-12-11T11:57:18Z
date_published: 2007-12-01T00:00:00Z
date_updated: 2021-01-12T06:57:06Z
day: '01'
doi: 10.1007/s11005-007-0211-x
extern: 1
intvolume: ' 82'
issue: 2-3
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/0710.1877
month: '12'
oa: 1
page: 107 - 116
publication: Letters in Mathematical Physics
publication_status: published
publisher: Springer
publist_id: '4552'
quality_controlled: 0
status: public
title: Number of bound states of Schrödinger operators with matrix-valued potentials
type: journal_article
volume: 82
year: '2007'
...
---
_id: '7323'
abstract:
- lang: eng
text: The main factors for reducing the consumption of a vehicle are reduction of
curb weight, air drag and increase in the drivetrain efficiency. Highly efficient
drivetrains can be developed based on PEFC technology and curb weight may be limited
by an innovative vehicle construction. In this paper, data on consumption and
efficiency of a four‐place passenger vehicle with a curb weight of 850 kg and
an H2/O2 fed PEFC/Supercap hybrid electric powertrain are presented. Hydrogen
consumption in the New European Driving Cycle is 0.67 kg H2/100 km, which corresponds
to a gasoline equivalent consumption of 2.5 l/100 km. When including the energy
needed to supply pure oxygen, the calculated consumption increases from 0.67 to
0.69–0.79 kg H2/100 km, depending on the method of oxygen production.
article_processing_charge: No
article_type: original
author:
- first_name: F. N.
full_name: Büchi, F. N.
last_name: Büchi
- first_name: G.
full_name: Paganelli, G.
last_name: Paganelli
- first_name: P.
full_name: Dietrich, P.
last_name: Dietrich
- first_name: D.
full_name: Laurent, D.
last_name: Laurent
- first_name: A.
full_name: Tsukada, A.
last_name: Tsukada
- first_name: P.
full_name: Varenne, P.
last_name: Varenne
- first_name: A.
full_name: Delfino, A.
last_name: Delfino
- first_name: R.
full_name: Kötz, R.
last_name: Kötz
- first_name: Stefan Alexander
full_name: Freunberger, Stefan Alexander
id: A8CA28E6-CE23-11E9-AD2D-EC27E6697425
last_name: Freunberger
orcid: 0000-0003-2902-5319
- first_name: P.-A.
full_name: Magne, P.-A.
last_name: Magne
- first_name: D.
full_name: Walser, D.
last_name: Walser
- first_name: D.
full_name: Olsommer, D.
last_name: Olsommer
citation:
ama: Büchi FN, Paganelli G, Dietrich P, et al. Consumption and efficiency of a passenger
car with a Hydrogen/Oxygen PEFC based hybrid electric drivetrain. Fuel Cells.
2007;7(4):329-335. doi:10.1002/fuce.200600050
apa: Büchi, F. N., Paganelli, G., Dietrich, P., Laurent, D., Tsukada, A., Varenne,
P., … Olsommer, D. (2007). Consumption and efficiency of a passenger car with
a Hydrogen/Oxygen PEFC based hybrid electric drivetrain. Fuel Cells. Wiley.
https://doi.org/10.1002/fuce.200600050
chicago: Büchi, F. N., G. Paganelli, P. Dietrich, D. Laurent, A. Tsukada, P. Varenne,
A. Delfino, et al. “Consumption and Efficiency of a Passenger Car with a Hydrogen/Oxygen
PEFC Based Hybrid Electric Drivetrain.” Fuel Cells. Wiley, 2007. https://doi.org/10.1002/fuce.200600050.
ieee: F. N. Büchi et al., “Consumption and efficiency of a passenger car
with a Hydrogen/Oxygen PEFC based hybrid electric drivetrain,” Fuel Cells,
vol. 7, no. 4. Wiley, pp. 329–335, 2007.
ista: Büchi FN, Paganelli G, Dietrich P, Laurent D, Tsukada A, Varenne P, Delfino
A, Kötz R, Freunberger SA, Magne P-A, Walser D, Olsommer D. 2007. Consumption
and efficiency of a passenger car with a Hydrogen/Oxygen PEFC based hybrid electric
drivetrain. Fuel Cells. 7(4), 329–335.
mla: Büchi, F. N., et al. “Consumption and Efficiency of a Passenger Car with a
Hydrogen/Oxygen PEFC Based Hybrid Electric Drivetrain.” Fuel Cells, vol.
7, no. 4, Wiley, 2007, pp. 329–35, doi:10.1002/fuce.200600050.
short: F.N. Büchi, G. Paganelli, P. Dietrich, D. Laurent, A. Tsukada, P. Varenne,
A. Delfino, R. Kötz, S.A. Freunberger, P.-A. Magne, D. Walser, D. Olsommer, Fuel
Cells 7 (2007) 329–335.
date_created: 2020-01-15T12:22:10Z
date_published: 2007-08-01T00:00:00Z
date_updated: 2021-01-12T08:13:04Z
day: '01'
doi: 10.1002/fuce.200600050
extern: '1'
intvolume: ' 7'
issue: '4'
language:
- iso: eng
month: '08'
oa_version: None
page: 329-335
publication: Fuel Cells
publication_identifier:
issn:
- 1615-6846
- 1615-6854
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: Consumption and efficiency of a passenger car with a Hydrogen/Oxygen PEFC based
hybrid electric drivetrain
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2007'
...
---
_id: '7324'
abstract:
- lang: eng
text: Efficiency is the key parameter for the application of fuel cells in automotive
applications. The efficiency of a hydrogen/oxygen polymer electrolyte fuel cell
system is analyzed and compared to hydrogen/air systems. The analysis is performed
for the tank to electric power chain. Furthermore, the additional energy required
for using pure oxygen as a second fuel is analyzed and included in the calculation.
The results show that if hydrogen is produced from primary fossil energy carriers,
such as natural gas and pure oxygen needs to be obtained by a conventional process;
the fuel to electric current efficiency is comparable for hydrogen/oxygen and
hydrogen/air systems. However, if hydrogen and oxygen are produced by the splitting
of water, i.e., by electrolysis or by a thermochemical process, the fuel to electric
current efficiency for the hydrogen/oxygen system is clearly superior.
article_processing_charge: No
article_type: original
author:
- first_name: F. N.
full_name: Büchi, F. N.
last_name: Büchi
- first_name: Stefan Alexander
full_name: Freunberger, Stefan Alexander
id: A8CA28E6-CE23-11E9-AD2D-EC27E6697425
last_name: Freunberger
orcid: 0000-0003-2902-5319
- first_name: M.
full_name: Reum, M.
last_name: Reum
- first_name: G.
full_name: Paganelli, G.
last_name: Paganelli
- first_name: A.
full_name: Tsukada, A.
last_name: Tsukada
- first_name: P.
full_name: Dietrich, P.
last_name: Dietrich
- first_name: A.
full_name: Delfino, A.
last_name: Delfino
citation:
ama: Büchi FN, Freunberger SA, Reum M, et al. On the efficiency of an advanced automotive
fuel cell system. Fuel Cells. 2007;7(2):159-164. doi:10.1002/fuce.200500257
apa: Büchi, F. N., Freunberger, S. A., Reum, M., Paganelli, G., Tsukada, A., Dietrich,
P., & Delfino, A. (2007). On the efficiency of an advanced automotive fuel
cell system. Fuel Cells. Wiley. https://doi.org/10.1002/fuce.200500257
chicago: Büchi, F. N., Stefan Alexander Freunberger, M. Reum, G. Paganelli, A. Tsukada,
P. Dietrich, and A. Delfino. “On the Efficiency of an Advanced Automotive Fuel
Cell System.” Fuel Cells. Wiley, 2007. https://doi.org/10.1002/fuce.200500257.
ieee: F. N. Büchi et al., “On the efficiency of an advanced automotive fuel
cell system,” Fuel Cells, vol. 7, no. 2. Wiley, pp. 159–164, 2007.
ista: Büchi FN, Freunberger SA, Reum M, Paganelli G, Tsukada A, Dietrich P, Delfino
A. 2007. On the efficiency of an advanced automotive fuel cell system. Fuel Cells.
7(2), 159–164.
mla: Büchi, F. N., et al. “On the Efficiency of an Advanced Automotive Fuel Cell
System.” Fuel Cells, vol. 7, no. 2, Wiley, 2007, pp. 159–64, doi:10.1002/fuce.200500257.
short: F.N. Büchi, S.A. Freunberger, M. Reum, G. Paganelli, A. Tsukada, P. Dietrich,
A. Delfino, Fuel Cells 7 (2007) 159–164.
date_created: 2020-01-15T12:22:20Z
date_published: 2007-04-01T00:00:00Z
date_updated: 2021-01-12T08:13:04Z
day: '01'
doi: 10.1002/fuce.200500257
extern: '1'
intvolume: ' 7'
issue: '2'
language:
- iso: eng
month: '04'
oa_version: None
page: 159-164
publication: Fuel Cells
publication_identifier:
issn:
- 1615-6846
- 1615-6854
publication_status: published
publisher: Wiley
status: public
title: On the efficiency of an advanced automotive fuel cell system
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2007'
...
---
_id: '7325'
abstract:
- lang: eng
text: Our experimental results shown here disprove that finite diffusion can generally
be assumed in ac impedance models for H2/air-polymer electrolyte fuel cells (PEFCs)
to account for the diffusive transport of oxygen through the gas diffusion layer
(GDL) toward the air electrode. It is shown that the amplitude of the oxygen concentration
oscillation created as a consequence of superimposed ac current at the air electrode
is not zero at the channel/GDL interface but extends into the gas channels, at
least below modulation frequencies of fmod=10 Hz . By this, sinusoidal oxygen-concentration
oscillations within the cathode gas channels are excited locally along the flow
field. Due to the forced air convection in the cathode flow-field channels, a
coupling via the gas phase occurs downstream of the flow field. The coupling strongly
affects the local and by this the overall impedance response of the cell and evokes
the formation of a low-frequency arc in H2/air-PEFC impedance spectra. Based on
the experimental results, a qualitative model is presented explaining the local
impedance response of a segmented 200cm2H2/air PEFC.
article_number: B383
article_processing_charge: No
article_type: original
author:
- first_name: I. A.
full_name: Schneider, I. A.
last_name: Schneider
- first_name: Stefan Alexander
full_name: Freunberger, Stefan Alexander
id: A8CA28E6-CE23-11E9-AD2D-EC27E6697425
last_name: Freunberger
orcid: 0000-0003-2902-5319
- first_name: D.
full_name: Kramer, D.
last_name: Kramer
- first_name: A.
full_name: Wokaun, A.
last_name: Wokaun
- first_name: G. G.
full_name: Scherer, G. G.
last_name: Scherer
citation:
ama: 'Schneider IA, Freunberger SA, Kramer D, Wokaun A, Scherer GG. Oscillations
in gas channels: Part I. The forgotten player in impedance spectroscopy in PEFCs.
Journal of The Electrochemical Society. 2007;154(4). doi:10.1149/1.2435706'
apa: 'Schneider, I. A., Freunberger, S. A., Kramer, D., Wokaun, A., & Scherer,
G. G. (2007). Oscillations in gas channels: Part I. The forgotten player in impedance
spectroscopy in PEFCs. Journal of The Electrochemical Society. The Electrochemical
Society. https://doi.org/10.1149/1.2435706'
chicago: 'Schneider, I. A., Stefan Alexander Freunberger, D. Kramer, A. Wokaun,
and G. G. Scherer. “Oscillations in Gas Channels: Part I. The Forgotten Player
in Impedance Spectroscopy in PEFCs.” Journal of The Electrochemical Society.
The Electrochemical Society, 2007. https://doi.org/10.1149/1.2435706.'
ieee: 'I. A. Schneider, S. A. Freunberger, D. Kramer, A. Wokaun, and G. G. Scherer,
“Oscillations in gas channels: Part I. The forgotten player in impedance spectroscopy
in PEFCs,” Journal of The Electrochemical Society, vol. 154, no. 4. The
Electrochemical Society, 2007.'
ista: 'Schneider IA, Freunberger SA, Kramer D, Wokaun A, Scherer GG. 2007. Oscillations
in gas channels: Part I. The forgotten player in impedance spectroscopy in PEFCs.
Journal of The Electrochemical Society. 154(4), B383.'
mla: 'Schneider, I. A., et al. “Oscillations in Gas Channels: Part I. The Forgotten
Player in Impedance Spectroscopy in PEFCs.” Journal of The Electrochemical
Society, vol. 154, no. 4, B383, The Electrochemical Society, 2007, doi:10.1149/1.2435706.'
short: I.A. Schneider, S.A. Freunberger, D. Kramer, A. Wokaun, G.G. Scherer, Journal
of The Electrochemical Society 154 (2007).
date_created: 2020-01-15T12:22:31Z
date_published: 2007-02-09T00:00:00Z
date_updated: 2021-01-12T08:13:05Z
day: '09'
doi: 10.1149/1.2435706
extern: '1'
intvolume: ' 154'
issue: '4'
language:
- iso: eng
month: '02'
oa_version: None
publication: Journal of The Electrochemical Society
publication_identifier:
issn:
- 0013-4651
publication_status: published
publisher: The Electrochemical Society
quality_controlled: '1'
status: public
title: 'Oscillations in gas channels: Part I. The forgotten player in impedance spectroscopy
in PEFCs'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 154
year: '2007'
...
---
_id: '7704'
abstract:
- lang: eng
text: Gradients of axon guidance molecules instruct the formation of continuous
neural maps, such as the retinotopic map in the vertebrate visual system. Here
we show that molecular gradients can also instruct the formation of a discrete
neural map. In the fly olfactory system, axons of 50 classes of olfactory receptor
neurons (ORNs) and dendrites of 50 classes of projection neurons (PNs) form one-to-one
connections at discrete units called glomeruli. We provide expression, loss- and
gain-of-function data to demonstrate that the levels of transmembrane Semaphorin-1a
(Sema-1a), acting cell-autonomously as a receptor or part of a receptor complex,
direct the dendritic targeting of PNs along the dorsolateral to ventromedial axis
of the antennal lobe. Sema-1a also regulates PN axon targeting in higher olfactory
centers. Thus, graded expression of Sema-1a contributes to connection specificity
from ORNs to PNs and then to higher brain centers, ensuring proper representation
of olfactory information in the brain.
article_processing_charge: No
article_type: original
author:
- first_name: Takaki
full_name: Komiyama, Takaki
last_name: Komiyama
- first_name: Lora Beatrice Jaeger
full_name: Sweeney, Lora Beatrice Jaeger
id: 56BE8254-C4F0-11E9-8E45-0B23E6697425
last_name: Sweeney
orcid: 0000-0001-9242-5601
- first_name: Oren
full_name: Schuldiner, Oren
last_name: Schuldiner
- first_name: K. Christopher
full_name: Garcia, K. Christopher
last_name: Garcia
- first_name: Liqun
full_name: Luo, Liqun
last_name: Luo
citation:
ama: Komiyama T, Sweeney LB, Schuldiner O, Garcia KC, Luo L. Graded expression of
semaphorin-1a cell-autonomously directs dendritic targeting of olfactory projection
neurons. Cell. 2007;128(2):399-410. doi:10.1016/j.cell.2006.12.028
apa: Komiyama, T., Sweeney, L. B., Schuldiner, O., Garcia, K. C., & Luo, L.
(2007). Graded expression of semaphorin-1a cell-autonomously directs dendritic
targeting of olfactory projection neurons. Cell. Elsevier. https://doi.org/10.1016/j.cell.2006.12.028
chicago: Komiyama, Takaki, Lora B. Sweeney, Oren Schuldiner, K. Christopher Garcia,
and Liqun Luo. “Graded Expression of Semaphorin-1a Cell-Autonomously Directs Dendritic
Targeting of Olfactory Projection Neurons.” Cell. Elsevier, 2007. https://doi.org/10.1016/j.cell.2006.12.028.
ieee: T. Komiyama, L. B. Sweeney, O. Schuldiner, K. C. Garcia, and L. Luo, “Graded
expression of semaphorin-1a cell-autonomously directs dendritic targeting of olfactory
projection neurons,” Cell, vol. 128, no. 2. Elsevier, pp. 399–410, 2007.
ista: Komiyama T, Sweeney LB, Schuldiner O, Garcia KC, Luo L. 2007. Graded expression
of semaphorin-1a cell-autonomously directs dendritic targeting of olfactory projection
neurons. Cell. 128(2), 399–410.
mla: Komiyama, Takaki, et al. “Graded Expression of Semaphorin-1a Cell-Autonomously
Directs Dendritic Targeting of Olfactory Projection Neurons.” Cell, vol.
128, no. 2, Elsevier, 2007, pp. 399–410, doi:10.1016/j.cell.2006.12.028.
short: T. Komiyama, L.B. Sweeney, O. Schuldiner, K.C. Garcia, L. Luo, Cell 128 (2007)
399–410.
date_created: 2020-04-30T10:37:08Z
date_published: 2007-01-26T00:00:00Z
date_updated: 2024-01-31T10:14:48Z
day: '26'
doi: 10.1016/j.cell.2006.12.028
extern: '1'
intvolume: ' 128'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 399-410
publication: Cell
publication_identifier:
issn:
- 0092-8674
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Graded expression of semaphorin-1a cell-autonomously directs dendritic targeting
of olfactory projection neurons
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 128
year: '2007'
...
---
_id: '7705'
abstract:
- lang: eng
text: Axon-axon interactions have been implicated in neural circuit assembly, but
the underlying mechanisms are poorly understood. Here, we show that in the Drosophila
antennal lobe, early-arriving axons of olfactory receptor neurons (ORNs) from
the antenna are required for the proper targeting of late-arriving ORN axons from
the maxillary palp (MP). Semaphorin-1a is required for targeting of all MP but
only half of the antennal ORN classes examined. Sema-1a acts nonautonomously to
control ORN axon-axon interactions, in contrast to its cell-autonomous function
in olfactory projection neurons. Phenotypic and genetic interaction analyses implicate
PlexinA as the Sema-1a receptor in ORN targeting. Sema-1a on antennal ORN axons
is required for correct targeting of MP axons within the antennal lobe, while
interactions amongst MP axons facilitate their entry into the antennal lobe. We
propose that Sema-1a/PlexinA-mediated repulsion provides a mechanism by which
early-arriving ORN axons constrain the target choices of late-arriving axons.
article_processing_charge: No
article_type: original
author:
- first_name: Lora Beatrice Jaeger
full_name: Sweeney, Lora Beatrice Jaeger
id: 56BE8254-C4F0-11E9-8E45-0B23E6697425
last_name: Sweeney
orcid: 0000-0001-9242-5601
- first_name: Africa
full_name: Couto, Africa
last_name: Couto
- first_name: Ya-Hui
full_name: Chou, Ya-Hui
last_name: Chou
- first_name: Daniela
full_name: Berdnik, Daniela
last_name: Berdnik
- first_name: Barry J.
full_name: Dickson, Barry J.
last_name: Dickson
- first_name: Liqun
full_name: Luo, Liqun
last_name: Luo
- first_name: Takaki
full_name: Komiyama, Takaki
last_name: Komiyama
citation:
ama: Sweeney LB, Couto A, Chou Y-H, et al. Temporal target restriction of olfactory
receptor neurons by semaphorin-1a/plexinA-mediated axon-axon interactions. Neuron.
2007;53(2):185-200. doi:10.1016/j.neuron.2006.12.022
apa: Sweeney, L. B., Couto, A., Chou, Y.-H., Berdnik, D., Dickson, B. J., Luo, L.,
& Komiyama, T. (2007). Temporal target restriction of olfactory receptor neurons
by semaphorin-1a/plexinA-mediated axon-axon interactions. Neuron. Elsevier.
https://doi.org/10.1016/j.neuron.2006.12.022
chicago: Sweeney, Lora B., Africa Couto, Ya-Hui Chou, Daniela Berdnik, Barry J.
Dickson, Liqun Luo, and Takaki Komiyama. “Temporal Target Restriction of Olfactory
Receptor Neurons by Semaphorin-1a/PlexinA-Mediated Axon-Axon Interactions.” Neuron.
Elsevier, 2007. https://doi.org/10.1016/j.neuron.2006.12.022.
ieee: L. B. Sweeney et al., “Temporal target restriction of olfactory receptor
neurons by semaphorin-1a/plexinA-mediated axon-axon interactions,” Neuron,
vol. 53, no. 2. Elsevier, pp. 185–200, 2007.
ista: Sweeney LB, Couto A, Chou Y-H, Berdnik D, Dickson BJ, Luo L, Komiyama T. 2007.
Temporal target restriction of olfactory receptor neurons by semaphorin-1a/plexinA-mediated
axon-axon interactions. Neuron. 53(2), 185–200.
mla: Sweeney, Lora B., et al. “Temporal Target Restriction of Olfactory Receptor
Neurons by Semaphorin-1a/PlexinA-Mediated Axon-Axon Interactions.” Neuron,
vol. 53, no. 2, Elsevier, 2007, pp. 185–200, doi:10.1016/j.neuron.2006.12.022.
short: L.B. Sweeney, A. Couto, Y.-H. Chou, D. Berdnik, B.J. Dickson, L. Luo, T.
Komiyama, Neuron 53 (2007) 185–200.
date_created: 2020-04-30T10:37:24Z
date_published: 2007-01-18T00:00:00Z
date_updated: 2024-01-31T10:14:39Z
day: '18'
doi: 10.1016/j.neuron.2006.12.022
extern: '1'
intvolume: ' 53'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 185-200
publication: Neuron
publication_identifier:
issn:
- 0896-6273
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Temporal target restriction of olfactory receptor neurons by semaphorin-1a/plexinA-mediated
axon-axon interactions
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 53
year: '2007'
...
---
_id: '7753'
abstract:
- lang: eng
text: 'In many species, females show reduced expression of a trait that is under
sexual selection in males, and this expression is thought to be maintained through
genetic associations with the male phenotype. However, there is also the potential
for the female trait to convey an advantage in intrasexual conflicts over resources.
We tested this hypothesis in a feral population of Soay sheep, in which males
and females have a polymorphism for horn development, producing either full (normal
horned), reduced (scurred) or no (polled, females only) horns. During the lambing
period, females who possessed horns were more likely to initiate and win aggressive
interactions, independent of age, weight and birthing status. The occurrence of
aggression was also context dependent, decreasing over the lambing period and
associated with local density. Our results demonstrate that a trait that confers
benefits to males during intrasexual competition for mates may also be used by
females in intrasexual competition over resources: males use weaponry to gain
mates, whereas females use weaponry to gain food.'
article_processing_charge: No
article_type: original
author:
- first_name: Matthew Richard
full_name: Robinson, Matthew Richard
id: E5D42276-F5DA-11E9-8E24-6303E6697425
last_name: Robinson
orcid: 0000-0001-8982-8813
- first_name: Loeske E.B
full_name: Kruuk, Loeske E.B
last_name: Kruuk
citation:
ama: 'Robinson MR, Kruuk LE. Function of weaponry in females: The use of horns in
intrasexual competition for resources in female Soay sheep. Biology Letters.
2007;3(6):651-654. doi:10.1098/rsbl.2007.0278'
apa: 'Robinson, M. R., & Kruuk, L. E. . (2007). Function of weaponry in females:
The use of horns in intrasexual competition for resources in female Soay sheep.
Biology Letters. The Royal Society. https://doi.org/10.1098/rsbl.2007.0278'
chicago: 'Robinson, Matthew Richard, and Loeske E.B Kruuk. “Function of Weaponry
in Females: The Use of Horns in Intrasexual Competition for Resources in Female
Soay Sheep.” Biology Letters. The Royal Society, 2007. https://doi.org/10.1098/rsbl.2007.0278.'
ieee: 'M. R. Robinson and L. E. . Kruuk, “Function of weaponry in females: The use
of horns in intrasexual competition for resources in female Soay sheep,” Biology
Letters, vol. 3, no. 6. The Royal Society, pp. 651–654, 2007.'
ista: 'Robinson MR, Kruuk LE. 2007. Function of weaponry in females: The use of
horns in intrasexual competition for resources in female Soay sheep. Biology Letters.
3(6), 651–654.'
mla: 'Robinson, Matthew Richard, and Loeske E. .. Kruuk. “Function of Weaponry in
Females: The Use of Horns in Intrasexual Competition for Resources in Female Soay
Sheep.” Biology Letters, vol. 3, no. 6, The Royal Society, 2007, pp. 651–54,
doi:10.1098/rsbl.2007.0278.'
short: M.R. Robinson, L.E.. Kruuk, Biology Letters 3 (2007) 651–654.
date_created: 2020-04-30T11:02:28Z
date_published: 2007-08-21T00:00:00Z
date_updated: 2021-01-12T08:15:18Z
day: '21'
doi: 10.1098/rsbl.2007.0278
extern: '1'
external_id:
pmid:
- '17711817'
intvolume: ' 3'
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1098/rsbl.2007.0278
month: '08'
oa: 1
oa_version: Published Version
page: 651-654
pmid: 1
publication: Biology Letters
publication_identifier:
issn:
- 1744-9561
- 1744-957X
publication_status: published
publisher: The Royal Society
quality_controlled: '1'
status: public
title: 'Function of weaponry in females: The use of horns in intrasexual competition
for resources in female Soay sheep'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 3
year: '2007'
...
---
_id: '4559'
abstract:
- lang: eng
text: |-
We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not.
We establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless \epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real \epsilon>0, where an \epsilon-optimal strategy achieves the value of the game with in \epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games.
We then go beyond \omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME.
Finally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.
acknowledgement: Technical Report No. UCB/EECS-2007-122
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Chatterjee K. Stochastic ω-Regular Games. 2007:1-247.
apa: Chatterjee, K. (2007). Stochastic ω-Regular Games. University of California,
Berkeley.
chicago: Chatterjee, Krishnendu. “Stochastic ω-Regular Games.” University of California,
Berkeley, 2007.
ieee: K. Chatterjee, “Stochastic ω-Regular Games,” University of California, Berkeley,
2007.
ista: Chatterjee K. 2007. Stochastic ω-Regular Games. University of California,
Berkeley.
mla: Chatterjee, Krishnendu. Stochastic ω-Regular Games. University of California,
Berkeley, 2007, pp. 1–247.
short: K. Chatterjee, Stochastic ω-Regular Games, University of California, Berkeley,
2007.
date_created: 2018-12-11T12:09:29Z
date_published: 2007-10-08T00:00:00Z
date_updated: 2021-01-12T07:59:42Z
day: '08'
extern: 1
main_file_link:
- open_access: '0'
url: http://chess.eecs.berkeley.edu/pubs/462.html
month: '10'
page: 1 - 247
publication_status: published
publisher: University of California, Berkeley
publist_id: '150'
quality_controlled: 0
status: public
title: Stochastic ω-Regular Games
type: dissertation
year: '2007'
...
---
_id: '4566'
abstract:
- lang: eng
text: "Complex system design today calls for compositional design and implementation.
However each component is designed with certain assumptions about the environment
it is meant to operate in, and delivering certain guarantees if those assumptions
are satisfied; numerous inter-component interaction errors are introduced in the
manual and error-prone integration process as there is little support in design
environments for machine-readably representing these assumptions and guarantees
and automatically checking consistency during integration.\r\n\r\nBased on Interface
Automata we propose a framework for compositional design and analysis of systems:
a set of domain-specific automata-theoretic type systems for compositional system
specification and analysis by behavioral specification of open systems. We focus
on three different domains: component-based hardware systems communicating on
bidirectional wires. concurrent distributed recursive message-passing software
systems, and embedded software system components operating in resource-constrained
environments. For these domains we present approaches to formally represent the
assumptions and conditional guarantees between interacting open system components.
Composition of such components produces new components with the appropriate assumptions
and guarantees. We check satisfaction of temporal logic specifications by such
components, and the substitutability of one component with another in an arbitrary
context. Using this framework one can analyze large systems incrementally without
needing extensive summary information to close the system at each stage. Furthermore,
we focus only on the inter-component interaction behavior without dealing with
the full implementation details of each component. Many of the merits of automata-theoretic
model-checking are combined with the compositionality afforded by type-system
based techniques. We also present an integer-based extension of the conventional
boolean verification framework motivated by our interface formalism for embedded
software components.\r\n\r\nOur algorithms for checking the behavioral compatibility
of component interfaces are available in our tool Chic, which can be used as a
plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment
Ptolemy II.\r\n\r\nFinally, we address the complementary problem of partitioning
a large system into meaningful coherent components by analyzing the interaction
patterns between its basic elements. We demonstrate the usefulness of our partitioning
approach by evaluating its efficacy in improving unit-test branch coverage for
a large software system implemented in C."
article_processing_charge: No
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
citation:
ama: Chakrabarti A. A framework for compositional design and analysis of systems.
2007:1-244.
apa: Chakrabarti, A. (2007). A framework for compositional design and analysis
of systems. University of California, Berkeley.
chicago: Chakrabarti, Arindam. “A Framework for Compositional Design and Analysis
of Systems.” University of California, Berkeley, 2007.
ieee: A. Chakrabarti, “A framework for compositional design and analysis of systems,”
University of California, Berkeley, 2007.
ista: Chakrabarti A. 2007. A framework for compositional design and analysis of
systems. University of California, Berkeley.
mla: Chakrabarti, Arindam. A Framework for Compositional Design and Analysis
of Systems. University of California, Berkeley, 2007, pp. 1–244.
short: A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems,
University of California, Berkeley, 2007.
date_created: 2018-12-11T12:09:31Z
date_published: 2007-12-20T00:00:00Z
date_updated: 2021-01-12T07:59:45Z
day: '20'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 244
publication_status: published
publisher: University of California, Berkeley
publist_id: '145'
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
- first_name: George
full_name: Necula, George
last_name: Necula
- first_name: Edward
full_name: Lee, Edward
last_name: Lee
- first_name: Jack
full_name: Silver, Jack
last_name: Silver
title: A framework for compositional design and analysis of systems
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2007'
...
---
_id: '4567'
abstract:
- lang: eng
text: BLAST is an automatic verification tool for checking temporal safety properties
of C programs. Given a C program and a temporal safety property, BLAST either
statically proves that the program satisfies the safety property, or provides
an execution path that exhibits a violation of the property (or, since the problem
is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions
of the program state space based on lazy predicate abstraction and interpolation-based
predicate discovery. This paper gives an introduction to BLAST and demonstrates,
through two case studies, how it can be applied to program verification and test-case
generation. In the first case study, we use BLAST to statically prove memory safety
for C programs. We use CCured, a type-based memory-safety analyzer, to annotate
a program with run-time assertions that check for safe memory operations. Then,
we use BLAST to remove as many of the run-time checks as possible (by proving
that these checks never fail), and to generate execution scenarios that violate
the assertions for the remaining run-time checks. In our second case study, we
use BLAST to automatically generate test suites that guarantee full coverage with
respect to a given predicate. Given a C program and a target predicate p, BLAST
determines the program locations q for which there exists a program execution
that reaches q with p true, and automatically generates a set of test vectors
that cause such executions. Our experiments show that BLAST can provide automated,
precise, and scalable analysis for C programs.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker BLAST:
Applications to software engineering. International Journal on Software Tools
for Technology Transfer. 2007;9(5):505-525. doi:10.1007/s10009-007-0044-z'
apa: 'Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2007). The software
model checker BLAST: Applications to software engineering. International Journal
on Software Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-007-0044-z'
chicago: 'Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar.
“The Software Model Checker BLAST: Applications to Software Engineering.” International
Journal on Software Tools for Technology Transfer. Springer, 2007. https://doi.org/10.1007/s10009-007-0044-z.'
ieee: 'D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “The software model
checker BLAST: Applications to software engineering,” International Journal
on Software Tools for Technology Transfer, vol. 9, no. 5. Springer, pp. 505–525,
2007.'
ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2007. The software model checker
BLAST: Applications to software engineering. International Journal on Software
Tools for Technology Transfer. 9(5), 505–525.'
mla: 'Beyer, Dirk, et al. “The Software Model Checker BLAST: Applications to Software
Engineering.” International Journal on Software Tools for Technology Transfer,
vol. 9, no. 5, Springer, 2007, pp. 505–25, doi:10.1007/s10009-007-0044-z.'
short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, International Journal on
Software Tools for Technology Transfer 9 (2007) 505–525.
date_created: 2018-12-11T12:09:31Z
date_published: 2007-10-01T00:00:00Z
date_updated: 2021-01-12T07:59:45Z
day: '01'
doi: 10.1007/s10009-007-0044-z
extern: 1
intvolume: ' 9'
issue: '5'
month: '10'
page: 505 - 525
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '139'
quality_controlled: 0
status: public
title: 'The software model checker BLAST: Applications to software engineering'
type: journal_article
volume: 9
year: '2007'
...
---
_id: '4570'
abstract:
- lang: eng
text: We consider the minimum-time reachability problem in concurrent two-player
timed automaton game structures. We show how to compute the minimum time needed
by a player to reach a target location against all possible choices of the opponent.
We do not put any syntactic restriction on the game structure, nor do we require
any player to guarantee time divergence. We only require players to use receptive
strategies which do not block time. The minimal time is computed in part using
a fixpoint expression, which we show can be evaluated on equivalence classes of
a non-trivial extension of the clock-region equivalence relation for timed automata.
acknowledgement: This research was supported in part by the NSF grant CCR-0225610
and by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Thomas
full_name: Brihaye, Thomas
last_name: Brihaye
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
- first_name: Jean
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: 'Brihaye T, Henzinger TA, Prabhu V, Raskin J. Minimum-time reachability in
timed games. In: Vol 4596. Springer; 2007:825-837. doi:10.1007/978-3-540-73420-8_71'
apa: 'Brihaye, T., Henzinger, T. A., Prabhu, V., & Raskin, J. (2007). Minimum-time
reachability in timed games (Vol. 4596, pp. 825–837). Presented at the ICALP:
Automata, Languages and Programming, Springer. https://doi.org/10.1007/978-3-540-73420-8_71'
chicago: Brihaye, Thomas, Thomas A Henzinger, Vinayak Prabhu, and Jean Raskin. “Minimum-Time
Reachability in Timed Games,” 4596:825–37. Springer, 2007. https://doi.org/10.1007/978-3-540-73420-8_71.
ieee: 'T. Brihaye, T. A. Henzinger, V. Prabhu, and J. Raskin, “Minimum-time reachability
in timed games,” presented at the ICALP: Automata, Languages and Programming,
2007, vol. 4596, pp. 825–837.'
ista: 'Brihaye T, Henzinger TA, Prabhu V, Raskin J. 2007. Minimum-time reachability
in timed games. ICALP: Automata, Languages and Programming, LNCS, vol. 4596, 825–837.'
mla: Brihaye, Thomas, et al. Minimum-Time Reachability in Timed Games. Vol.
4596, Springer, 2007, pp. 825–37, doi:10.1007/978-3-540-73420-8_71.
short: T. Brihaye, T.A. Henzinger, V. Prabhu, J. Raskin, in:, Springer, 2007, pp.
825–837.
conference:
name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-06-29T00:00:00Z
date_updated: 2021-01-12T07:59:47Z
day: '29'
doi: 10.1007/978-3-540-73420-8_71
extern: 1
intvolume: ' 4596'
month: '06'
page: 825 - 837
publication_status: published
publisher: Springer
publist_id: '142'
quality_controlled: 0
status: public
title: Minimum-time reachability in timed games
type: conference
volume: 4596
year: '2007'
...
---
_id: '4571'
abstract:
- lang: eng
text: The success of software verification depends on the ability to find a suitable
abstraction of a program automatically. We propose a method for automated abstraction
refinement which overcomes some limitations of current predicate discovery schemes.
In current schemes, the cause of a false alarm is identified as an infeasible
error path, and the abstraction is refined in order to remove that path. By contrast,
we view the cause of a false alarm -the spurious counterexample- as a full-fledged
program, namely, a fragment of the original program whose control-flow graph may
contain loops and represent unbounded computations. There are two advantages to
using such path programs as counterexamples for abstraction refinement. First,
we can bring the whole machinery of program analysis to bear on path programs,
which are typically small compared to the original program. Specifically, we use
constraint-based invariant generation to automatically infer invariants of path
programs-so-called path invariants. Second, we use path invariants for abstraction
refinement in order to remove not one infeasibility at a time, but at once all
(possibly infinitely many) infeasible error computations that are represented
by a path program. Unlike previous predicate discovery schemes, our method handles
loops without unrolling them; it infers abstractions that involve universal quantification
and naturally incorporates disjunctive reasoning.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
citation:
ama: 'Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Path invariants. In: ACM;
2007:300-309. doi:10.1145/1250734.1250769'
apa: 'Beyer, D., Henzinger, T. A., Majumdar, R., & Rybalchenko, A. (2007). Path
invariants (pp. 300–309). Presented at the PLDI: Programming Languages Design
and Implementation, ACM. https://doi.org/10.1145/1250734.1250769'
chicago: Beyer, Dirk, Thomas A Henzinger, Ritankar Majumdar, and Andrey Rybalchenko.
“Path Invariants,” 300–309. ACM, 2007. https://doi.org/10.1145/1250734.1250769.
ieee: 'D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Path invariants,”
presented at the PLDI: Programming Languages Design and Implementation, 2007,
pp. 300–309.'
ista: 'Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. 2007. Path invariants.
PLDI: Programming Languages Design and Implementation, 300–309.'
mla: Beyer, Dirk, et al. Path Invariants. ACM, 2007, pp. 300–09, doi:10.1145/1250734.1250769.
short: D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, ACM, 2007, pp.
300–309.
conference:
name: 'PLDI: Programming Languages Design and Implementation'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-06-01T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '01'
doi: 10.1145/1250734.1250769
extern: 1
month: '06'
page: 300 - 309
publication_status: published
publisher: ACM
publist_id: '137'
quality_controlled: 0
status: public
title: Path invariants
type: conference
year: '2007'
...
---
_id: '4572'
abstract:
- lang: eng
text: We present a constraint-based algorithm for the synthesis of invariants expressed
in the combined theory of linear arithmetic and uninterpreted function symbols.
Given a set of programmer-specified invariant templates, our algorithm reduces
the invariant synthesis problem to a sequence of arithmetic constraint satisfaction
queries. Since the combination of linear arithmetic and uninterpreted functions
is a widely applied predicate domain for program verification, our algorithm provides
a powerful tool to statically and automatically reason about program correctness.
The algorithm can also be used for the synthesis of invariants over arrays and
set data structures, because satisfiability questions for the theories of sets
and arrays can be reduced to the theory of linear arithmetic with uninterpreted
functions. We have implemented our algorithm and used it to find invariants for
a low-level memory allocator written in C.
acknowledgement: This research was sponsored in part by the grants NSF-CCF-0427202
and NSF-CCF-0546170.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
citation:
ama: 'Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Invariant synthesis for
combined theories. In: Vol 4349. Springer; 2007:378-394. doi:10.1007/978-3-540-69738-1_27'
apa: 'Beyer, D., Henzinger, T. A., Majumdar, R., & Rybalchenko, A. (2007). Invariant
synthesis for combined theories (Vol. 4349, pp. 378–394). Presented at the VMCAI:
Verification, Model Checking and Abstract Interpretation, Springer. https://doi.org/10.1007/978-3-540-69738-1_27'
chicago: Beyer, Dirk, Thomas A Henzinger, Ritankar Majumdar, and Andrey Rybalchenko.
“Invariant Synthesis for Combined Theories,” 4349:378–94. Springer, 2007. https://doi.org/10.1007/978-3-540-69738-1_27.
ieee: 'D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Invariant synthesis
for combined theories,” presented at the VMCAI: Verification, Model Checking and
Abstract Interpretation, 2007, vol. 4349, pp. 378–394.'
ista: 'Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. 2007. Invariant synthesis
for combined theories. VMCAI: Verification, Model Checking and Abstract Interpretation,
LNCS, vol. 4349, 378–394.'
mla: Beyer, Dirk, et al. Invariant Synthesis for Combined Theories. Vol.
4349, Springer, 2007, pp. 378–94, doi:10.1007/978-3-540-69738-1_27.
short: D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, Springer, 2007,
pp. 378–394.
conference:
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '01'
doi: 10.1007/978-3-540-69738-1_27
extern: 1
intvolume: ' 4349'
month: '01'
page: 378 - 394
publication_status: published
publisher: Springer
publist_id: '138'
quality_controlled: 0
status: public
title: Invariant synthesis for combined theories
type: conference
volume: 4349
year: '2007'
...
---
_id: '4573'
abstract:
- lang: eng
text: In automatic software verification, we have observed a theoretical convergence
of model checking and program analysis. In practice, however, model checkers are
still mostly concerned with precision, e.g., the removal of spurious counterexamples;
for this purpose they build and refine reachability trees. Lattice-based program
analyzers, on the other hand, are primarily concerned with efficiency. We designed
an algorithm and built a tool that can be configured to perform not only a purely
tree-based or a purely lattice-based analysis, but offers many intermediate settings
that have not been evaluated before. The algorithm and tool take one or more abstract
interpreters, such as a predicate abstraction and a shape analysis, and configure
their execution and interaction using several parameters. Our experiments show
that such customization may lead to dramatic improvements in the precision-efficiency
spectrum.
acknowledgement: This research was supported in part by the grant SFU/PRG 06-3, and
by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G. Configurable software verification: Concretizing
the convergence of model checking and program analysis. In: Vol 4590. Springer;
2007:504-518. doi:10.1007/978-3-540-73368-3_51'
apa: 'Beyer, D., Henzinger, T. A., & Théoduloz, G. (2007). Configurable software
verification: Concretizing the convergence of model checking and program analysis
(Vol. 4590, pp. 504–518). Presented at the CAV: Computer Aided Verification, Springer.
https://doi.org/10.1007/978-3-540-73368-3_51'
chicago: 'Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Configurable
Software Verification: Concretizing the Convergence of Model Checking and Program
Analysis,” 4590:504–18. Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_51.'
ieee: 'D. Beyer, T. A. Henzinger, and G. Théoduloz, “Configurable software verification:
Concretizing the convergence of model checking and program analysis,” presented
at the CAV: Computer Aided Verification, 2007, vol. 4590, pp. 504–518.'
ista: 'Beyer D, Henzinger TA, Théoduloz G. 2007. Configurable software verification:
Concretizing the convergence of model checking and program analysis. CAV: Computer
Aided Verification, LNCS, vol. 4590, 504–518.'
mla: 'Beyer, Dirk, et al. Configurable Software Verification: Concretizing the
Convergence of Model Checking and Program Analysis. Vol. 4590, Springer, 2007,
pp. 504–18, doi:10.1007/978-3-540-73368-3_51.'
short: D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2007, pp. 504–518.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:09:33Z
date_published: 2007-07-02T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '02'
doi: 10.1007/978-3-540-73368-3_51
extern: 1
intvolume: ' 4590'
month: '07'
page: 504 - 518
publication_status: published
publisher: Springer
publist_id: '135'
quality_controlled: 0
status: public
title: 'Configurable software verification: Concretizing the convergence of model
checking and program analysis'
type: conference
volume: 4590
year: '2007'
...
---
_id: '4575'
abstract:
- lang: eng
text: 'We present a case study to illustrate our formalism for the specification
and verification of the method-invocation behavior of web-service applications
constructed from asynchronously interacting multi-threaded distributed components.
Our model is expressive enough to allow the representation of recursion and dynamic
thread creation, and yet permits the algorithmic analysis of the following two
questions: (1) Does a given service satisfy a safety specification? (2) Can a
given service be substituted by a another service in an arbitrary context? Our
case study is based on the Amazon.com E-Commerce Services (ECS) platform.'
acknowledgement: This research was supported in part by the NSF grant CCR-0225610
and by the Swiss National Science Foundation.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Sanjit
full_name: Seshia, Sanjit A
last_name: Seshia
citation:
ama: 'Beyer D, Chakrabarti A, Henzinger TA, Seshia S. An application of web-service
interfaces. In: IEEE; 2007:831-838. doi:10.1109/ICWS.2007.32 '
apa: 'Beyer, D., Chakrabarti, A., Henzinger, T. A., & Seshia, S. (2007). An
application of web-service interfaces (pp. 831–838). Presented at the ICWS: International
Conference on Web Service, IEEE. https://doi.org/10.1109/ICWS.2007.32 '
chicago: Beyer, Dirk, Arindam Chakrabarti, Thomas A Henzinger, and Sanjit Seshia.
“An Application of Web-Service Interfaces,” 831–38. IEEE, 2007. https://doi.org/10.1109/ICWS.2007.32 .
ieee: 'D. Beyer, A. Chakrabarti, T. A. Henzinger, and S. Seshia, “An application
of web-service interfaces,” presented at the ICWS: International Conference on
Web Service, 2007, pp. 831–838.'
ista: 'Beyer D, Chakrabarti A, Henzinger TA, Seshia S. 2007. An application of web-service
interfaces. ICWS: International Conference on Web Service, 831–838.'
mla: Beyer, Dirk, et al. An Application of Web-Service Interfaces. IEEE,
2007, pp. 831–38, doi:10.1109/ICWS.2007.32
.
short: D. Beyer, A. Chakrabarti, T.A. Henzinger, S. Seshia, in:, IEEE, 2007, pp.
831–838.
conference:
name: 'ICWS: International Conference on Web Service'
date_created: 2018-12-11T12:09:33Z
date_published: 2007-07-30T00:00:00Z
date_updated: 2021-01-12T07:59:49Z
day: '30'
doi: '10.1109/ICWS.2007.32 '
extern: 1
month: '07'
page: 831 - 838
publication_status: published
publisher: IEEE
publist_id: '134'
quality_controlled: 0
status: public
title: An application of web-service interfaces
type: conference
year: '2007'
...
---
_id: '4626'
abstract:
- lang: eng
text: 'We consider concurrent two-player games with reachability objectives. In
such games, at each round, player 1 and player 2 independently and simultaneously
choose moves, and the two choices determine the next state of the game. The objective
of player 1 is to reach a set of target states; the objective of player 2 is to
prevent this. These are zero-sum games, and the reachability objective is one
of the most basic objectives: determining the set of states from which player
1 can win the game is a fundamental problem in control theory and system verification.
There are three types of winning states, according to the degree of certainty
with which player 1 can reach the target. From type-1 states, player 1 has a deterministic
strategy to always reach the target. From type-2 states, player 1 has a randomized
strategy to reach the target with probability 1. From type-3 states, player 1
has for every real ε>0 a randomized strategy to reach the target with probability
greater than 1−ε. We show that for finite state spaces, all three sets of winning
states can be computed in polynomial time: type-1 states in linear time, and type-2
and type-3 states in quadratic time. The algorithms to compute the three sets
of winning states also enable the construction of the winning and spoiling strategies.'
author:
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. Theoretical
Computer Science. 2007;386(3):188-217. doi:10.1016/j.tcs.2007.07.008
apa: De Alfaro, L., Henzinger, T. A., & Kupferman, O. (2007). Concurrent reachability
games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2007.07.008
chicago: De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability
Games.” Theoretical Computer Science. Elsevier, 2007. https://doi.org/10.1016/j.tcs.2007.07.008.
ieee: L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability
games,” Theoretical Computer Science, vol. 386, no. 3. Elsevier, pp. 188–217,
2007.
ista: De Alfaro L, Henzinger TA, Kupferman O. 2007. Concurrent reachability games.
Theoretical Computer Science. 386(3), 188–217.
mla: De Alfaro, Luca, et al. “Concurrent Reachability Games.” Theoretical Computer
Science, vol. 386, no. 3, Elsevier, 2007, pp. 188–217, doi:10.1016/j.tcs.2007.07.008.
short: L. De Alfaro, T.A. Henzinger, O. Kupferman, Theoretical Computer Science
386 (2007) 188–217.
date_created: 2018-12-11T12:09:49Z
date_published: 2007-11-01T00:00:00Z
date_updated: 2021-01-12T08:00:37Z
day: '01'
doi: 10.1016/j.tcs.2007.07.008
extern: 1
intvolume: ' 386'
issue: '3'
month: '11'
page: 188 - 217
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '81'
quality_controlled: 0
status: public
title: Concurrent reachability games
type: journal_article
volume: 386
year: '2007'
...
---
_id: '582'
abstract:
- lang: eng
text: Using the techniques of "quantum weak-measurements" as a coherent
amplification mechanism for small signals, for the first time we have measured
the recently proposed "spin Hall effect" of light.
alternative_title:
- Optics InfoBase Conference Papers
author:
- first_name: Onur
full_name: Onur Hosten
id: 4C02D85E-F248-11E8-B48F-1D18A9856A87
last_name: Hosten
orcid: 0000-0002-2031-204X
- first_name: Paul
full_name: Kwiat, Paul G
last_name: Kwiat
citation:
ama: 'Hosten O, Kwiat P. Observing the spin hall effect of light via quantum weak
measurements. In: OSA; 2007. doi:10.1364/FIO.2007.JTuA4'
apa: 'Hosten, O., & Kwiat, P. (2007). Observing the spin hall effect of light
via quantum weak measurements. Presented at the OMD: Organic Materials and Devices
for Displays and Energy Conversion, OSA. https://doi.org/10.1364/FIO.2007.JTuA4'
chicago: Hosten, Onur, and Paul Kwiat. “Observing the Spin Hall Effect of Light
via Quantum Weak Measurements.” OSA, 2007. https://doi.org/10.1364/FIO.2007.JTuA4.
ieee: 'O. Hosten and P. Kwiat, “Observing the spin hall effect of light via quantum
weak measurements,” presented at the OMD: Organic Materials and Devices for Displays
and Energy Conversion, 2007.'
ista: 'Hosten O, Kwiat P. 2007. Observing the spin hall effect of light via quantum
weak measurements. OMD: Organic Materials and Devices for Displays and Energy
Conversion, Optics InfoBase Conference Papers, .'
mla: Hosten, Onur, and Paul Kwiat. Observing the Spin Hall Effect of Light via
Quantum Weak Measurements. OSA, 2007, doi:10.1364/FIO.2007.JTuA4.
short: O. Hosten, P. Kwiat, in:, OSA, 2007.
conference:
name: 'OMD: Organic Materials and Devices for Displays and Energy Conversion'
date_created: 2018-12-11T11:47:19Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T08:03:41Z
day: '01'
doi: 10.1364/FIO.2007.JTuA4
extern: 1
month: '01'
publication_status: published
publisher: OSA
publist_id: '7228'
quality_controlled: 0
status: public
title: Observing the spin hall effect of light via quantum weak measurements
type: conference
year: '2007'
...
---
_id: '6150'
author:
- first_name: Tina L.
full_name: Gumienny, Tina L.
last_name: Gumienny
- first_name: Lesley T.
full_name: MacNeil, Lesley T.
last_name: MacNeil
- first_name: Huang
full_name: Wang, Huang
last_name: Wang
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
- first_name: Jeffrey L.
full_name: Wrana, Jeffrey L.
last_name: Wrana
- first_name: Richard W.
full_name: Padgett, Richard W.
last_name: Padgett
citation:
ama: Gumienny TL, MacNeil LT, Wang H, de Bono M, Wrana JL, Padgett RW. Glypican
LON-2 is a conserved negative regulator of BMP-like signaling in Caenorhabditis
elegans. Current Biology. 2007;17(2):159-164. doi:10.1016/j.cub.2006.11.065
apa: Gumienny, T. L., MacNeil, L. T., Wang, H., de Bono, M., Wrana, J. L., &
Padgett, R. W. (2007). Glypican LON-2 is a conserved negative regulator of BMP-like
signaling in Caenorhabditis elegans. Current Biology. Elsevier. https://doi.org/10.1016/j.cub.2006.11.065
chicago: Gumienny, Tina L., Lesley T. MacNeil, Huang Wang, Mario de Bono, Jeffrey
L. Wrana, and Richard W. Padgett. “Glypican LON-2 Is a Conserved Negative Regulator
of BMP-like Signaling in Caenorhabditis Elegans.” Current Biology. Elsevier,
2007. https://doi.org/10.1016/j.cub.2006.11.065.
ieee: T. L. Gumienny, L. T. MacNeil, H. Wang, M. de Bono, J. L. Wrana, and R. W.
Padgett, “Glypican LON-2 is a conserved negative regulator of BMP-like signaling
in Caenorhabditis elegans,” Current Biology, vol. 17, no. 2. Elsevier,
pp. 159–164, 2007.
ista: Gumienny TL, MacNeil LT, Wang H, de Bono M, Wrana JL, Padgett RW. 2007. Glypican
LON-2 is a conserved negative regulator of BMP-like signaling in Caenorhabditis
elegans. Current Biology. 17(2), 159–164.
mla: Gumienny, Tina L., et al. “Glypican LON-2 Is a Conserved Negative Regulator
of BMP-like Signaling in Caenorhabditis Elegans.” Current Biology, vol.
17, no. 2, Elsevier, 2007, pp. 159–64, doi:10.1016/j.cub.2006.11.065.
short: T.L. Gumienny, L.T. MacNeil, H. Wang, M. de Bono, J.L. Wrana, R.W. Padgett,
Current Biology 17 (2007) 159–164.
date_created: 2019-03-21T08:44:44Z
date_published: 2007-01-23T00:00:00Z
date_updated: 2021-01-12T08:06:22Z
day: '23'
doi: 10.1016/j.cub.2006.11.065
extern: '1'
external_id:
pmid:
- '17240342'
intvolume: ' 17'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 159-164
pmid: 1
publication: Current Biology
publication_identifier:
issn:
- 0960-9822
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Glypican LON-2 is a conserved negative regulator of BMP-like signaling in Caenorhabditis
elegans
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2007'
...
---
_id: '6321'
abstract:
- lang: eng
text: These lecture notes describe the current state of affairs for Manin's conjecture
in the context of del Pezzo surfaces.
article_number: '0704.1217'
article_processing_charge: No
arxiv: 1
author:
- first_name: Timothy D
full_name: Browning, Timothy D
id: 35827D50-F248-11E8-B48F-1D18A9856A87
last_name: Browning
orcid: 0000-0002-8314-0177
citation:
ama: Browning TD. The Manin conjecture in dimension 2. arXiv.
apa: Browning, T. D. (n.d.). The Manin conjecture in dimension 2. arXiv.
chicago: Browning, Timothy D. “The Manin Conjecture in Dimension 2.” ArXiv,
n.d.
ieee: T. D. Browning, “The Manin conjecture in dimension 2,” arXiv. .
ista: Browning TD. The Manin conjecture in dimension 2. arXiv, 0704.1217.
mla: Browning, Timothy D. “The Manin Conjecture in Dimension 2.” ArXiv, 0704.1217.
short: T.D. Browning, ArXiv (n.d.).
date_created: 2019-04-16T14:17:50Z
date_published: 2007-04-10T00:00:00Z
date_updated: 2021-01-12T08:07:04Z
day: '10'
extern: '1'
external_id:
arxiv:
- '0704.1217'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/0704.1217
month: '04'
oa: 1
oa_version: Preprint
publication: arXiv
publication_status: submitted
status: public
title: The Manin conjecture in dimension 2
type: preprint
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2007'
...