| 1. |
- Aartsen, M. G., et al.
(författare)
-
Very high-energy gamma-ray follow-up program using neutrino triggers from IceCube
- 2016
-
Ingår i: Journal of Instrumentation. - 1748-0221. ; 11
-
Tidskriftsartikel (refereegranskat)abstract
- We describe and report the status of a neutrino-triggered program in IceCube that generates real-time alerts for gamma-ray follow-up observations by atmospheric-Cherenkov telescopes (MAGIC and VERITAS). While IceCube is capable of monitoring the whole sky continuously, high-energy gamma-ray telescopes have restricted fields of view and in general are unlikely to be observing a potential neutrino-flaring source at the time such neutrinos are recorded. The use of neutrino-triggered alerts thus aims at increasing the availability of simultaneous multi-messenger data during potential neutrino flaring activity, which can increase the discovery potential and constrain the phenomenological interpretation of the high-energy emission of selected source classes (e. g. blazars). The requirements of a fast and stable online analysis of potential neutrino signals and its operation are presented, along with first results of the program operating between 14 March 2012 and 31 December 2015.
|
|
| 2. |
- Salami, B., et al.
(författare)
-
LEGaTO: Low-Energy, Secure, and Resilient Toolset for Heterogeneous Computing
- 2020
-
Ingår i: PROCEEDINGS OF THE 2020 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE 2020). - 1530-1591. - 9783981926347 ; , s. 169-174
-
Konferensbidrag (refereegranskat)abstract
- The LEGaTO project leverages task-based programming models to provide a software ecosystem for Made in-Europe heterogeneous hardware composed of CPUs, GPUs, FPGAs and dataflow engines. The aim is to attain one order of magnitude energy savings from the edge to the converged cloud/HPC, balanced with the security and resilience challenges. LEGaTO is an ongoing three-year EU H2020 project started in December 2017.
|
|
| 3. |
- Revelli, A., et al.
(författare)
-
Spin-orbit entangled j=1/2 moments in Ba2CeIrO6 : A frustrated fcc quantum magnet
- 2019
-
Ingår i: Physical Review B. - 2469-9950 .- 2469-9969. ; 100:8
-
Tidskriftsartikel (refereegranskat)abstract
- We establish the double perovskite Ba2CeIrO6 as a nearly ideal model system for j = 1/2 moments, with resonant inelastic x-ray scattering indicating that the ideal j = 1/2 state contributes by more than 99% to the ground-state wave function. The local j = 1/2 moments form an fcc lattice and are found to order antiferromagnetically at T-N = 14 K, more than an order of magnitude below the Curie-Weiss temperature. Model calculations show that the geometric frustration of the fcc Heisenberg antiferromagnet is further enhanced by a next-nearest neighbor exchange, and a significant size of the latter is indicated by ab initio theory. Our theoretical analysis shows that magnetic order is driven by a bond-directional Kitaev exchange and by local distortions via a strong magnetoelastic effect. Both, the suppression of frustration by Kitaev exchange and the strong magnetoelastic effect are typically not expected for j = 1/2 compounds making Ba2CeIrO6 a riveting example for the rich physics of spin-orbit entangled Mott insulators.
|
|
| 4. |
- Kienzle, J., et al.
(författare)
-
Toward model-driven sustainability evaluation
- 2020
-
Ingår i: Communications of the ACM. - : Association for Computing Machinery (ACM). - 0001-0782 .- 1557-7317. ; 63:3, s. 80-91
-
Forskningsöversikt (refereegranskat)abstract
- Exploring the vision of a model-based framework that may enable broader engagement with and informed decision making about sustainability issues.
|
|
| 5. |
- Becker, Heiko, et al.
(författare)
-
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
- 2018
-
Ingår i: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018. ; , s. 215-224
-
Konferensbidrag (refereegranskat)abstract
- Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the discrepancy between continuous reals and discrete finite-precision values, automated static analysis tools are highly valuable to estimate roundoff errors. The results, however, are only as correct as the implementations of the static analysis tools. This paper presents a formally verified and modular tool which fully automatically checks the correctness of finite-precision roundoff error bounds encoded in a certificate. We present implementations of certificate generation and checking for both Coq and HOL4 and evaluate it on a number of examples from the literature. The experiments use both in-logic evaluation of Coq and HOL4, and execution of extracted code outside of the logics: we benchmark Coq extracted unverified OCaml code and a CakeML-generated verified binary.
|
|
| 6. |
- Becker, Heiko, et al.
(författare)
-
Verified Compilation and Optimization of Floating-Point Programs in CakeML
- 2022
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl - Leibniz-Zentrum für Informatik. - 1868-8969. ; 222
-
Konferensbidrag (refereegranskat)abstract
- Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the “fast-math-style” optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake's end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
|
|
| 7. |
- Santambrogio, M. D., et al.
(författare)
-
Smart technologies for effective reconfiguration: The FASTER approach
- 2012
-
Ingår i: ReCoSoC 2012 - 7th International Workshop on Reconfigurable and Communication-Centric Systems-on-Chip, Proceedings. - 9781467325721
-
Konferensbidrag (refereegranskat)abstract
- Current and future computing systems increasingly require that their functionality stays flexible after the system is operational, in order to cope with changing user requirements and improvements in system features, i.e. changing protocols and data-coding standards, evolving demands for support of different user applications, and newly emerging applications in communication, computing and consumer electronics. Therefore, extending the functionality and the lifetime of products requires the addition of new functionality to track and satisfy the customers needs and market and technology trends. Many contemporary products along with the software part incorporate hardware accelerators for reasons of performance and power efficiency. While adaptivity of software is straightforward, adaptation of the hardware to changing requirements constitutes a challenging problem requiring delicate solutions. The FASTER (Facilitating Analysis and Synthesis Technologies for Effective Reconfiguration) project aims at introducing a complete methodology to allow designers to easily implement a system specification on a platform which includes a general purpose processor combined with multiple accelerators running on an FPGA, taking as input a high-level description and fully exploiting, both at design time and at run time, the capabilities of partial dynamic reconfiguration. The goal is that for selected application domains, the FASTER toolchain will be able to reduce the design and verification time of complex reconfigurable systems providing additional novel verification features that are not available in existing tool flows.
|
|
| 8. |
- Schweiker, Marcel, et al.
(författare)
-
Evaluating assumptions of scales for subjective assessment of thermal environments – Do laypersons perceive them the way, we researchers believe?
- 2020
-
Ingår i: Energy and Buildings. - : Elsevier BV. - 0378-7788. ; 211
-
Tidskriftsartikel (refereegranskat)abstract
- People's subjective response to any thermal environment is commonly investigated by using rating scales describing the degree of thermal sensation, comfort, and acceptability. Subsequent analyses of results collected in this way rely on the assumption that specific distances between verbal anchors placed on the scale exist and that relationships between verbal anchors from different dimensions that are assessed (e.g. thermal sensation and comfort) do not change. Another inherent assumption is that such scales are independent of the context in which they are used (climate zone, season, etc.). Despite their use worldwide, there is indication that contextual differences influence the way the scales are perceived and therefore question the reliability of the scales’ interpretation. To address this issue, a large international collaborative questionnaire study was conducted in 26 countries, using 21 different languages, which led to a dataset of 8225 questionnaires. Results, analysed by means of robust statistical techniques, revealed that only a subset of the responses are in accordance with the mentioned assumptions. Significant differences appeared between groups of participants in their perception of the scales, both in relation to distances of the anchors and relationships between scales. It was also found that respondents’ interpretations of scales changed with contextual factors, such as climate, season, and language. These findings highlight the need to carefully consider context-dependent factors in interpreting and reporting results from thermal comfort studies or post-occupancy evaluations, as well as to revisit the use of rating scales and the analysis methods used in thermal comfort studies to improve their reliability.
|
|
| 9. |
- Singer, A., et al.
(författare)
-
Intensity Interferometry of Single X-Ray Pulses from a Synchrotron Storage Ring
- 2014
-
Ingår i: Physical Review Letters. - 0031-9007 .- 1079-7114. ; 113:6, s. Art. no. 064801-
-
Tidskriftsartikel (refereegranskat)abstract
- We report on measurements of second-order intensity correlations at the high-brilliance storage ring PETRA III using a prototype of the newly developed adaptive gain integrating pixel detector. The detector records individual synchrotron radiation pulses with an x-ray photon energy of 14.4 keV and repetition rate of about 5 MHz. The second-order intensity correlation function is measured simultaneously at different spatial separations, which allows us to determine the transverse coherence length at these x-ray energies. The measured values are in a good agreement with theoretical simulations based on the Gaussian Schell model.
|
|
| 10. |
- Ardo, Shane, et al.
(författare)
-
Pathways to electrochemical solar-hydrogen technologies
- 2018
-
Ingår i: Energy & Environmental Science. - : Royal Society of Chemistry. - 1754-5692 .- 1754-5706. ; 11:10, s. 2768-2783
-
Forskningsöversikt (refereegranskat)abstract
- Solar-powered electrochemical production of hydrogen through water electrolysis is an active and important research endeavor. However, technologies and roadmaps for implementation of this process do not exist. In this perspective paper, we describe potential pathways for solar-hydrogen technologies into the marketplace in the form of photoelectrochemical or photovoltaic-driven electrolysis devices and systems. We detail technical approaches for device and system architectures, economic drivers, societal perceptions, political impacts, technological challenges, and research opportunities. Implementation scenarios are broken down into short-term and long-term markets, and a specific technology roadmap is defined. In the short term, the only plausible economical option will be photovoltaic-driven electrolysis systems for niche applications. In the long term, electrochemical solar-hydrogen technologies could be deployed more broadly in energy markets but will require advances in the technology, significant cost reductions, and/ or policy changes. Ultimately, a transition to a society that significantly relies on solar-hydrogen technologies will benefit from continued creativity and influence from the scientific community.
|
|
