-
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
Authors:
Pedro Barroso,
Mário Pereira,
António Ravara
Abstract:
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering their formalization was performed essentially in first-order logic, one question left open by the authors was whether their proofs could be automated using a verification framework for first-order logic. We took the chal…
▽ More
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering their formalization was performed essentially in first-order logic, one question left open by the authors was whether their proofs could be automated using a verification framework for first-order logic. We took the challenge and automated their formalization using Why3, significantly reducing the proof effort. We systematically followed the Coq proofs and realized that in many cases at around one third of the way Why3 was able to discharge all VCs. Furthermore, the proofs still requiring interactions (e.g. induction, witnesses for existential proofs, assertions) were factorized isolating auxiliary results that we stated explicitly. In this way, we achieved an almost-automatic soundness and safety proof of the memory model. Nonetheless, our development allows an extraction of a correct-by-construction concrete memory model, going thus further than the preliminary Why version of Leroy and Blazy.
△ Less
Submitted 5 December, 2022;
originally announced December 2022.
-
Experimental study of the interaction of two laser-driven radiative shocks at the PALS laser
Authors:
R. L. Singh,
C. Stehle,
F. Suzuki-Vidal,
M. Kozlova,
J. Larour,
U. Chaulagain,
T. Clayson,
R. Rodriguez,
J. M. Gil,
J. Nejdl,
M. Krus,
J. Dostal,
R. Dudzak,
P. Barroso,
O. Acef,
M. Cotelo,
P. Velarde
Abstract:
Radiative shocks (RS) are complex phenomena which are ubiquitous in astrophysical environments. The study of such hypersonic shocks in the laboratory, under controlled conditions, is of primary interest to understand the physics at play and also to check the ability of numerical simulations to reproduce the experimental results. In this context, we conducted, at the Prague Asterix Laser System fac…
▽ More
Radiative shocks (RS) are complex phenomena which are ubiquitous in astrophysical environments. The study of such hypersonic shocks in the laboratory, under controlled conditions, is of primary interest to understand the physics at play and also to check the ability of numerical simulations to reproduce the experimental results. In this context, we conducted, at the Prague Asterix Laser System facility (PALS), the first experiments dedicated to the study of two counter-propagating radiative shocks propagating at non-equal speeds up to 25-50 km/s in noble gases at pressures ranging between 0.1 and 0.6 bar. These experiments highlighted the interaction between the two radiative precursors. This interaction is qualitatively but not quantitatively described by 1D simulations. Preliminary results obtained with XUV spectroscopy leading to the estimation of shock temperature and ion charge of the plasma are also presented.
△ Less
Submitted 5 May, 2022;
originally announced May 2022.
-
Target Design for XUV Probing of Radiative Shock Experiments
Authors:
U. Chaulagain,
C. Stehlé,
P. Barroso,
M. Kozlova,
J. Nejdl,
F. Suzuki Vidal,
J. Larour
Abstract:
Radiative shocks are strong shocks characterized by plasma at a high temperature emitting an important fraction of its energy as radiation. Radiative shocks are commonly found in many astrophysical systems and are templates of radiative hydrodynamic flows, which can be studied experimentally using high-power lasers. This is not only important in the context of laboratory astrophysics but also to b…
▽ More
Radiative shocks are strong shocks characterized by plasma at a high temperature emitting an important fraction of its energy as radiation. Radiative shocks are commonly found in many astrophysical systems and are templates of radiative hydrodynamic flows, which can be studied experimentally using high-power lasers. This is not only important in the context of laboratory astrophysics but also to benchmark numerical studies. We present details on the design of experiments on radiative shocks in xenon gas performed at the kJ scale PALS laser facility. It includes technical specifications for the tube targets design and numerical studies with the 1-D radiative hydrodynamics code MULTI. Emphasis is given to the technical feasibility of an XUV imaging diagnostic with a 21 nm (~58 eV) probing beam, which allows to probe simultaneously the post-shock and the precursor region ahead of the shock. The novel design of the target together with the improved X-ray optics and XUV source allow to show both the dense post-shock structure and the precursor of the radiative shock.
△ Less
Submitted 6 December, 2020;
originally announced December 2020.
-
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
Authors:
Pedro Barroso,
Mário Pereira,
António Ravara
Abstract:
We present an approach to obtain formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform because it allows to implement functions in a style very close to the mathematical definitions, as well as it allows a high degree of automation in the verification process.
As proof of concept, we present a mathematical definition of the algorithm to conver…
▽ More
We present an approach to obtain formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform because it allows to implement functions in a style very close to the mathematical definitions, as well as it allows a high degree of automation in the verification process.
As proof of concept, we present a mathematical definition of the algorithm to convert propositional formulae to conjunctive normal form, implementations in WhyML (the Why3 language, very similar to OCaml), and proofs of correctness of the implementations. We apply our proposal on two variants of this algorithm: one in direct-style and another with an explicit stack structure. Being both first-order versions, Why3 processes the proofs naturally.
△ Less
Submitted 10 March, 2020;
originally announced March 2020.
-
Equation of state and optical properties of shock-compressed C:H:N:O molecular mixtures
Authors:
M. Guarguaglini,
J. -A. Hernandez,
T. Okuchi,
P. Barroso,
A. Benuzzi-Mounaix,
R. Bolis,
E. Brambrink,
Y. Fujimoto,
R. Kodama,
M. Koenig,
F. Lefevre,
K. Miyanishi,
N. Ozaki,
T. Sano,
Y. Umeda,
T. Vinci,
A. Ravasio
Abstract:
Water, ethanol, and ammonia are the key components of the mantles of Uranus and Neptune. To improve structure and evolution models and give an explanation of the magnetic fields and luminosities of the icy giants, those components need to be characterised at planetary conditions (some Mbar and a few $10^3$ K). Those conditions are typical of the Warm Dense Matter regime, which exhibits a rich phas…
▽ More
Water, ethanol, and ammonia are the key components of the mantles of Uranus and Neptune. To improve structure and evolution models and give an explanation of the magnetic fields and luminosities of the icy giants, those components need to be characterised at planetary conditions (some Mbar and a few $10^3$ K). Those conditions are typical of the Warm Dense Matter regime, which exhibits a rich phase diagram, with the coexistence of many states of matter and a large variety of chemical processes. H$_2$O, C:H:O, and C:H:N:O mixtures have been compressed up to 2.8 Mbar along the principal Hugoniot using laser-driven decaying shocks. The experiments were performed at the GEKKO XII and LULI 2000 laser facilities using standard optical diagnostics (Doppler velocimetry and pyrometry) to characterise equation of state and optical reflectivity of the shocked states. The results show that H$_2$O and the C:H:N:O mixture share the same equation of state with a density scaling, while the reflectivity behaves differently by what concerns both the onset pressures and the saturation values. The reflectivity measurement at two frequencies allows to estimate the conductivity and the complex refractive index using a Drude model.
△ Less
Submitted 18 April, 2018;
originally announced April 2018.
-
Laboratory radiative accretion shocks on GEKKO XII laser facility for POLAR project
Authors:
L. Van Box Som,
E. Falize,
M. Koenig,
Y. Sakawa,
B. Albertazzi,
P. Barroso,
J. -M. Bonnet-Bidaud,
C. Busschaert,
A. Ciardi,
Y. Hara,
N. Katsuki,
R. Kumar,
F. Lefevre,
C. Michaut,
Th. Michel,
T. Miura,
T. Morita,
M. Mouchet,
G. Rigon,
T. Sano,
S. Shiiba,
H. Shimogawara,
S. Tomiya
Abstract:
A new target design is presented to model high-energy radiative accretion shocks in polars. In this paper, we present the experimental results obtained on the GEKKO XII laser facility for the POLAR project. The experimental results are compared with 2D FCI2 simulations to characterize the dynamics and the structure of plasma flow before and after the collision. The good agreement between simulatio…
▽ More
A new target design is presented to model high-energy radiative accretion shocks in polars. In this paper, we present the experimental results obtained on the GEKKO XII laser facility for the POLAR project. The experimental results are compared with 2D FCI2 simulations to characterize the dynamics and the structure of plasma flow before and after the collision. The good agreement between simulations and experimental data confirm the formation of a reverse shock where cooling losses start modifying the post-shock region. With the multi-material structure of the target, a hydrodynamic collimation is exhibited and a radiative structure coupled with the reverse shock is highlighted in both experimental data and simulations. The flexibility on the laser energy produced on GEKKO XII, allowed us to produce high-velocity flows and study new and interesting radiation hydrodynamic regimes between those obtained on the LULI2000 and Orion laser facilities.
△ Less
Submitted 8 April, 2018;
originally announced April 2018.
-
Miniature shock tube for laser driven shocks
Authors:
Michel Busquet,
Patrice Barroso,
Thierry Melse,
Daniel Bauduin
Abstract:
We describe in this paper the design of a miniature shock tube (smaller than 1 cm3) that can be placed in a vacuum vessel and allows transverse optical probing and longitudinal backside XUV emission spectroscopy. Typical application is the study of laser launched radiative shocks, in the framework of what is called "laboratory Astrophysics".
We describe in this paper the design of a miniature shock tube (smaller than 1 cm3) that can be placed in a vacuum vessel and allows transverse optical probing and longitudinal backside XUV emission spectroscopy. Typical application is the study of laser launched radiative shocks, in the framework of what is called "laboratory Astrophysics".
△ Less
Submitted 11 May, 2010;
originally announced May 2010.
-
Experimental study of radiative shocks at PALS facility
Authors:
Chantal Stehlé,
Matthias González,
Michaela Kozlova,
Bedrich Rus,
Tomas Mocek,
Ouali Acef,
Jean-Philippe Colombier,
Thierry Lanz,
Norbert Champion,
Krzysztof Jakubczak,
Jiri Polan,
Patrice Barroso,
Daniel Bauduin,
Edouard Audit,
Jan Dostal,
Michal Stupka
Abstract:
We report on the investigation of strong radiative shocks generated with the high energy, sub-nanosecond iodine laser at PALS. These shock waves are characterized by a developed radiative precursor and their dynamics is analyzed over long time scales (~50 ns), approaching a quasi-stationary limit. We present the first preliminary results on the rear side XUV spectroscopy. These studies are relevan…
▽ More
We report on the investigation of strong radiative shocks generated with the high energy, sub-nanosecond iodine laser at PALS. These shock waves are characterized by a developed radiative precursor and their dynamics is analyzed over long time scales (~50 ns), approaching a quasi-stationary limit. We present the first preliminary results on the rear side XUV spectroscopy. These studies are relevant to the understanding of the spectroscopic signatures of accretion shocks in Classical T Tauri Stars.
△ Less
Submitted 13 March, 2010;
originally announced March 2010.
