Showing 1–23 of 23 results for author: Nagashima, Y

Template-Based Conjecturing for Automated Induction in Isabelle/HOL

Authors: Yutaka Nagashima, Zi** Xu, Ningli Wang, Daniel Sebastian Goc, James Bang

Abstract: Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluatio… ▽ More Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 40 percentage point improvement of success rates for problems at intermediate difficulty level. △ Less

Submitted 19 January, 2023; v1 submitted 20 November, 2022; originally announced December 2022.

Comments: To appear at Fundamentals of Software engineering 2023 (http://fsen.ir/2023/)

Genetic Algorithm for Program Synthesis

Authors: Yutaka Nagashima

Abstract: A deductive program synthesis tool takes a specification as input and derives a program that satisfies the specification. The drawback of this approach is that search spaces for such correct programs tend to be enormous, making it difficult to derive correct programs within a realistic timeout. To speed up such program derivation, we improve the search strategy of a deductive program synthesis too… ▽ More A deductive program synthesis tool takes a specification as input and derives a program that satisfies the specification. The drawback of this approach is that search spaces for such correct programs tend to be enormous, making it difficult to derive correct programs within a realistic timeout. To speed up such program derivation, we improve the search strategy of a deductive program synthesis tool, SuSLik, using evolutionary computation. Our cross-validation shows that the improvement brought by evolutionary computation generalises to unforeseen problems. △ Less

Submitted 19 January, 2023; v1 submitted 21 November, 2022; originally announced November 2022.

Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

Authors: Yutaka Nagashima

Abstract: Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users' knowledge on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct… ▽ More Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users' knowledge on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the SeLFiE interpreter judges whether the arguments are plausible for that problem according to the heuristic by examining both the syntactic structure of the problem and definitions of the relevant constants. To examine the intricate interaction between syntactic analysis and analysis of constant definitions, we introduce definitional quantifiers. For evaluation we build an automatic induction prover using SeLFiE. Our evaluation based on 347 inductive problems shows that our new prover achieves 1.4 x 10^3% improvement over the corresponding baseline prover for 1.0 second of timeout and the median value of speedup is 4.48x. △ Less

Submitted 20 May, 2022; v1 submitted 19 October, 2020; originally announced October 2020.

Comments: This is the preprint of our paper accepted at Tests and Proofs 2022. arXiv admin note: substantial text overlap with arXiv:2009.09215

Faster Smarter Induction in Isabelle/HOL

Authors: Yutaka Nagashima

Abstract: Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed sem_ind. Given inductive problem, sem_ind recommends what arguments to pass to the induct method. To improve the accuracy of sem_ind, we introduced definitional quantifiers, a new… ▽ More Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed sem_ind. Given inductive problem, sem_ind recommends what arguments to pass to the induct method. To improve the accuracy of sem_ind, we introduced definitional quantifiers, a new kind of quantifiers that allow us to investigate not only the syntactic structures of inductive problems but also the definitions of relevant constants in a domain-agnostic style. Our evaluation shows that compared to its predecessor sem_ind improves the accuracy of recommendation from 20.1% to 38.2% for the most promising candidates within 5.0 seconds of timeout while decreasing the median value of execution time from 2.79 seconds to 1.06 seconds. △ Less

Submitted 9 May, 2021; v1 submitted 19 September, 2020; originally announced September 2020.

Comments: This is the preprint of our paper of the same title, which is accepted to IJCAI2021. For the formal proceeding, please refer to the IJCAI2021 website

Towards United Reasoning for Automatic Induction in Isabelle/HOL

Authors: Yutaka Nagashima

Abstract: Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a novel approach to further automating inductive theorem proving. Upon success, united reasoning takes the best of three schools of reasoning: deductive reasoning, indu… ▽ More Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a novel approach to further automating inductive theorem proving. Upon success, united reasoning takes the best of three schools of reasoning: deductive reasoning, inductive reasoning, and inductive reasoning, to prove difficult inductive problems automatically. △ Less

Submitted 25 May, 2020; originally announced May 2020.

Comments: This is the pre-print of our short-paper accepted at the 34th Annual Conference of the Japanese Society for Artificial Intelligence, 2020 (https://www.ai-gakkai.or.jp/jsai2020/en)

Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)

Authors: Yutaka Nagashima

Abstract: Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data des… ▽ More Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic. △ Less

Submitted 26 May, 2020; v1 submitted 21 April, 2020; originally announced April 2020.

Comments: This is the preprint of our short paper accepted at the 13th Conference on Intelligent Computer Mathematics (CICM 2020)

Smart Induction for Isabelle/HOL (System Description)

Authors: Yutaka Nagashima

Abstract: Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct lists promising arguments for the induct tactic without relying on a search. Our evaluation demonstrat… ▽ More Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct lists promising arguments for the induct tactic without relying on a search. Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains. △ Less

Submitted 27 January, 2020; originally announced January 2020.

Comments: Under submission at IJCAR2020 as a System Description

Enhanced spectral resolution for broadband coherent anti-Stokes Raman spectroscopy

Authors: Faris Sinjab, Kazuki Hashimoto, Xuanqiang Zhao, Yu Nagashima, Takuro Ideguchi

Abstract: The spectral resolution of broadband Fourier-transform coherent anti-Stokes Raman spectroscopy is limited by the maximum optical path length difference that can be scanned within a short time in an interferometer. However, alternatives to the Fourier-transform exist which can bypass this limitation with certain assumptions. We apply one such approach to broadband coherent Raman spectroscopy using… ▽ More The spectral resolution of broadband Fourier-transform coherent anti-Stokes Raman spectroscopy is limited by the maximum optical path length difference that can be scanned within a short time in an interferometer. However, alternatives to the Fourier-transform exist which can bypass this limitation with certain assumptions. We apply one such approach to broadband coherent Raman spectroscopy using interferometers with short delay line (low Fourier spectral resolution) and large delay line (high Fourier spectral resolution). With this method, we demonstrate broadband coherent Raman spectroscopy of closely spaced vibrational bands is possible using a short delay line interferometer, with superior spectral resolution to the longer delay line instrument. We discuss how this approach may be particularly useful for more complex Raman spectra, such as those measured from biological samples. △ Less

Submitted 17 January, 2020; originally announced January 2020.

Label-free biochemical quantitative phase imaging with mid-infrared photothermal effect

Authors: Miu Tamamitsu, Keiichiro Toda, Hiroyuki Shimada, Takaaki Honda, Masaharu Takarada, Kohki Okabe, Yu Nagashima, Ryoichi Horisaki, Takuro Ideguchi

Abstract: Label-free optical imaging is valuable in biology and medicine with its non-destructive property and reduced optical and chemical damages. Quantitative phase (QPI) and molecular vibrational imaging (MVI) are the two most successful label-free methods, providing morphology and biochemistry, respectively, that have pioneered numerous applications along their independent technological maturity over t… ▽ More Label-free optical imaging is valuable in biology and medicine with its non-destructive property and reduced optical and chemical damages. Quantitative phase (QPI) and molecular vibrational imaging (MVI) are the two most successful label-free methods, providing morphology and biochemistry, respectively, that have pioneered numerous applications along their independent technological maturity over the past few decades. However, the distinct label-free contrasts are inherently complementary and difficult to integrate due to the use of different light-matter interactions. Here, we present a unified imaging scheme that realizes simultaneous and in-situ acquisition of MV-fingerprint contrasts of single cells in the framework of QPI utilizing the mid-infrared photothermal effect. The fully label-free and robust integration of subcellular morphology and biochemistry would have important implications, especially for studying complex and fragile biological phenomena such as drug delivery, cellular diseases and stem cell development, where long-time observation of unperturbed cells are needed under low phototoxicity. △ Less

Submitted 5 December, 2019; originally announced December 2019.

Domain-Specific Language to Encode Induction Heuristics

Authors: Yutaka Nagashima

Abstract: Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of… ▽ More Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics specified by experienced users, thus systematically transferring experienced users' expertise to new Isabelle users. △ Less

Submitted 29 June, 2019; originally announced July 2019.

Comments: Accepted at ICFP2019-SRC (International Conference on Functional Programming Student Research Competition). Our draft, "LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL" (arXiv:1906.08084), gives further details of this domain specific language. arXiv admin note: substantial text overlap with arXiv:1906.08084

Designing Game of Theorems

Authors: Yutaka Nagashima

Abstract: "Theorem proving is similar to the game of Go. So, we can probably improve our provers using deep learning, like DeepMind built the super-human computer Go program, AlphaGo." Such optimism has been observed among participants of AITP2017. But is theorem proving really similar to Go? In this paper, we first identify the similarities and differences between them and then propose a system in which va… ▽ More "Theorem proving is similar to the game of Go. So, we can probably improve our provers using deep learning, like DeepMind built the super-human computer Go program, AlphaGo." Such optimism has been observed among participants of AITP2017. But is theorem proving really similar to Go? In this paper, we first identify the similarities and differences between them and then propose a system in which various provers keep competing against each other and changing themselves until they prove conjectures provided by users. △ Less

Submitted 20 June, 2019; originally announced June 2019.

Comments: Presented at the third Conference on Artificial Intelligence and Theorem Proving (AITP 2018)

LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL

Authors: Yutaka Nagashima

Abstract: Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little tool support for transferring this expert knowledge to a wider user audience. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heu… ▽ More Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little tool support for transferring this expert knowledge to a wider user audience. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus automating the knowledge transfer loop. △ Less

Submitted 24 May, 2020; v1 submitted 19 June, 2019; originally announced June 2019.

Comments: This is the pre-print of our paper of the same title accepted at APLAS2019 (https://doi.org/10.1007/978-3-030-34175-6_14). We updated the draft after fixing the errata found by Kenji Miyamoto

Towards Evolutionary Theorem Proving for Isabelle/HOL

Authors: Yutaka Nagashima

Abstract: Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, su… ▽ More Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation. △ Less

Submitted 17 April, 2019; originally announced April 2019.

Comments: 2 pages, This is a pre-print of our poster-only paper accepted at GECCO'19. For the final version, please visit the corresponding ACM website

Towards Machine Learning Induction

Authors: Yutaka Nagashima

Abstract: Induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle/HOL. Then, we present MeLoId, our approach to suggesting promising applications of induction without completing a proof search. Induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle/HOL. Then, we present MeLoId, our approach to suggesting promising applications of induction without completing a proof search. △ Less

Submitted 26 March, 2019; v1 submitted 4 December, 2018; originally announced December 2018.

Comments: This abstract is submitted to the fourth Conference on Artificial Intelligence (AITP2019) and Theorem Proving and to the third Workshop on Learning in Verification (LiVE2019)

PaMpeR: Proof Method Recommendation System for Isabelle/HOL

Authors: Yutaka Nagashima, Yilun He

Abstract: Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on… ▽ More Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users' expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users' proof methods invocation especially when it comes to special purpose proof methods. △ Less

Submitted 19 June, 2018; originally announced June 2018.

Comments: An anonymized version of this paper has been submitted to a Computer Science conference in April 2018

Goal-Oriented Conjecturing for Isabelle/HOL

Authors: Yutaka Nagashima, Julian Parsert

Abstract: We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isa… ▽ More We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle's strong automation to identify and prove such conjectures. △ Less

Submitted 25 July, 2018; v1 submitted 12 June, 2018; originally announced June 2018.

Comments: This paper has been accepted at 11th Conference on Intelligent Computer Mathematics. An error in Abstract has been fixed

Macroscale three-dimensional proximity effect in disordered normal/superconductor nanocomposites

Authors: Katsuya Ueno, Nobuhito Kokubo, Satoru Okayasu, Tsutomu Nojima, Yukihito Nagashima, Yusuke Seto, Megumi Matsumoto, Takahiro Sakurai, Hithoshi Ohta, Kazuyuki Takahashi, Takashi Uchino

Abstract: Recently, interest in Superconductor (S)-Normal (N) interfaces was renewed by the observation of exotic proximity effects in various systems, including S/semiconductor, S/ferromagnet, and S/topological insulator. In general, the proximity effect is enhanced in transparent weak links where coherent Andreev reflection is possible. Also, it is a common knowledge that the proximity effect is, by defin… ▽ More Recently, interest in Superconductor (S)-Normal (N) interfaces was renewed by the observation of exotic proximity effects in various systems, including S/semiconductor, S/ferromagnet, and S/topological insulator. In general, the proximity effect is enhanced in transparent weak links where coherent Andreev reflection is possible. Also, it is a common knowledge that the proximity effect is, by definition, is a localized phenomenon that can only be active in each S/N interface region. However, here we show that a three-dimensional (3D) macroscale proximity effect is realized in few-micrometer-thick MgO/Mg2Si/MgB2 nanocomposite layers with atomically smooth and clean heterointerfaces. We found from scanning superconducting quantum interference device (SQUID) microscopy measurements that a normal region of more than 100x100 square micrometers totally undergoes transition into a bulk-like superconducting state although the normal host originally contains less than ~10 vol % of superconducting MgB2 nanograins in a dispersed manner. In the proximity-induced superconducting region, vortex formation and annihilation processes as well as vortex-free Meissner regions were observed with respect to applied fields in a similar manner as Abrikosov vortices in type-II superconductors. Furthermore, we found that the induced superconducting layers exhibit an anisotropic magnetization behavior, in consistent with the formation of the large-scale superconducting coherence. This unusually extended proximity effect suggests that disorder-induced interaction and coupling of Andreev bound states, which are coherent superposition of time reversed electron hole pairs, is realized in the nanocomposite. Thus, the present results not only expand the limit of the proximity effect to bulk scales, but also provides a new route to obtain a proximity-induced superconducting state from disordered systems. △ Less

Submitted 14 September, 2017; v1 submitted 4 September, 2017; originally announced September 2017.

Comments: 21 pages, 4 main figures and 6 additional figures

Towards Smart Proof Search for Isabelle

Authors: Yutaka Nagashima

Abstract: Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach. Then, we propose an AI-based approach to drastically improve proof automation for Isabelle, while identifying three major challenges we plan to address for this obj… ▽ More Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach. Then, we propose an AI-based approach to drastically improve proof automation for Isabelle, while identifying three major challenges we plan to address for this objective. △ Less

Submitted 10 January, 2017; originally announced January 2017.

Comments: Accepted at AITP2017

Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML

Authors: Yutaka Nagashima, Liam O'Connor

Abstract: We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses. We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Comments: Accepted by ACM SIGPLAN Workshop on ML, September 2016

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL

Authors: Yutaka Nagashima, Ramana Kumar

Abstract: We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL's monadic interpreter to… ▽ More We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL's monadic interpreter to show that the underlying idea of PSL is transferable to other ITPs. △ Less

Submitted 1 March, 2017; v1 submitted 9 June, 2016; originally announced June 2016.

Comments: This paper has been submitted to CADE26

COGENT: Certified Compilation for a Functional Systems Language

Authors: Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby Murray, Gerwin Klein

Abstract: We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing suc… ▽ More We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL. △ Less

Submitted 21 January, 2016; originally announced January 2016.

The Physics of the B Factories

Authors: A. J. Bevan, B. Golob, Th. Mannel, S. Prell, B. D. Yabsley, K. Abe, H. Aihara, F. Anulli, N. Arnaud, T. Aushev, M. Beneke, J. Beringer, F. Bianchi, I. I. Bigi, M. Bona, N. Brambilla, J. B rodzicka, P. Chang, M. J. Charles, C. H. Cheng, H. -Y. Cheng, R. Chistov, P. Colangelo, J. P. Coleman, A. Drutskoy , et al. (2009 additional authors not shown)

Abstract: This work is on the Physics of the B Factories. Part A of this book contains a brief description of the SLAC and KEK B Factories as well as their detectors, BaBar and Belle, and data taking related issues. Part B discusses tools and methods used by the experiments in order to obtain results. The results themselves can be found in Part C. Please note that version 3 on the archive is the auxiliary… ▽ More This work is on the Physics of the B Factories. Part A of this book contains a brief description of the SLAC and KEK B Factories as well as their detectors, BaBar and Belle, and data taking related issues. Part B discusses tools and methods used by the experiments in order to obtain results. The results themselves can be found in Part C. Please note that version 3 on the archive is the auxiliary version of the Physics of the B Factories book. This uses the notation alpha, beta, gamma for the angles of the Unitarity Triangle. The nominal version uses the notation phi_1, phi_2 and phi_3. Please cite this work as Eur. Phys. J. C74 (2014) 3026. △ Less

Submitted 31 October, 2015; v1 submitted 24 June, 2014; originally announced June 2014.

Comments: 928 pages, version 3 (arXiv:1406.6311v3) corresponds to the alpha, beta, gamma version of the book, the other versions use the phi1, phi2, phi3 notation

Report number: SLAC-PUB-15968, KEK Preprint 2014-3

Journal ref: Eur. Phys. J. C74 (2014) 3026

Search for Dark Matter WIMPs using Upward Through-going Muons in Super-Kamiokande

Authors: Super-Kamiokande Collaboration, :, S. Desai, Y. Ashie, S. Fukuda, Y. Fukuda, K. Ishihara, Y. Itow, Y. Koshio, A. Minamino, M. Miura, S. Moriyama, M. Nakahata, T. Namba, R. Nambu, Y. Obayashi, N. Sakurai, M. Shiozawa, Y. Suzuki, H. Takeuchi, Y. Takeuchi, S. Yamada, M. Ishitsuka, T. Kajita, K. Kaneyuki , et al. (112 additional authors not shown)

Abstract: We present the results of indirect searches for Weakly Interacting Massive Particles (WIMPs) with 1679.6 live days of data from the Super-Kamiokande detector using neutrino-induced upward through-going muons. The search is performed by looking for an excess of high energy muon neutrinos from WIMP annihilations in the Sun, the core of the Earth, and the Galactic Center, as compared to the number… ▽ More We present the results of indirect searches for Weakly Interacting Massive Particles (WIMPs) with 1679.6 live days of data from the Super-Kamiokande detector using neutrino-induced upward through-going muons. The search is performed by looking for an excess of high energy muon neutrinos from WIMP annihilations in the Sun, the core of the Earth, and the Galactic Center, as compared to the number expected from the atmospheric neutrino background. No statistically significant excess was seen. We calculate flux limits in various angular cones around each of the above celestial objects. We obtain conservative model-independent upper limits on WIMP-nucleon cross-section as a function of WIMP mass and compare these results with the corresponding results from direct dark matter detection experiments. △ Less

Submitted 27 July, 2004; v1 submitted 21 April, 2004; originally announced April 2004.

Comments: 10 pages, 14 figures, Submitted to Phys. Rev. D

Journal ref: Phys.Rev.D70:083523,2004; Erratum-ibid.D70:109901,2004