Skip to main content

Showing 1–24 of 24 results for author: Fleury, M

.
  1. arXiv:2402.01202  [pdf, other

    cs.LO

    Life span of SAT techniques

    Authors: Mathias Fleury, Daniela Kaufmann

    Abstract: In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) d… ▽ More

    Submitted 2 February, 2024; originally announced February 2024.

  2. arXiv:2207.13577  [pdf, other

    cs.LO

    Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses

    Authors: Mathias Fleury, Armin Biere

    Abstract: We give a first account of our new parallel SAT solver Gimsatul. Its key feature is to share clauses physically in memory instead of copying them, which is the method of other state-of-the-art multi-threaded SAT solvers to exchange clauses logically. Our approach keeps information about which literals are watched in a clause local to a solving thread but shares the actual immutable literals of a c… ▽ More

    Submitted 29 July, 2022; v1 submitted 27 July, 2022; originally announced July 2022.

    Comments: Accepted at the Pragmatics of SAT workshop http://www.pragmaticsofsat.org/2022/

  3. Observations of Bell Inequality Violations with causal isolation between source and detectors

    Authors: Marc Fleury

    Abstract: We report the experimental observations of Bell Inequality Violations (BIV) in entangled photons causally separated by a rotating mirror. A Foucault mirror gating geometry is used to causally isolate the entangled photon source and detectors. We report an observed BIV of CHSH-$S = 2.30 \pm 0.07 > 2.00$. This result rules out theories that explain correlations with traveling communication between s… ▽ More

    Submitted 24 February, 2022; originally announced February 2022.

    Comments: 5 pages, 2 figures

  4. Alethe: Towards a Generic SMT Proof Format (extended abstract)

    Authors: Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine

    Abstract: The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the for… ▽ More

    Submitted 5 July, 2021; originally announced July 2021.

    Comments: In Proceedings PxTP 2021, arXiv:2107.01544

    ACM Class: I.2.3

    Journal ref: EPTCS 336, 2021, pp. 49-54

  5. Proceedings Seventh Workshop on Proof eXchange for Theorem Proving

    Authors: Chantal Keller, Mathias Fleury

    Abstract: This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 online conference in Pittsburgh, USA. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proo… ▽ More

    Submitted 4 July, 2021; originally announced July 2021.

    Journal ref: EPTCS 336, 2021

  6. arXiv:2106.01448  [pdf

    physics.flu-dyn physics.class-ph

    Spontaneous emergence of a spin state for an emitter in a time-varying medium

    Authors: Samuel Bernard-Bernardet, Marc Fleury, Emmanuel Fort

    Abstract: Time varying media can dramatically modify the emission of embedded sources by producing time reversed waves refocusing on the source. Here we show that such a back action can create an angular momentum by setting the source in a spontaneous spin state. We experimentally implement this coupling using self-propelled bouncing droplets sources coupled to the surface waves they emit on a parametricall… ▽ More

    Submitted 30 March, 2022; v1 submitted 2 June, 2021; originally announced June 2021.

  7. arXiv:2103.15647  [pdf, ps, other

    cond-mat.soft physics.app-ph

    Explicit and asymptotic solutions for frictional incomplete half-plane contacts subject to general oscillatory loading in the steady-state

    Authors: Hendrik Andresen, Rodolfo M. N. Fleury, Matthew R. Moore, David A. Hills

    Abstract: This contribution presents an asymptotic formulation for the stick-slip behaviour of incomplete contacts under oscillatory variation of normal load, moment, shear load and differential bulk tension. The asymptotic description allows us not only to approximate the size of the slip zones during the steady-state of a cyclic problem without knowledge of the geometry or contact law, but provides a solu… ▽ More

    Submitted 26 March, 2021; originally announced March 2021.

    Comments: 21 pages, 11 figures

    Journal ref: Journal of the Mechanics and Physics of Solids, Volume 146, 2021, 104214

  8. arXiv:2003.02370  [pdf, ps, other

    physics.chem-ph cond-mat.soft

    Elucidating the $^1$H NMR relaxation mechanism in polydisperse polymers and bitumen using measurements, MD simulations, and models

    Authors: Philip M. Singer, Arjun Valiya Parambathu, Xinglin Wang, Dilip Asthagiri, Walter G. Chapman, George J. Hirasaki, Marc Fleury

    Abstract: The mechanism behind the $^1$H NMR frequency dependence of $T_1$ and the viscosity dependence of $T_2$ for polydisperse polymers and bitumen remains elusive. We elucidate the matter through NMR relaxation measurements of polydisperse polymers over an extended range of frequencies ($f_0 = 0.01 \leftrightarrow$ 400 MHz) and viscosities ($η= 385 \leftrightarrow 102,000$ cP) using $T_{1}$ and $T_2$ in… ▽ More

    Submitted 4 March, 2020; originally announced March 2020.

  9. Reconstructing veriT Proofs in Isabelle/HOL

    Authors: Mathias Fleury, Hans-Jörg Schurr

    Abstract: Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theo… ▽ More

    Submitted 26 August, 2019; originally announced August 2019.

    Comments: In Proceedings PxTP 2019, arXiv:1908.08639

    Journal ref: EPTCS 301, 2019, pp. 36-50

  10. arXiv:1902.06990  [pdf

    cs.MM

    Effectiveness of Crypto-Transcoding for H.264/AVC and HEVC Video Bit-streams

    Authors: Rizwan A. Shah, Mamoona N. Asghar, Saima Abdullah, Martin Fleury, Neelam Gohar

    Abstract: To avoid delays arising from a need to decrypt a video prior to transcoding and then re-encrypt it afterwards, this paper assesses a selective encryption (SE) content protection scheme. The scheme is suited to both recent standardized codecs, namely H.264/Advanced Video Coding (AVC) and High Efficiency Video Coding (HEVC). Specifically, the paper outlines a joint crypto-transcoding scheme for secu… ▽ More

    Submitted 19 February, 2019; originally announced February 2019.

    Comments: Revision-3 Version of Multimedia Tools and Application (Springer)

  11. arXiv:1812.09011  [pdf, other

    physics.flu-dyn nlin.CD

    State space geometry of the chaotic pilot-wave hydrodynamics

    Authors: Nazmi Burak Budanur, Marc Fleury

    Abstract: We consider the motion of a droplet bouncing on a vibrating bath of the same fluid in the presence of a central potential. We formulate a rotation symmetry-reduced description of this system, which allows for the straightforward application of dynamical systems theory tools. As an illustration of the utility of the symmetry reduction, we apply it to a model of the pilot-wave system with a central… ▽ More

    Submitted 21 December, 2018; originally announced December 2018.

    Comments: Accepted for publication in Chaos: An Interdisciplinary Journal of Nonlinear Science

  12. arXiv:1809.06139  [pdf

    eess.SP cs.CV q-bio.NC

    Automatic Electrodes Detection during simultaneous EEG/fMRI acquisition

    Authors: Mathis Fleury, Pierre Maurel, Marsel Mano, Elise Bannier, Christian Barillot

    Abstract: Simultaneous EEG/fMRI acquisition allows to measure brain activity at high spatial-temporal resolution. The localisation of EEG sources depends on several parameters including the position of the electrodes on the scalp. The position of the MR electrodes during its acquisitions is obtained with the use of the UTE sequence allowing their visualisation. The retrieval of the electrodes consists in ob… ▽ More

    Submitted 17 September, 2018; originally announced September 2018.

    Comments: ISMRM, Jun 2018, Paris, France. 2018, https://www.ismrm.org/

  13. HARPS3 for a Roboticized Isaac Newton Telescope

    Authors: Samantha J. Thompson, Didier Queloz, Isabelle Baraffe, Martyn Brake, Andrey Dolgopolov, Martin Fisher, Michel Fleury, Joost Geelhoed, Richard Hall, Jonay I. Gonzalez Hernandez, Rik ter Horst, Jan Kragt, Ramon Navarro, Tim Naylor, Francesco Pepe, Nikolai Piskunov, Rafael Rebolo, Louis Sander, Damien Segransan, Eugene Seneta, David Sing, Ignas Snellen, Frans Snik, Julien Spronck, Eric Stempels , et al. (3 additional authors not shown)

    Abstract: We present a description of a new instrument development, HARPS3, planned to be installed on an upgraded and roboticized Isaac Newton Telescope by end-2018. HARPS3 will be a high resolution (R = 115,000) echelle spectrograph with a wavelength range from 380-690 nm. It is being built as part of the Terra Hunting Experiment - a future 10 year radial velocity measurement programme to discover Earth-l… ▽ More

    Submitted 16 August, 2016; originally announced August 2016.

    Comments: 13 pages, 8 figures, SPIE conference proceedings

    Journal ref: Proc. SPIE 9908, Ground-based and Airborne Instrumentation for Astronomy VI, 99086F (August 9, 2016)

  14. Axion String Dynamics I: 2+1D

    Authors: Leesa M. Fleury, Guy D. Moore

    Abstract: If the axion exists and if the initial axion field value is uncorrelated at causally disconnected points, then it should be possible to predict the efficiency of cosmological axion production, relating the axionic dark matter density to the axion mass. The main obstacle to making this prediction is correctly treating the axion string cores. We develop a new algorithm for treating the axionic strin… ▽ More

    Submitted 8 April, 2016; v1 submitted 15 February, 2016; originally announced February 2016.

    Comments: 22 pages plus two appendices; 15 figures. Version 2 adds minor clarifications and catches a few typos, no substantive changes. Published version

  15. Improving Cosmological Distance Measurements Using Twin Type Ia Supernovae

    Authors: H. K. Fakhouri, K. Boone, G. Aldering, P. Antilogus, C. Aragon, S. Bailey, C. Baltay, K. Barbary, D. Baugh, S. Bongard, C. Buton, J. Chen, M. Childress, N. Chotard, Y. Copin, P. Fagrelius, U. Feindt, M. Fleury, D. Fouchez, E. Gangler, B. Hayden, A. G. Kim, M. Kowalski, P. -F. Leget, S. Lombardo , et al. (19 additional authors not shown)

    Abstract: We introduce a method for identifying "twin" Type Ia supernovae, and using them to improve distance measurements. This novel approach to Type Ia supernova standardization is made possible by spectrophotometric time series observations from the Nearby Supernova Factory (SNfactory). We begin with a well-measured set of supernovae, find pairs whose spectra match well across the entire optical window,… ▽ More

    Submitted 5 November, 2015; v1 submitted 3 November, 2015; originally announced November 2015.

    Comments: 37 pages, 9 figures, 5 tables. Accepted for publication in ApJ. Fixed typo in arXiv abstract

  16. SN 2009ip at late times - an interacting transient at +2 years

    Authors: Morgan Fraser, Rubina Kotak, Andrea Pastorello, Anders Jerkstrand, Stephen J. Smartt, Ting-Wan Chen, Michael Childress, Gerard Gilmore, Cosimo Inserra, Erkki Kankare, Steve Margheim, Seppo Mattila, Stefano Valenti, Christopher Ashall, Stefano Benetti, Maria Teresa Botticella, Franz Erik Bauer, Heather Campbell, Nancy Elias-Rosa, Mathilde Fleury, Avishay Gal-Yam, Stephan Hachinger, D. Andrew Howell, Laurent Le Guillou, Pierre-François Léget , et al. (9 additional authors not shown)

    Abstract: We present photometric and spectroscopic observations of the interacting transient SN 2009ip taken during the 2013 and 2014 observing seasons. We characterise the photometric evolution as a steady and smooth decline in all bands, with a decline rate that is slower than expected for a solely $^{56}$Co-powered supernova at late phases. No further outbursts or eruptions were seen over a two year peri… ▽ More

    Submitted 20 February, 2015; originally announced February 2015.

    Comments: Submitted to MNRAS

  17. Confirmation of a Star Formation Bias in Type Ia Supernova Distances and its Effect on Measurement of the Hubble Constant

    Authors: M. Rigault, G. Aldering, M. Kowalski, Y. Copin, P. Antilogus, C. Aragon, S. Bailey, C. Baltay, D. Baugh, S. Bongard, K. Boone, C. Buton, J. Chen, N. Chotard, H. K. Fakhouri, U. Feindt, P. Fagrelius, M. Fleury, D. Fouchez, E. Gangler, B. Hayden, A. G. Kim, P. -F. Leget, S. Lombardo, J. Nordin , et al. (13 additional authors not shown)

    Abstract: Previously we used the Nearby Supernova Factory sample to show that SNe~Ia having locally star-forming environments are dimmer than SNe~Ia having locally passive environments.Here we use the \constitution\ sample together with host galaxy data from \GALEX\ to independently confirm that result. The effect is seen using both the SALT2 and MLCS2k2 lightcurve fitting and standardization methods, with… ▽ More

    Submitted 19 December, 2014; originally announced December 2014.

    Comments: 3 Figures ; Submitted to ApJ: Oct.~30, 2014 -- Accepted: Dec.~17, 2014

  18. arXiv:1411.4424  [pdf, other

    astro-ph.SR astro-ph.CO

    A metric space for type Ia supernova spectra

    Authors: Michele Sasdelli, W. Hillebrandt, G. Aldering, P. Antilogus, C. Aragon, S. Bailey, C. Baltay, S. Benitez-Herrera, S. Bongard, C. Buton, A. Canto, F. Cellier-Holzem, J. Chen, M. Childress, N. Chotard, Y. Copin, H. K. Fakhouri, U. Feindt, M. Fink, M. Fleury, D. Fouchez, E. Gangler, J. Guy, E. E. O. Ishida, A. G. Kim , et al. (21 additional authors not shown)

    Abstract: We develop a new framework for use in exploring Type Ia Supernova (SN Ia) spectra. Combining Principal Component Analysis (PCA) and Partial Least Square analysis (PLS) we are able to establish correlations between the Principal Components (PCs) and spectroscopic/photometric SNe Ia features. The technique was applied to ~120 supernova and ~800 spectra from the Nearby Supernova Factory. The ability… ▽ More

    Submitted 17 November, 2014; originally announced November 2014.

    Comments: 22 pages, 26 figures, 3 tables, accepted for publication in MNRAS

  19. arXiv:1411.0299  [pdf, ps, other

    astro-ph.SR astro-ph.IM

    PESSTO : survey description and products from the first data release by the Public ESO Spectroscopic Survey of Transient Objects

    Authors: S. J. Smartt, S. Valenti, M. Fraser, C. Inserra, D. R. Young, M. Sullivan, A. Pastorello, S. Benetti, A. Gal-Yam, C. Knapic, M. Molinaro, R. Smareglia, K. W. Smith, S. Taubenberger, O. Yaron, J. P. Anderson, C. Ashall, C. Balland, C. Baltay, C. Barbarino, F. E. Bauer, S. Baumont, D. Bersier, N. Blagorodnova, S. Bongard , et al. (77 additional authors not shown)

    Abstract: The Public European Southern Observatory Spectroscopic Survey of Transient Objects (PESSTO) began as a public spectroscopic survey in April 2012. We describe the data reduction strategy and data products which are publicly available through the ESO archive as the Spectroscopic Survey Data Release 1 (SSDR1). PESSTO uses the New Technology Telescope with EFOSC2 and SOFI to provide optical and NIR sp… ▽ More

    Submitted 10 May, 2015; v1 submitted 2 November, 2014; originally announced November 2014.

    Comments: Accepted for publication in A&A. Describes the PESSTO public data products. All reduced data available from the ESO archive. See http://www.pessto.org for download instructions

    Journal ref: A&A 579, A40 (2015)

  20. Type Ia Supernova Hubble Residuals and Host-Galaxy Properties

    Authors: A. G. Kim, G. Aldering, P. Antilogus, C. Aragon, S. Bailey, C. Baltay, S. Bongard, C. Buton, A. Canto, F. Cellier-Holzem, M. Childress, N. Chotard, Y. Copin, H. K. Fakhouri, U. Feindt, M. Fleury, E. Gangler, P. Greskovic, J. Guy, M. Kowalski, S. Lombardo, J. Nordin, P. Nugent, R. Pain, E. Pecontal , et al. (11 additional authors not shown)

    Abstract: Kim et al. (2013) [K13] introduced a new methodology for determining peak-brightness absolute magnitudes of type Ia supernovae from multi-band light curves. We examine the relation between their parameterization of light curves and Hubble residuals, based on photometry synthesized from the Nearby Supernova Factory spectrophotometric time series, with global host-galaxy properties. The K13 Hubble r… ▽ More

    Submitted 14 January, 2014; originally announced January 2014.

    Comments: 17 pages, 6 figures. Accepted by Astrophysical Journal

  21. The supernova CSS121015:004244+132827: a clue for understanding super-luminous supernovae

    Authors: S. Benetti, M. Nicholl, E. Cappellaro, A. Pastorello, S. J. Smartt, N. Elias-Rosa, A. J. Drake, L. Tomasella, M. Turatto, A. Harutyunyan, S. Taubenberger, S. Hachinger, A. Morales-Garoffolo, T. -W. Chen, S. G. Djorgovski, M. Fraser, A. Gal-Yam, C. Inserra, P. Mazzali, M. L. Pumo, J. Sollerman, S. Valenti, D. R. Young, M. Dennefeld, L. Le Guillou , et al. (2 additional authors not shown)

    Abstract: We present optical photometry and spectra of the super luminous type II/IIn supernova CSS121015:004244+132827 (z=0.2868) spanning epochs from -30 days (rest frame) to more than 200 days after maximum. CSS121015 is one of the more luminous supernova ever found and one of the best observed. The photometric evolution is characterized by a relatively fast rise to maximum (~40 days in the SN rest frame… ▽ More

    Submitted 17 March, 2014; v1 submitted 4 October, 2013; originally announced October 2013.

    Comments: 17 pages, 10 figures and 5 tables. In press to MNRAS. This version matches the accepted one. Main conclusions are unchanged

  22. Evidence of Environmental Dependencies of Type Ia Supernovae from the Nearby Supernova Factory indicated by Local Hα

    Authors: M. Rigault, Y. Copin, G. Aldering, P. Antilogus, C. Aragon, S. Bailey, C. Baltay, S. Bongard, C. Buton, A. Canto, F. Cellier-Holzem, M. Childress, N. Chotard, H. K. Fakhouri, U. Feindt, M. Fleury, E. Gangler, P. Greskovic, J. Guy, A. G. Kim, M. Kowalski, S. Lombardo, J. Nordin, P. Nugent, R. Pain , et al. (11 additional authors not shown)

    Abstract: (Abridged) We study the host galaxy regions in close proximity to Type Ia supernovae (SNe Ia) to analyze relations between the properties of SN Ia events and environments most similar to where their progenitors formed. We focus on local Hα emission as an indicator of young environments. The Nearby Supernova Factory has obtained flux-calibrated spectral timeseries for SNe Ia using integral field sp… ▽ More

    Submitted 10 September, 2013; v1 submitted 4 September, 2013; originally announced September 2013.

    Comments: accepted for publication in Section 3. Cosmology of A&A (The official date of acceptance is 30/08/2013)

  23. arXiv:1303.1312  [pdf, ps, other

    stat.ML cs.IT

    A Fast Iterative Bayesian Inference Algorithm for Sparse Channel Estimation

    Authors: Niels Lovmand Pedersen, Carles Navarro Manchón Bernard Henri Fleury

    Abstract: In this paper, we present a Bayesian channel estimation algorithm for multicarrier receivers based on pilot symbol observations. The inherent sparse nature of wireless multipath channels is exploited by modeling the prior distribution of multipath components' gains with a hierarchical representation of the Bessel K probability density function; a highly efficient, fast iterative Bayesian inference… ▽ More

    Submitted 6 March, 2013; originally announced March 2013.

    Comments: in Proc. IEEE Int. Communications Conf. (ICC), 2013

  24. arXiv:1212.2227  [pdf, other

    astro-ph.IM astro-ph.EP astro-ph.SR

    The ESPRI project: astrometric exoplanet search with PRIMA I. Instrument description and performance of first light observations

    Authors: J. Sahlmann, T. Henning, D. Queloz, A. Quirrenbach, N. M. Elias II, R. Launhardt, F. Pepe, S. Reffert, D. Segransan, J. Setiawan, R. Abuter, L. Andolfato, P. Bizenberger, H. Baumeister, B. Chazelas, F. Delplancke, F. Derie, N. Di Lieto, T. P. Duc, M. Fleury, U. Graser, A. Kaminski, R. Koehler, S. Leveque, C. Maire , et al. (20 additional authors not shown)

    Abstract: The ESPRI project relies on the astrometric capabilities offered by the PRIMA facility of the Very Large Telescope Interferometer for the discovery and study of planetary systems. Our survey consists of obtaining high-precision astrometry for a large sample of stars over several years and to detect their barycentric motions due to orbiting planets. We present the operation principle, the instrumen… ▽ More

    Submitted 10 December, 2012; originally announced December 2012.

    Comments: 32 pages, 39 figures, Accepted for publication in Astronomy and Astrophysics