6 papers
Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
Lidia Losavio, Marco Paganoni, Carlo A. Furia
Lightweight validation technique, such as those based on random testing, are sometimes practical alternatives to full formal verification -- providing valuable benefits, such as fi…
The CMS Barrel Timing Layer: test beam confirmation of module timing performance
F. Addesa, P. Akrap, A. Albert +127
First of its kind, the barrel section of the MIP Timing Detector is a large area timing detector based on LYSO:Ce crystals and SiPMs which are required to operate in an unprecedent…
Exploring Scintillators and Cherenkov Radiators for MIP Timing Detectors
R. Cala', L. Martinazzoli, N. Kratochwil +14
This article presents the timing performance of materials with fast light emission, tested as Minimum Ionizing Particle detectors using 150 GeV hadron beams in Monte Carlo simulati…
Optimization of LYSO crystals and SiPM parameters for the CMS MIP timing detector
F. Addesa, T. Anderson, P. Barria +68
For the High-Luminosity (HL-LHC) phase, the upgrade of the Compact Muon Solenoid (CMS) experiment at CERN will include a novel MIP Timing Detector (MTD). The central part of MTD, t…
Verifying Functional Correctness Properties At the Level of Java Bytecode
Marco Paganoni, Carlo A. Furia
The breakneck evolution of modern programming languages aggravates the development of deductive verification tools, which struggle to timely and fully support all new language feat…
Reasoning About Exceptional Behavior At the Level of Java Bytecode
Marco Paganoni, Carlo A. Furia
A program's exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program's correctness. On the other hand, formally verifyin…