• The flux of very high-energy neutrinos produced in our Galaxy by the interaction of accelerated cosmic rays with the interstellar medium is not yet determined. The characterization of this flux will shed light on Galactic accelerator features, gas distribution morphology and Galactic cosmic ray transport. The central Galactic plane can be the site of an enhanced neutrino production, thus leading to anisotropies in the extraterrestrial neutrino signal as measured by the IceCube Collaboration. The ANTARES neutrino telescope, located in the Mediterranean Sea, offers a favourable view on this part of the sky, thereby allowing for a contribution to the determination of this flux. The expected diffuse Galactic neutrino emission can be obtained linking a model of generation and propagation of cosmic rays with the morphology of the gas distribution in the Milky Way. In this paper, the so-called "Gamma model" introduced recently to explain the high-energy gamma ray diffuse Galactic emission, is assumed as reference. The neutrino flux predicted by the "Gamma model" depends of the assumed primary cosmic ray spectrum cut-off. Considering a radially-dependent diffusion coefficient, this proposed scenario is able to account for the local cosmic ray measurements, as well as for the Galactic gamma ray observations. Nine years of ANTARES data are used in this work to search for a possible Galactic contribution according to this scenario. All flavour neutrino interactions are considered. No excess of events is observed and an upper limit is set on the neutrino flux of $1.1$ ($1.2$) times the prediction of the "Gamma model" assuming the primary cosmic ray spectrum cut-off at 5 (50) PeV. This limit excludes the diffuse Galactic neutrino emission as the major cause of the "spectral anomaly" between the two hemispheres measured by IceCube.
• ### Inferring Types for Parallel Programs(1704.03096)

April 11, 2017 cs.LO, cs.PL
The Message Passing Interface (MPI) framework is widely used in implementing imperative pro- grams that exhibit a high degree of parallelism. The PARTYPES approach proposes a behavioural type discipline for MPI-like programs in which a type describes the communication protocol followed by the entire program. Well-typed programs are guaranteed to be exempt from deadlocks. In this paper we describe a type inference algorithm for a subset of the original system; the algorithm allows to statically extract a type for an MPI program from its source code.
• ### Deductive Verification of Parallel Programs Using Why3(1508.04856)

Aug. 20, 2015 cs.PL, cs.DC
The Message Passing Interface specification (MPI) defines a portable message-passing API used to program parallel computers. MPI programs manifest a number of challenges on what concerns correctness: sent and expected values in communications may not match, resulting in incorrect computations possibly leading to crashes; and programs may deadlock resulting in wasted resources. Existing tools are not completely satisfactory: model-checking does not scale with the number of processes; testing techniques wastes resources and are highly dependent on the quality of the test set. As an alternative, we present a prototype for a type-based approach to programming and verifying MPI like programs against protocols. Protocols are written in a dependent type language designed so as to capture the most common primitives in MPI, incorporating, in addition, a form of primitive recursion and collective choice. Protocols are then translated into Why3, a deductive software verification tool. Source code, in turn, is written in WhyML, the language of the Why3 platform, and checked against the protocol. Programs that pass verification are guaranteed to be communication safe and free from deadlocks. We verified several parallel programs from textbooks using our approach, and report on the outcome.
• ### Deductive Verification of Parallel Programs Using Why3(1508.04856)

Aug. 20, 2015 cs.PL, cs.DC
The Message Passing Interface specification (MPI) defines a portable message-passing API used to program parallel computers. MPI programs manifest a number of challenges on what concerns correctness: sent and expected values in communications may not match, resulting in incorrect computations possibly leading to crashes; and programs may deadlock resulting in wasted resources. Existing tools are not completely satisfactory: model-checking does not scale with the number of processes; testing techniques wastes resources and are highly dependent on the quality of the test set. As an alternative, we present a prototype for a type-based approach to programming and verifying MPI like programs against protocols. Protocols are written in a dependent type language designed so as to capture the most common primitives in MPI, incorporating, in addition, a form of primitive recursion and collective choice. Protocols are then translated into Why3, a deductive software verification tool. Source code, in turn, is written in WhyML, the language of the Why3 platform, and checked against the protocol. Programs that pass verification are guaranteed to be communication safe and free from deadlocks. We verified several parallel programs from textbooks using our approach, and report on the outcome.
• ### Deductive Verification of Parallel Programs Using Why3(1508.04856)

Aug. 20, 2015 cs.PL, cs.DC
The Message Passing Interface specification (MPI) defines a portable message-passing API used to program parallel computers. MPI programs manifest a number of challenges on what concerns correctness: sent and expected values in communications may not match, resulting in incorrect computations possibly leading to crashes; and programs may deadlock resulting in wasted resources. Existing tools are not completely satisfactory: model-checking does not scale with the number of processes; testing techniques wastes resources and are highly dependent on the quality of the test set. As an alternative, we present a prototype for a type-based approach to programming and verifying MPI like programs against protocols. Protocols are written in a dependent type language designed so as to capture the most common primitives in MPI, incorporating, in addition, a form of primitive recursion and collective choice. Protocols are then translated into Why3, a deductive software verification tool. Source code, in turn, is written in WhyML, the language of the Why3 platform, and checked against the protocol. Programs that pass verification are guaranteed to be communication safe and free from deadlocks. We verified several parallel programs from textbooks using our approach, and report on the outcome.
• The third generation of the Sloan Digital Sky Survey (SDSS-III) took data from 2008 to 2014 using the original SDSS wide-field imager, the original and an upgraded multi-object fiber-fed optical spectrograph, a new near-infrared high-resolution spectrograph, and a novel optical interferometer. All the data from SDSS-III are now made public. In particular, this paper describes Data Release 11 (DR11) including all data acquired through 2013 July, and Data Release 12 (DR12) adding data acquired through 2014 July (including all data included in previous data releases), marking the end of SDSS-III observing. Relative to our previous public release (DR10), DR12 adds one million new spectra of galaxies and quasars from the Baryon Oscillation Spectroscopic Survey (BOSS) over an additional 3000 sq. deg of sky, more than triples the number of H-band spectra of stars as part of the Apache Point Observatory (APO) Galactic Evolution Experiment (APOGEE), and includes repeated accurate radial velocity measurements of 5500 stars from the Multi-Object APO Radial Velocity Exoplanet Large-area Survey (MARVELS). The APOGEE outputs now include measured abundances of 15 different elements for each star. In total, SDSS-III added 2350 sq. deg of ugriz imaging; 155,520 spectra of 138,099 stars as part of the Sloan Exploration of Galactic Understanding and Evolution 2 (SEGUE-2) survey; 2,497,484 BOSS spectra of 1,372,737 galaxies, 294,512 quasars, and 247,216 stars over 9376 sq. deg; 618,080 APOGEE spectra of 156,593 stars; and 197,040 MARVELS spectra of 5,513 stars. Since its first light in 1998, SDSS has imaged over 1/3 of the Celestial sphere in five bands and obtained over five million astronomical spectra.
• ### Planet-vortex interaction:How a vortex can shepherd a planetary embryo(1410.0132)

Oct. 1, 2014 astro-ph.EP
Context: Anticyclonic vortices are considered as a favourable places for trapping dust and forming planetary embryos. On the other hand, they are massive blobs that can interact gravitationally with the planets in the disc. Aims: We aim to study how a vortex interacts gravitationally with a planet which migrates toward it or a planet which is created inside the vortex. Methods: We performed hydrodynamical simulations of a viscous locally isothermal disc using GFARGO and FARGO-ADSG. We set a stationary Gaussian pressure bump in the disc in a way that RWI is triggered. After a large vortex is established, we implanted a low mass planet in the outer disc or inside the vortex and allowed it to migrate. We also examined the effect of vortex strength on the planet migration and checked the validity of the final result in the presence of self-gravity. Results: We noticed regardless of the planet's initial position, the planet is finally locked to the vortex or its migration is stopped in a farther orbital distance in case of a stronger vortex. For the model with the weaker vortex, we studied the effect of different parameters such as background viscosity, background surface density, mass of the planet and different planet positions. In these models, while the trapping time and locking angle of the planet vary for different parameters, the main result, which is the planet-vortex locking, remains valid. We discovered that even a planet with a mass less than 5 * 10^{-7} M_{\star} comes out from the vortex and is locked to it at the same orbital distance. For a stronger vortex, both in non-self-gravitated and self-gravitating models, the planet migration is stopped far away from the radial position of the vortex. This effect can make the vortices a suitable place for continual planet formation under the condition that they save their shape during the planetary growth.
• ### Searching for a quantum critical point in YbCu5-xAux(1403.6004)

March 24, 2014 cond-mat.str-el
Structural, magnetic, transport and thermal properties of YbCu5-xAux alloys with Au concentration between the limit of structural stability of AuBe5 type at x = 0.4 up to x = 0.7 are reported. The outstanding features of this system are: i) the constant and record high values of Cm /T 7J/molK^2 below a characteristic temperature T*, ranging between 150 mK and 350 mK. ii) A power law thermal dependence dependence Cm/T(T>T*)=A/T^q, with q = 1.3 +/- 0.1, and iii) an arising incoherent electronic scattering observed in the resistivity at T < 1K for x < 0.6 despite the fact that Yb magnetic atoms are placed in a lattice. Magnetic frustration, originated in the tetrahedral distribution of Yb atoms, appears as the responsible of the exotic behavior of this system.
• ### On the eclipsing cataclysmic variable star HBHA 4705-03(1306.4462)

June 19, 2013 astro-ph.SR
We present observations and analysis of a new eclipsing binary HBHA 4705-03. Using decomposition of the light curve into accretion disk and hot spot components, we estimated photometrically the mass ratio of the studied system to be q=0.62 +-0.07. Other fundamental parameters was found with modeling. This approach gave: white dwarf mass M_1 = (0.8 +- 0.2) M_sun, secondary mass M_2=(0.497 +- 0.05) M_sun, orbital radius a=1.418 R_sun, orbital inclination i = (81.58 +- 0.5) deg, accretion disk radius r_d/a = 0.366 +- 0.002, and accretion rate dot{M} = (2.5 +- 2) * 10^{18}[g/s], (3*10^{-8} [M_sun/yr]). Power spectrum analysis revealed ambiguous low-period Quasi Periodic Oscillations centered at the frequencies f_{1}=0.00076 Hz, f_2=0.00048 Hz and f_3=0.00036 Hz. The B-V=0.04 [mag] color corresponds to a dwarf novae during an outburst. The examined light curves suggest that HBHA 4705-03 is a nova-like variable star.
• ### Asymmetric transition disks: Vorticity or eccentricity?(1304.1736)

April 5, 2013 astro-ph.EP
Context. Transition disks typically appear in resolved millimeter observations as giant dust rings surrounding their young host stars. More accurate observations with ALMA have shown several of these rings to be in fact asymmetric: they have lopsided shapes. It has been speculated that these rings act as dust traps, which would make them important laboratories for studying planet formation. It has been shown that an elongated giant vortex produced in a disk with a strong viscosity jump strikingly resembles the observed asymmetric rings. Aims. We aim to study a similar behavior for a disk in which a giant planet is embedded. However, a giant planet can induce two kinds of asymmetries: (1) a giant vortex, and (2) an eccentric disk. We studied under which conditions each of these can appear, and how one can observationally distinguish between them. This is important because only a vortex can trap particles both radially and azimuthally, while the eccentric ring can only trap particles in radial direction. Methods. We used the FARGO code to conduct the hydro-simulations. We set up a disk with an embedded giant planet and took a radial grid spanning from 0.1 to 7 times the planet semi-major axis. We ran the simulations with various viscosity values and planet masses for 1000 planet orbits to allow a fully developed vortex or disk eccentricity. Afterwards, we compared the dust distribution in a vortex-holding disk with an eccentric disk using dust simulations. Results. We find that vorticity and eccentricity are distinguishable by looking at the azimuthal contrast of the dust density. While vortices, as particle traps, produce very pronounced azimuthal asymmetries, eccentric features are not able to accumulate millimeter dust particles in azimuthal direction, and therefore the asymmetries are expected to be modest.
• ### State selective differential cross sections for single and double electron capture in $He\sp{1,2+}-He$ and $p-He$ collisons(0711.4920)

Nov. 30, 2007 physics.atom-ph
Using the COLTRIMStechnique, scattering angle differential cross sections for single and double electron capture in collisions of protons and $He\sp{1,2+}$ projectiles with helium atoms for incident energies of $60-630 keV/u$ are measured. We also report new theoretical results obtained by means of four-body one-channel distorted wave models (CDW-BFS, CDW-BIS and BDW), and find mixed agreement with the measured data.
• ### Vibrational Enhancement of the Effective Donor - Acceptor Coupling(cond-mat/0505761)

The paper deals with a simple three sites model for charge transfer phenomena in an one-dimensional donor (D) - bridge (B) - acceptor (A) system coupled with vibrational dynamics of the B site. It is found that in a certain range of parameters the vibrational coupling leads to an enhancement of the effective donor - acceptor electronic coupling as a result of the formation of the polaron on the B site. This enhancement of the charge transfer efficiency is maximum at the resonance, where the effective energy of the fluctuating B site coincides with the donor (acceptor) energy.