-
Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
Authors:
Márk Somorjai,
Mihály Dobos-Kovács,
Zsófia Ádám,
Levente Bajczi,
András Vörös
Abstract:
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to…
▽ More
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique.
△ Less
Submitted 23 April, 2024;
originally announced April 2024.
-
Variable stars in the residual light curves of OGLE-IV eclipsing binaries towards the Galactic Bulge
Authors:
Rozália Z. Ádám,
Tamás Hajdu,
Attila Bódi,
Róbert Hajdu,
Tamás Szklenár,
László Molnár
Abstract:
Context. The Optical Gravitational Lensing Experiment (OGLE) observed around 450,000 eclipsing binaries (EBs) towards the Galactic Bulge. Decade-long photometric observations such as these provide an exceptional opportunity to thoroughly examine the targets. However, observing dense stellar fields such as the Bulge may result in blends and contamination by close objects.
Aims. We searched for pe…
▽ More
Context. The Optical Gravitational Lensing Experiment (OGLE) observed around 450,000 eclipsing binaries (EBs) towards the Galactic Bulge. Decade-long photometric observations such as these provide an exceptional opportunity to thoroughly examine the targets. However, observing dense stellar fields such as the Bulge may result in blends and contamination by close objects.
Aims. We searched for periodic variations in the residual light curves of EBs in OGLE-IV and created a new catalogue for the EBs that contain `background' signals after the investigation of the source of the signal.
Methods. From the about half a million EB systems, we selected those that contain more than 4000 data points. We fitted the EB signal with a simple model and subtracted it. To identify periodical signals in the residuals, we used a GPU-based phase dispersion minimisation python algorithm called cuvarbase and validated the found periods with Lomb-Scargle periodograms. We tested the reliability of our method with artificial light curves.
Results. We identified 354 systems where short-period background variation was significant. In these cases, we determined whether it is a new variable or just the result of contamination by an already catalogued nearby one. We classified 292 newly found variables into EB, $δ$ Scuti, or RR Lyrae categories, or their sub-classes, and collected them in a catalogue. We also discovered four new doubly eclipsing systems and one eclipsing multiple system with a $δ$ Scuti variable, and modelled the outer orbits of the components.
△ Less
Submitted 17 April, 2023;
originally announced April 2023.
-
Community Report from the Biosignatures Standards of Evidence Workshop
Authors:
Victoria Meadows,
Heather Graham,
Victor Abrahamsson,
Zach Adam,
Elena Amador-French,
Giada Arney,
Laurie Barge,
Erica Barlow,
Anamaria Berea,
Maitrayee Bose,
Dina Bower,
Marjorie Chan,
Jim Cleaves,
Andrea Corpolongo,
Miles Currie,
Shawn Domagal-Goldman,
Chuanfei Dong,
Jennifer Eigenbrode,
Allison Enright,
Thomas J. Fauchez,
Martin Fisk,
Matthew Fricke,
Yuka Fujii,
Andrew Gangidine,
Eftal Gezer
, et al. (50 additional authors not shown)
Abstract:
The search for life beyond the Earth is the overarching goal of the NASA Astrobiology Program, and it underpins the science of missions that explore the environments of Solar System planets and exoplanets. However, the detection of extraterrestrial life, in our Solar System and beyond, is sufficiently challenging that it is likely that multiple measurements and approaches, spanning disciplines and…
▽ More
The search for life beyond the Earth is the overarching goal of the NASA Astrobiology Program, and it underpins the science of missions that explore the environments of Solar System planets and exoplanets. However, the detection of extraterrestrial life, in our Solar System and beyond, is sufficiently challenging that it is likely that multiple measurements and approaches, spanning disciplines and missions, will be needed to make a convincing claim. Life detection will therefore not be an instantaneous process, and it is unlikely to be unambiguous-yet it is a high-stakes scientific achievement that will garner an enormous amount of public interest. Current and upcoming research efforts and missions aimed at detecting past and extant life could be supported by a consensus framework to plan for, assess and discuss life detection claims (c.f. Green et al., 2021). Such a framework could help increase the robustness of biosignature detection and interpretation, and improve communication with the scientific community and the public. In response to this need, and the call to the community to develop a confidence scale for standards of evidence for biosignature detection (Green et al., 2021), a community-organized workshop was held on July 19-22, 2021. The meeting was designed in a fully virtual (flipped) format. Preparatory materials including readings, instructional videos and activities were made available prior to the workshop, allowing the workshop schedule to be fully dedicated to active community discussion and prompted writing sessions. To maximize global interaction, the discussion components of the workshop were held during business hours in three different time zones, Asia/Pacific, European and US, with daily information hand-off between group organizers.
△ Less
Submitted 8 December, 2022; v1 submitted 25 October, 2022;
originally announced October 2022.
-
Evidence of gravitons as fused photons in four dimensions
Authors:
Z R Adam
Abstract:
A model of graviton momentum transfer was constructed to investigate a conjecture that gravitons are fused photons propagating in four dimensions. The model describes gravitational attraction between two bodies, each of simplified geometric shape and comprised of a calculable number of massive particles (quarks and leptons), as a probabilistic quantized mechanism of graviton scattering that give…
▽ More
A model of graviton momentum transfer was constructed to investigate a conjecture that gravitons are fused photons propagating in four dimensions. The model describes gravitational attraction between two bodies, each of simplified geometric shape and comprised of a calculable number of massive particles (quarks and leptons), as a probabilistic quantized mechanism of graviton scattering that gives rise to gravitational momentum flux. Earth-Human, Moon-Human, and Earth-Moon gravitational systems were investigated to solve for the wavelength of photons that comprise the graviton. The calculated wavelength for each system was approximately equal to the predicted value of the Planck length, which is interpreted as evidence that gravitons may be formed as fused four dimensional photons. The results corroborate current thinking about the temperature at which gravity separated from a unified force during the Big Bang, while explaining the weakness of the gravitational force from the atomic to the sub-planetary scale. Extension of the model produces unique, testable predictions arising from the averaged quantum properties of the graviton as fused photons, and the general model approach may be compatible with other efforts to describe the inner structure of the graviton.
△ Less
Submitted 1 June, 2009; v1 submitted 1 February, 2009;
originally announced February 2009.
-
Collective excitations of trapped Fermi or Bose gases
Authors:
A. Csordas,
Z. Adam
Abstract:
A new method is developed to calculate all excitations of trapped gases using hydrodynamics at zero temperature for any equation of state $μ=μ(n)$ and for any trap** potential. It is shown that a natural scalar product can be defined for the mode functions, by which the wave operator is hermitian and the mode functions are orthogonal. It is also shown that the Kohn-modes are exact for harmonic…
▽ More
A new method is developed to calculate all excitations of trapped gases using hydrodynamics at zero temperature for any equation of state $μ=μ(n)$ and for any trap** potential. It is shown that a natural scalar product can be defined for the mode functions, by which the wave operator is hermitian and the mode functions are orthogonal. It is also shown that the Kohn-modes are exact for harmonic trap** in hydrodynamic theory. Excitations for fermions are calculated in the BCS-BEC transition region using the equation of state of the mean-field Leggett-model for isotrop harmonic trap potential.
△ Less
Submitted 22 December, 2005;
originally announced December 2005.
