P. Maksimović

We present the report of the hadronic working group of the BOOST2010 workshop held at the University of Oxford in June 2010. The first part contains a review of the potential of hadronic decays of highly boosted particles as an aid for discovery at the LHC and a discussion of the status of tools developed to meet the challenge of reconstructing and isolating these topologies. In the second part, we present new results comparing the performance of jet grooming techniques and top tagging algorithms on a common set of benchmark channels. We also study the sensitivity of jet substructure observables to the uncertainties in Monte Carlo predictions.

In this paper, we review recent theoretical progress and the latest experimental results in jet substructure from the Tevatron and the LHC. We review the status of and outlook for calculation and simulation tools for studying jet substructure. Following up on the report of the Boost 2010 workshop, we present a new set of benchmark comparisons of substructure techniques, focusing on the set of variables and grooming methods that are collectively known as 'top taggers'. To facilitate further exploration, we have attempted to collect, harmonize and publish software implementations of these techniques.

Over the past decade, a large number of jet substructure observables have been proposed in the literature, and explored at the LHC experiments. Such observables attempt to utilize the internal structure of jets in order to distinguish those initiated by quarks, gluons, or by boosted heavy objects, such as top quarks and W bosons. This report, originating from and motivated by the BOOST2013 workshop, presents original particle-level studies that aim to improve our understanding of the relationships between jet substructure observables, their complementarity, and their dependence on the underlying jet properties, particularly the jet radius and jet transverse momentum. This is explored in the context of quark/gluon discrimination, boosted W boson tagging and boosted top quark tagging.

This report provides a comprehensive overview of the prospects for B physics at the Tevatron. The work was carried out during a series of workshops starting in September 1999. There were four working groups: 1) CP Violation, 2) Rare and Semileptonic Decays, 3) Mixing and Lifetimes, 4) Production, Fragmentation and Spectroscopy. The report also includes introductory chapters on theoretical and experimental tools emphasizing aspects of B physics specific to hadron colliders, as well as overviews of the CDF, D0, and BTeV detectors, and a Summary.

U ovoj studiji pružen je pregled procesa razvoja veb aplikacija namenjenih podršci elektronske uprave u procesu izdavanja dokumenata. Analizirane su prednosti i nedostaci tehnologija koje su odabrane za implementaciju, kao i samog izabranog rešenja. Pored toga, pružen je predlog mogućih poboljšanja u postojećem rešenju s ciljem optimizacije njegove efikasnosti i funkcionalnosti.

We demonstrate the utility of leptons which fail standard isolation criteria in searches for new physics at the LHC. Such leptons can arise in any event containing a highly boosted particle which decays to both leptons and quarks. We begin by considering multiple extensions to the Standard Model which primarily lead to events with non-isolated leptons and are therefore missed by current search strategies. We emphasize the failure of standard isolation variables to adequately discriminate between signal and SM background for any value of the isolation cuts. We then introduce a new approach which makes use of jet substructure techniques to distinguish a broad range of signals from QCD events. We proceed with a simulated, proof-of-principle search for R-parity violating supersymmetry to demonstrate both the experimental reach possible with the use of non-isolated leptons and the utility of new substructure variables over existing techniques

High granularity silicon pixel sensors are at the heart of energy frontier particle physics collider experiments. At an collision rate of 40\,MHz, these detectors create massive amounts of data. Signal processing that handles data incoming at those rate and intelligently reduces the data within the pixelated region of the detector \textit{at rate} will enhance physics performance and enable physics analyses that are not currently possible. Using the shape of charge clusters deposited in an array of small pixels, the physical properties of the traversing particle can be extracted with locally customized neural networks. In this first work, we present a neural network that can be embedded into the on-sensor readout and filter out hits from low momentum tracks, reducing the detector's data volume by 54.4-75.4\%. The network is designed and simulated as a custom readout integrated circuit with 28\,nm CMOS technology and is expected to operate at less than 300\,$\mu W$ with an area of less than 0.2\,mm$^2$.

Computational grids are a promising resource for modeling complex biochemical processes such as protein folding, penetration of gases or water into proteins, or protein structural rearrangements coupled to ligand binding. We have enabled the molecular dynamics program CHARMM to run on the Open Science Grid. The implementation is general, flexible, easily modifiable for use with other molecular dynamics programs and other grids and automated in terms of job submission, monitoring, and resubmission. The usefulness of grid computing was demonstrated through the study of hydration of the Glu-66 side chain in the interior of protein staphylococcal nuclease. Multiple simulations started with and without two internal water molecules shown crystallographically to be associated with the side chain of Glu-66 yielded two distinct populations of rotameric states of Glu-66 that differed by as much as 20%. This illustrates how internal water molecules can bias protein conformations. Furthermore, there appeared to be a temporal correlation between dehydration of the side chain and conformational transitions of Glu-66. This example demonstrated how difficult it is to get convergence even in the relatively simple case of a side chain oscillating between two conformations. With grid computing, we also benchmarked the self-guided Langevin dynamics method against the Langevin dynamics method traditionally used for temperature control in molecular dynamics simulations and showed that the two methods yield comparable results.

This work describes the investigation of neuromorphic computing-based spiking neural network (SNN) models used to filter data from sensor electronics in high energy physics experiments conducted at the High Luminosity Large Hadron Collider (HL-LHC). We present our approach for developing a compact neuromorphic model that filters out the sensor data based on the particle's transverse momentum with the goal of reducing the amount of data being sent to the downstream electronics. The incoming charge waveforms are converted to streams of binary-valued events, which are then processed by the SNN. We present our insights on the various system design choices---from data encoding to optimal hyperparameters of the training algorithm---for an accurate and compact SNN optimized for hardware deployment. Our results show that an SNN trained with an evolutionary algorithm and an optimized set of hyperparameters obtains a signal efficiency of about 91% with nearly half as many parameters as a deep neural network.

New techniques for the reconstruction/validation and the simulation of hits in the pixel detectors of the Compact Muon Solenoid (CMS) Experiment are described.The techniques are based upon the use of pre-computed projected cluster shapes or "templates".A detailed simulation called Pixelav that has successfully described the profiles of clusters measured in beam tests of radiationdamaged sensors is used to generate the templates.Although the reconstruction technique was originally developed to optimally estimate the coordinates of hits after the detector became radiation damaged, it also has superior performance before irradiation.The technique requires a priori knowledge of the track angle which makes it suitable for the second in a two-pass reconstruction algorithm.However, the same modest angle sensitivity allows the algorithm to determine if the sizes and shapes of the cluster projections are consistent with the input angles.This information may be useful in suppressing spurious hits caused by secondary particles and in validating seeds used in track finding.The seed validation is currently under study but has the potential to significantly increase the speed of track finding in the CMS reconstruction software.Finally, a new procedure that uses the templates to re-weight clusters generated by the CMS offline simulation is described.The first tests of this technique are encouraging and when fully implemented, the technique will enable the fast simulation of pixel hits that have the characteristics of the much more CPU-intensive Pixelav hits.In particular, it may be the only practical technique available to simulate hits from a radiation damaged detector in the CMS offline software.

Differential rates in the decay B s 0 → J/ψϕ with ϕ →K + K −and J/ψ →μ+μ−are sensitive to the CP -violation phase β s = arg((−V ts V tb ∗)/(V cs V cb ∗)), predicted to be very small in the standard model. The analysis of B s 0 → J/ψϕ decays is also suitable for measuring the B s 0 lifetime, the decay width difference ΔΓ s between the B s 0 mass eigenstates, and the B s 0 oscillation frequency Δm even if appreciable CP violation does not occur. In this paper we present normalized probability densities useful in maximum likelihood fits, extended to allow for S -wave K + K − contributions on one hand and for direct CP violation on the other. Our treatment of the S -wave contributions includes the strong variation of the S -wave/P -wave amplitude ratio with m (K + K −) across the ϕ resonance, which was not considered in previous work. We include a scheme for re-normalizing the probability densities after detector sculpting of the angular distributions of the final state particles, and conclude with an examination of the symmetries of the rate formulae, with and without an S -wave K + K − contribution. All results are obtained with the use of a new compact formalism describing the differential decay rate of B s 0 mesons into J/ψϕ final states.

Abstract A new silicon microstrip detector was designed by the CDF collaboration for the proposed high-luminosity operation of the Tevatron p p ¯ collider (Run IIb). The detector is radiation-tolerant and will still be functional after exposure to particle fluences of 10 14 1 - MeV equivalent neutrons / cm 2 and radiation doses of 20 MRad. The detector will maintain or exceed the performance of the current CDF silicon detector throughout Run IIb. It is based on an innovative silicon “supermodule” design. Critical detector components like the custom radiation-hard SVX4 readout chip, the beryllia hybrids and mini-port (repeater) cards, and the silicon sensors fulfill their specifications and were produced with high yields. The design goals and solutions of the CDF Run IIb silicon detector are described, and the performance of preproduction modules is presented in detail. Results relevant for the development of future silicon systems are emphasized.

Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised, and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that, expectedly, abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.

Starting in September 1999, a series of workshops was carried out to study the prospects for B physics at the Tevatron. There were four working groups covering CP Violation, Rare and Semileptonic Decays, Mixing and Lifetimes, as well as Production, Fragmentation and Spectroscopy. Upon the completion of a comprehensive written report summarizing the results of this workshop, we will review the highlights of B Physics at the Tevatron in Run II and beyond. On our way to this goal, we will pass by questions such as ‘Why are there so many B factories these days?’ or ‘Why do we also want to do B Physics at Fermilab?’

A high performance system has been assembled using standard web components to deliver database information to a large number of broadly distributed clients. The CDF Experiment at Fermilab is establishing processing centers around the world imposing a high demand on their database repository. For delivering read-only data, such as calibrations, trigger information, and run conditions data, we have abstracted the interface that clients use to retrieve data objects. A middle tier is deployed that translates client requests into database specific queries and returns the data to the client as XML datagrams. The database connection management, request translation, and data encoding are accomplished in servlets running under Tomcat. Squid Proxy caching layers are deployed near the Tomcat servers, as well as close to the clients, to significantly reduce the load on the database and provide a scalable deployment model. Details the system's construction and use are presented, including its architecture, design, interfaces, administration, performance measurements, and deployment plan.

Over the past decade, a large number of jet substructure observables have been proposed in the literature, and explored at the LHC experiments. Such observables attempt to utilize the internal structure of jets in order to distinguish those initiated by quarks, gluons, or by boosted heavy objects, such as top quarks and W bosons. This report, originating from and motivated by the BOOST2013 workshop, presents original particle-level studies that aim to improve our understanding of the relationships between jet substructure observables, their complementarity, and their dependence on the underlying jet properties, particularly the jet radius and jet transverse momentum. This is explored in the context of quark/gluon discrimination, boosted W boson tagging and boosted top quark tagging.

Fermilab plans to deliver 5–15 fb−1 of integrated luminosity to the CDF and D0 experiments. The current inner silicon detectors at CDF (SVXIIa and L00) will not tolerate the radiation dose associated with high-luminosity running and will need to be replaced. A new readout chip (SVX4) has been designed in radiation-hard 0.25 μm, CMOS technology. Single-sided sensors are arranged in a compact structure, called a stave, with integrated readout and cooling systems. This paper describes the general design of the Run IIb system, testing results of prototype electrical components (staves), and prototype silicon sensor performance before and after irradiation.

The CMS Physics Analysis Toolkit (PAT) is presented. The PAT is a high-level analysis layer enabling the development of common analysis efforts across and within Physics Analysis Groups. It aims at fulfilling the needs of most CMS analyses, providing both ease-of-use for the beginner and flexibility for the advanced user. The main PAT concepts are described in detail and some examples from physics analyses are given.

This work describes the investigation of neuromorphic computing-based spiking neural network (SNN) models used to filter data from sensor electronics in high energy physics experiments conducted at the High Luminosity Large Hadron Collider. We present our approach for developing a compact neuromorphic model that filters out the sensor data based on the particle's transverse momentum with the goal of reducing the amount of data being sent to the downstream electronics. The incoming charge waveforms are converted to streams of binary-valued events, which are then processed by the SNN. We present our insights on the various system design choices - from data encoding to optimal hyperparameters of the training algorithm - for an accurate and compact SNN optimized for hardware deployment. Our results show that an SNN trained with an evolutionary algorithm and an optimized set of hyperparameters obtains a signal efficiency of about 91% with nearly half as many parameters as a deep neural network.

Highly granular pixel detectors allow for increasingly precise measurements of charged particle tracks. Next-generation detectors require that pixel sizes will be further reduced, leading to unprecedented data rates exceeding those foreseen at the High Luminosity Large Hadron Collider. Signal processing that handles data incoming at a rate of O(40MHz) and intelligently reduces the data within the pixelated region of the detector at rate will enhance physics performance at high luminosity and enable physics analyses that are not currently possible. Using the shape of charge clusters deposited in an array of small pixels, the physical properties of the traversing particle can be extracted with locally customized neural networks. In this first demonstration, we present a neural network that can be embedded into the on-sensor readout and filter out hits from low momentum tracks, reducing the detector's data volume by 54.4-75.4%. The network is designed and simulated as a custom readout integrated circuit with 28 nm CMOS technology and is expected to operate at less than 300 $\mu W$ with an area of less than 0.2 mm$^2$. The temporal development of charge clusters is investigated to demonstrate possible future performance gains, and there is also a discussion of future algorithmic and technological improvements that could enhance efficiency, data reduction, and power per area.

The combinatorics of track seeding has long been a computational bottleneck for triggering and offline computing in High Energy Physics (HEP), and remains so for the HL-LHC. Next-generation pixel sensors will be sufficiently fine-grained to determine angular information of the charged particle passing through from pixel-cluster properties. This detector technology immediately improves the situation for offline tracking, but any major improvements in physics reach are unrealized since they are dominated by lowest-level hardware trigger acceptance. We will demonstrate track angle and hit position prediction, including errors, using a mixture density network within a single layer of silicon as well as the progress towards and status of implementing the neural network in hardware on both FPGAs and ASICs.

The combinatorics of track seeding has long been a computational bottleneck for triggering and offline computing in High Energy Physics (HEP), and remains so for the HL-LHC. Next-generation pixel sensors will be sufficiently fine-grained to determine angular information of the charged particle passing through from pixel-cluster properties. This detector technology immediately improves the situation for offline tracking, but any major improvements in physics reach are unrealized since they are dominated by lowest-level hardware trigger acceptance. We will demonstrate track angle and hit position prediction, including errors, using a mixture density network within a single layer of silicon as well as the progress towards and status of implementing the neural network in hardware on both FPGAs and ASICs.

The innermost layer (L00) of the Run IIa silicon detector of CDF was planned to be replaced for the high luminosity Tevatron upgrade of Run IIb. This new silicon layer (L0) is designed to be a radiation tolerant replacement for the otherwise very similar L00 from Run IIa. The data are read out via long, fine-pitch, low-mass cables allowing the hybrids with the chips to sit at higher z(/spl sim/70 cm), outside of the tracking volume. The design and first results from the prototyping phase are presented. Special focus is placed on the amount and the structure of induced noise as well as signal-to-noise values.

We describe the characteristics of silicon microstrip sensors fabricated by Hamamatsu Photonics for the CDF Run 2b silicon detector. A total of 953 sensors, including 117 prototype sensors, have been produced and tested. Five sensors were irradiated with neutrons up to 1.4 /spl times/10/sup 14/ n/cm/sup 2/ as a part of the sensor quality assurance program. The electrical and mechanical characteristics are found to be superior in all aspects and fulfill our specifications. We comment on charge-up susceptibility of the sensors that employ a <100> crystal structure.

The various generations of Silicon Vertex Detectors (SVX, SVX', SVXII) for Collider Detector at Fermilab (CDF) at the Fermilab Tevatron have been fundamental tools for heavy-flavor tagging via secondary vertex detection. The CDF Run IIb Silicon Vertex Detector (SVXIIb) has been designed to be a radiation-tolerant replacement for the currently installed SVXII because SVXII was not expected to survive the Tevatron luminosity anticipated for Run IIb. One major change in the new design is the use of a single mechanical and electrical element throughout the array. This element, called a stave, carries six single-sided silicon sensors on each side and is built using carbon fiber skins with a high thermal conductivity on a foam core with a built-in cooling channel. A Kapton bus cable carries power, data and control signals underneath the silicon sensors on each side of the stave. Sensors are read out in pairs via a ceramic hybrid glued on one of the sensors and equipped with four SVX4 readout chips. This new design concept leads to a very compact mechanical and electrical unit, allowing streamlined production and ease of testing and installation. A description of the design and mechanical performance of the stave is given. Results on the electrical performance obtained using prototype staves are also presented.

The main building block and readout unit of the planned CDF Run IIb silicon detector is a "stave," a highly integrated mechanical, thermal, and electrical structure. One of its characteristic features is a copper-on-Kapton flexible cable for power, high voltage, data transmission, and control signals that is placed directly below the silicon microstrip sensors. The dense packaging makes deadtime-less operation of the stave a challenge since coupling of bus cable activity into the silicon sensors must be suppressed efficiently. The stave design features relevant for deadtime-less operation are discussed. The electrical performance achieved with stave prototypes is presented.

We present a new technique for pixel hit reconstruction with the CMS pixel detector. The technique is based on fitting the pixel cluster projections to templates obtained using a detailed simulation called Pixelav. Pixelav successfully describes the profiles of clusters measured in beam tests of radiation-damaged sensors. Originally developed to optimally estimate the coordinates of hits after the radiation damage, the technique has superior performance before irradiation as well, reducing the resolution tails of reconstructed track parameters and significantly reducing the light quark background of tagged b-quarks. It is the only technique currently available to simulate hits from a radiation-damaged detector.

New techniques for the reconstruction of hits in the pixel detectors of the Compact Muon Solenoid (CMS) experiment are described. The techniques are based upon the use of pre-computed projected cluster shapes or templates. A detailed simulation called Pixelav that has successfully described the profiles of clusters measured in beam tests of radiation-damaged sensors is used to generate the templates. Although the reconstruction technique was originally developed to optimally estimate the coordinates of hits after the detector became radiation damaged, it also has superior performance before irradiation. The technique requires a priori knowledge of the track angle which makes it suitable for the second in a two-pass reconstruction algorithm. However, the same modest angle sensitivity allows the algorithm to determine if the sizes and shapes of the cluster projections are consistent with the input angles. This information is proved to be useful in suppressing spurious hits caused by secondary particles and in validating seeds used in track finding. In addition, the template technique improves the resolution on the track impact parameter and light quark background rejection in b-tagged jets. Finally, a new procedure that uses the templates to reweigh clusters generated by the CMS offline simulation is described.

In the past decade, the Large Hadron Collider (LHC) has probed a higher energy scale than ever before. Most models of physics beyond the standard model (BSM) predict the production of new heavy particles; the LHC results have excluded lower masses of such particles. This makes the high-mass regions especially interesting for current and future searches. In most BSM scenarios of interest, the new heavy resonances decay to standard model particles. In a subset of these models, the new particles have large couplings to the top quark, the W and Z bosons, or the Higgs boson. The top quark and W, Z, and Higgs bosons often decay to quarks, giving rise to jets of particles with substructure; event selection based on substructure is used to suppress standard model backgrounds. This review covers the key concepts in experimental searches based on the jet substructure and discusses recent results from the ATLAS and CMS experiments.

We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly's stack-based semantics and the strong guarantees given by WebAssembly's type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly's uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

We present recent results from the CDF experiment, based on the data taken between 1992 and 1995 (Tevatron Run I). We classify the results according to the need to know the initial flavor of the B meson. Of the analyses that do not require this knowledge, we focus on the measurements of cross-sections, lifetimes, and polarizations. Next, we describe the analyses based on the knowledge of the initial flavor of the B meson: several B0 mixing measurements (which are also used to study the flavor determination), a Bs mixing search, and a recently updated limit on sin(2β).

This is an evolving document describing the meta-theory, the implementation, and the instantiations of Gillian, a multi-language symbolic analysis platform.

The Run II experiments at Fermilab, CDF and D0, have extensive database needs covering many areas of their online and offline operations. Delivering data to users and processing farms worldwide has represented major challenges to both experiments. The range of applications employing databases includes, calibration (conditions), trigger information, run configuration, run quality, luminosity, data management, and others. Oracle is the primary database product being used for these applications at Fermilab and some of its advanced features have been employed, such as table partitioning and replication. There is also experience with open source database products such as MySQL for secondary databases used, for example, in monitoring. Tools employed for monitoring the operation and diagnosing problems are also described.

The Collider Detector at Fermilab (CDF) operates in the beamline of the Tevatron proton-antiproton collider at Batavia, IL. The Tevatron is expected to undergo luminosity upgrades (Run IIb) in the future, resulting in a higher number of interactions per beam crossing. To operate in this dense radiation environment, an upgrade of the CDF's silicon vertex detector subsystem and a corresponding upgrade of its VME-based DAQ system has been explored. Prototypes of all the Run IIb SVX DAQ components have been constructed, assembled into a test stand, and operated successfully using an adapted version of the CDF's network-capable DAQ software. In addition, a PCI-based DAQ system has been developed as a fast and inexpensive tool for silicon detector and DAQ component testing in the production phase. We present an overview of the Run IIb silicon DAQ upgrade, emphasizing the new features and improvements incorporated into the constituent VME boards and discuss a PCI-based DAQ system developed to facilitate production tests.

The physics program of Run II at the Tevatron includes precision electroweak measurements such as the determination of the top quark and W boson masses; bottom and charm physics including the determination of the B{sub s} and D{sup 0} mixing parameters; studies of the strong interaction; and searches for the Higgs particle, supersymmetric particles, hidden space-time dimensions and quark substructure. All of these measurements benefit from a high-resolution tracking detector. Most of them rely heavily on the efficient identification of heavy flavored B hadrons by detection of displaced secondary vertices, and are enhanced by the capability to trigger on tracks not coming from the primary vertex. This is uniquely provided by CDF's finely-segmented silicon detectors surrounding the interaction region. Thus CDF experiment's physics potential critically depends on the performance of its silicon detectors. The CDF silicon detectors were designed to operate up to 2-3 fb{sup -1} of accumulated pji collisions, with an upgrade planned thereafter. However, the upgrade project was canceled in 2003 and Run II has been extended through 2011, with an expected total delivered integrated luminosity of 12 fb{sup -1} or more. Several preventive measures were taken to keep the original detector operational and maintain its performance. The most important of these are the decrease in the operating temperature of the detector, which reduces the impact of radiation exposure, and measures to minimize damage due to integrated radiation dose, thermal cycles, and wire bond resonance conditions. Despite these measures the detectors operating conditions continue to change with issues arising from radiation damage to the sensors, aging infrastructure and electronics. These, together with the basic challenges posed by the inaccessibility of the detector volume and large number (about 750 thousand) of readout channels, make the silicon detector operations the single most complex and high priority job in the CDF experiment.

On presente une Logique Probabiliste avec des operateurs Conditionnels - LPCP, sa syntaxe, semantique, axiomatisation correcte et fortement complete, comprenant une regle de deduction infinitaire. On prouve que LPCP est decidable, et on l'etend pour qu’il puisse representer l'evidence, en creant ainsi la premiere axiomatisation propositionnelle du raisonnement base sur l'evidence. On codifie les Logiques Probabilistes LPP1Q et LPPQ2 dans l'Assistant de Preuve Coq, et on verifie formellement leurs proprietes principales: correction, completude fort et non-compacite. Les deux logiques etendent la Logique Classique avec des operateurs de probabilite, et presentent une regle de deduction infinitaire. LPPQ1 permet des iterations des operateurs de probabilite, lorsque LPPQ2 ne le permet pas. On a formellement justifie l'utilisation des solveurs SAT probabilistes pour verifier les questions liees a la coherence. On presente LFP, un Cadre Logique avec Predicats Externes, en introduisant un mecanisme pour bloquer et debloquer types et termes dans LF, en permettant l'utilisation d’oracles externes. On demontre que LFP satisfait tous les principales proprietes et on developpe un cadre canonique correspondant, qui permet de prouver l’adequation. On fournit diverses encodages - le λ-calcul non-type avec la strategie de reduction CBV, Programmation-par-Contrats, un langage imperatif avec la Logique de Hoare, des Logiques Modales et la Logique Lineaire Non-Commutative, en montrant que en LFP on peut codifier aisement des side-conditions dans l'application des regles de typage et atteindre une separation entre verification et computation, en obtenant des preuves plus claires et lisibles.

Differential rates in the decay B 0 s → J/ � with � → K + K − andJ/ → µ + µ − are sensitive to the CP-violation phases = arg((−VtsV ∗ tb )/(VcsV ∗ cb )), predicted to be very small in the standard model. The analysis of B 0 → J/ � decays is also suitable for measuring theB 0 s lifetime, the decay width differences between theB 0 mass eigenstates, and the B 0 oscillation frequencym even if appreciable CP violation does not occur. In this paper we present normalized probability densities useful in maximum likelihood fits, extended to allow for S-wave K + K − contributions on one hand and for directCP violation on the other. Our treatment of the S-wave contributions includes the strong variation of the S-wave/P-wave amplitude ratio with m(K + K − ) across theresonance, which was not considered in previous work. We include a scheme for re-normalizing the probability densities after detector sculpting of the angular distributions of the final state particles, and conclude with an examination of the symmetries of the rate formulae, with and without an S-wave K + K − contribution. All results are obtained with the use of a new compact formalism describing the differential decay rate of B 0 mesons into J/ � final states.

je sistem u ovim dinamičkim stanjima najosetljiviji na perturbacije.

Expanding the mass range and techniques by which we search for dark matter is an important part of the worldwide particle physics program. Accelerator-based searches for dark matter and dark sector particles are a uniquely compelling part of this program as a way to both create and detect dark matter in the laboratory and explore the dark sector by searching for mediators and excited dark matter particles. This paper focuses on developing the DarkQuest experimental concept and gives an outlook on related enhancements collectively referred to as LongQuest. DarkQuest is a proton fixed-target experiment with leading sensitivity to an array of visible dark sector signatures in the MeV-GeV mass range. Because it builds off of existing accelerator and detector infrastructure, it offers a powerful but modest-cost experimental initiative that can be realized on a short timescale.

Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised, and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that, expectedly, abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.

CDF and DØ are caught between the idealistic projections from the mid‐1990’s based on the Run I results and their TDR’s on one side, and realistic extrapolations from the recent Run II measurements on the other. In this paper, we report only on the latter, and describe recent progress in other areas.

We have written a library of function classes in C++, which is distributed as part of the CLHEP foundation class libraries for High Energy Physics. The main goals of the library are to provide objects having all the mathematical behavior of functions, and to provide a mechanism for parameterizing these functions. Our functions support all the normal function operations such as addition, subtraction, multiplication, division, composition, et. cetera. The library allows programmers to compose complicated one-or multi-dimensional functions with great economy and natural semantics.

We report a measurement of the fraction of dijet events with a rapidity gap between jets produced by color-singlet exchange in {ovr p}p collisions at {radical} (s) =630 GeV at the Fermilab Tevatron. In events with two jets of transverse energy E{sup jet}{sub T}{gt}8 GeV , pseudorapidity in the range 1.8{lt}{vert_bar}{eta}{sup jet}{vert_bar}{lt}3.5 and {eta}{sub 1}{eta}{sub 2}{lt}0 , the color-singlet exchange fraction is found to be R=[2.7{plus_minus}0.7(stat){plus_minus}0 .6(syst)]{percent} . Comparisons are made with results obtained at {radical} (s) =1800 GeV and with theoretical expectations. {copyright} {ital 1998} {ital The American Physical Society }

A search for time-dependent B{sup 0}{sub d} mixing in the CDF inclusive lepton sample is described. The semileptonic decays (and their charge conjugates) are used to obtain the flavor of the decaying B-meson as well as the proper time of the decay, resulting in improved vertex and {beta}{gamma} resolution compared to more inclusive techniques. The B flavor at the time of production is determined by the combination of various CDF taggers. The authors use the CDF data collected during the 1992-1993 run.