| 1. |
- Abellán, C., et al.
(författare)
-
Challenging Local Realism with Human Choices
- 2018
-
Ingår i: Nature. - : Nature Publishing Group. - 0028-0836 .- 1476-4687. ; 557, s. 212-216
-
Tidskriftsartikel (refereegranskat)abstract
- A Bell test is a randomized trial that compares experimental observations against the philosophical worldview of local realism , in which the properties of the physical world are independent of our observation of them and no signal travels faster than light. A Bell test requires spatially distributed entanglement, fast and high-efficiency detection and unpredictable measurement settings. Although technology can satisfy the first two of these requirements, the use of physical devices to choose settings in a Bell test involves making assumptions about the physics that one aims to test. Bell himself noted this weakness in using physical setting choices and argued that human 'free will' could be used rigorously to ensure unpredictability in Bell tests. Here we report a set of local-realism tests using human choices, which avoids assumptions about predictability in physics. We recruited about 100,000 human participants to play an online video game that incentivizes fast, sustained input of unpredictable selections and illustrates Bell-test methodology. The participants generated 97,347,490 binary choices, which were directed via a scalable web platform to 12 laboratories on five continents, where 13 experiments tested local realism using photons, single atoms, atomic ensembles and superconducting devices. Over a 12-hour period on 30 November 2016, participants worldwide provided a sustained data flow of over 1,000 bits per second to the experiments, which used different human-generated data to choose each measurement setting. The observed correlations strongly contradict local realism and other realistic positions in bi-partite and tri-partite 12 scenarios. Project outcomes include closing the 'freedom-of-choice loophole' (the possibility that the setting choices are influenced by 'hidden variables' to correlate with the particle properties), the utilization of video-game methods for rapid collection of human-generated randomness, and the use of networking techniques for global participation in experimental science.
|
|
| 2. |
- Nelson, G., et al.
(författare)
-
QUAREP-LiMi: A community-driven initiative to establish guidelines for quality assessment and reproducibility for instruments and images in light microscopy
- 2021
-
Ingår i: Journal of Microscopy. - : Wiley. - 0022-2720 .- 1365-2818. ; 284:1, s. 56-73
-
Tidskriftsartikel (refereegranskat)abstract
- A modern day light microscope has evolved from a tool devoted to making primarily empirical observations to what is now a sophisticated , quantitative device that is an integral part of both physical and life science research. Nowadays, microscopes are found in nearly every experimental laboratory. However, despite their prevalent use in capturing and quantifying scientific phenomena, neither a thorough understanding of the principles underlying quantitative imaging techniques nor appropriate knowledge of how to calibrate, operate and maintain microscopes can be taken for granted. This is clearly demonstrated by the well-documented and widespread difficulties that are routinely encountered in evaluating acquired data and reproducing scientific experiments. Indeed, studies have shown that more than 70% of researchers have tried and failed to repeat another scientist's experiments, while more than half have even failed to reproduce their own experiments. One factor behind the reproducibility crisis of experiments published in scientific journals is the frequent underreporting of imaging methods caused by a lack of awareness and/or a lack of knowledge of the applied technique. Whereas quality control procedures for some methods used in biomedical research, such as genomics (e.g. DNA sequencing, RNA-seq) or cytometry, have been introduced (e.g. ENCODE), this issue has not been tackled for optical microscopy instrumentation and images. Although many calibration standards and protocols have been published, there is a lack of awareness and agreement on common standards and guidelines for quality assessment and reproducibility. In April 2020, the QUality Assessment and REProducibility for instruments and images in Light Microscopy (QUAREP-LiMi) initiative was formed. This initiative comprises imaging scientists from academia and industry who share a common interest in achieving a better understanding of the performance and limitations of microscopes and improved quality control (QC) in light microscopy. The ultimate goal of the QUAREP-LiMi initiative is to establish a set of common QC standards, guidelines, metadata models and tools, including detailed protocols, with the ultimate aim of improving reproducible advances in scientific research. This White Paper (1) summarizes the major obstacles identified in the field that motivated the launch of the QUAREP-LiMi initiative; (2) identifies the urgent need to address these obstacles in a grassroots manner, through a community of stakeholders including, researchers, imaging scientists, bioimage analysts, bioimage informatics developers, corporate partners, funding agencies, standards organizations, scientific publishers and observers of such; (3) outlines the current actions of the QUAREP-LiMi initiative and (4) proposes future steps that can be taken to improve the dissemination and acceptance of the proposed guidelines to manage QC. To summarize, the principal goal of the QUAREP-LiMi initiative is to improve the overall quality and reproducibility of light microscope image data by introducing broadly accepted standard practices and accurately captured image data metrics.
|
|
| 3. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Deductive Software Verification - The KeY Book
- 2016
-
Bok (övrigt vetenskapligt/konstnärligt)abstract
- Static analysis of software with deductive methods is a highly dynamic field of research on the verge of becoming a mainstream technology in software engineering. It consists of a large portfolio of - mostly fully automated - analyses: formal verification, test generation, security analysis, visualization, and debugging. All of them are realized in the state-of-art deductive verification framework KeY. This book is the definitive guide to KeY that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind KeY for active researchers who want to understand it in depth or use it in their own work. But the book also features fully self-contained chapters on the Java Modeling Language and on Using KeY that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M.Sc. level and beyond). The KeY framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
KeY: A Formal Method for Object-Oriented Systems
- 2007
-
Ingår i: Lecture Notes in Computer Science, Proc. 9th IFIP Intl. Conf. on Formal Methods for Open Object-based Distributed Systems (FMOODS), eds. M.Bonsangue and E. B. Johnsen. ; 4468, s. 32-43
-
Konferensbidrag (refereegranskat)
|
|
| 5. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
The KeY platform for verification and analysis of java programs
- 2014
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 8471:8471, s. 55-71
-
Konferensbidrag (refereegranskat)abstract
- The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flowsecurity, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Verifying Object-Oriented Programs with KeY: A Tutorial
- 2007
-
Ingår i: Formal Methods for Components and Objects, eds. de Boer, Bonsangue, Graf, de Roever. - 9783540747918 ; LNCS 4709
-
Konferensbidrag (refereegranskat)abstract
- This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers.
|
|
| 7. |
- Beckert, Bernhard, et al.
(författare)
-
The KeY system 1.0 (Deduction Component)
- 2007
-
Ingår i: Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, Springer-Verlag, LNCS. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540735946 ; 4603, s. 379-384
-
Konferensbidrag (refereegranskat)
|
|
| 8. |
- Joshi, Siddarth Koduru, et al.
(författare)
-
Space QUEST mission proposal : experimentally testing decoherence due to gravity
- 2018
-
Ingår i: New Journal of Physics. - : IOP Publishing. - 1367-2630. ; 20
-
Tidskriftsartikel (refereegranskat)abstract
- Models of quantum systems on curved space-times lack sufficient experimental verification. Some speculative theories suggest that quantum correlations, such as entanglement, may exhibit different behavior to purely classical correlations in curved space. By measuring this effect or lack thereof, we can test the hypotheses behind several such models. For instance, as predicted by Ralph et al [5] and Ralph and Pienaar [1], a bipartite entangled system could decohere if each particle traversed through a different gravitational field gradient. We propose to study this effect in a ground to space uplink scenario. We extend the above theoretical predictions of Ralph and coworkers and discuss the scientific consequences of detecting/failing to detect the predicted gravitational decoherence. We present a detailed mission design of the European Space Agency's Space QUEST (Space-Quantum Entanglement Space Test) mission, and study the feasibility of the mission scheme.
|
|
