Search

Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with finite traces only. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a progress condition, and prove that this progressive forward simulation does imply strong observational refinement., LIPIcs, Vol. 209, 35th International Symposium on Distributed Computing (DISC 2021), pages 55:1-55:4

Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki-Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g., reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by showing Nipkow and Nieto's encoding of Owicki-Gries in the Isabelle theorem prover can be extended to handle C11-style weak memory models in a straightforward manner. We exemplify our techniques over several litmus tests from the literature and a non-trivial example: Peterson's algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.

This note relates axioms for partial semigroups and monoids with those for small object-free categories, either with multiple monoidal units or with source and target maps. We discuss the adjunction of a zero element to both kinds of category and provide examples that separate the algebras considered.

Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover Isabelle., LIPIcs, Vol. 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020), pages 11:1-11:26

The paper "Owicki-Gries Reasoning for C11 RAR" introduces a new proof calculus for the C11 RAR memory model that allows Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. The proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. The artifact includes the Isabelle formalisation of the proof method introduced in the paper. It also contains the formalisation and proof of all case studies presented in the paper. All of the theorems are accompanied with their respective proofs., DARTS, Vol. 6, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020), pages 15:1-15:2

Hydrochlorofluorocarbons (HCFCs) are the first, but temporary, substitution products for the strong ozone-depleting chlorofluorocarbons (CFCs). HCFC consumption and production are currently regulated under the Montreal Protocol on Substances that Deplete the Ozone Layer and their emissions have started to stabilize or even decrease. As HCFC-22 (CHClF2) is by far the most abundant HCFC in today's atmosphere, it is crucial to continue to monitor the evolution of its atmospheric concentration. In this study, we describe an improved HCFC-22 retrieval strategy from ground-based high-resolution Fourier transform infrared (FTIR) solar spectra recorded at the high-altitude scientific station of Jungfraujoch, the Swiss Alps, 3580 m a.m.s.l. (above mean sea level). This new strategy distinguishes tropospheric and lower-stratospheric partial columns. Comparisons with independent datasets, such as the Advanced Global Atmospheric Gases Experiment (AGAGE) and the Michelson Interferometer for Passive Atmospheric Sounding (MIPAS), supported by models, such as the Belgian Assimilation System for Chemical ObErvation (BASCOE) and the Whole Atmosphere Community Climate Model (WACCM), demonstrate the validity of our tropospheric and lower-stratospheric long-term time series. A trend analysis on the datasets used here, now spanning 30 years, confirms the last decade's decline in the HCFC-22 growth rate. This updated retrieval strategy can be adapted for other ozone-depleting substances (ODSs), such as CFC-12. Measuring or retrieving ODS atmospheric concentrations is essential for scrutinizing the fulfilment of the globally ratified Montreal Protocol.

We present a compact and versatile cryofocusing–thermodesorption unit, which we developed for quantitative analysis of halogenated trace gases in ambient air. Possible applications include aircraft-based in situ measurements, in situ monitoring and laboratory operation for the analysis of flask samples. Analytes are trapped on adsorptive material cooled by a Stirling cooler to low temperatures (e.g. −80 °C) and subsequently desorbed by rapid heating of the adsorptive material (e.g. +200 °C). The set-up involves neither the exchange of adsorption tubes nor any further condensation or refocusing steps. No moving parts are used that would require vacuum insulation. This allows for a simple and robust design. Reliable operation is ensured by the Stirling cooler, which neither contains a liquid refrigerant nor requires refilling a cryogen. At the same time, it allows for significantly lower adsorption temperatures compared to commonly used Peltier elements. We use gas chromatography – mass spectrometry (GC–MS) for separation and detection of the preconcentrated analytes after splitless injection. A substance boiling point range of approximately −80 to +150 °C and a substance mixing ratio range of less than 1 ppt (pmol mol−1) to more than 500 ppt in preconcentrated sample volumes of 0.1 to 10 L of ambient air is covered, depending on the application and its analytical demands. We present the instrumental design of the preconcentration unit and demonstrate capabilities and performance through the examination of analyte breakthrough during adsorption, repeatability of desorption and analyte residues in blank tests. Examples of application are taken from the analysis of flask samples collected at Mace Head Atmospheric Research Station in Ireland using our laboratory GC–MS instruments and by data obtained during a research flight with our in situ aircraft instrument GhOST-MS (Gas chromatograph for the Observation of Tracers – coupled with a Mass Spectrometer).

Palladium nanoparticles stabilized by heteroatom donor‐modified polystyrene‐based polymer immobilized ionic liquids (PdNP@HAD‐PIILP; HAD‐PPh2, OMe, NH2, CN, pyrrolidone) are highly efficient catalysts for the Suzuki‐Miyaura cross‐coupling in aqueous media under mild conditions. Catalyst modified with phosphine was consistently the most efficient as it gave high yields across a range of substrates under mild conditions at low catalyst loadings. Incorporation of polyethylene glycol into the phosphine modified immobilised ionic liquid support improved catalyst efficacy by improving dispersibility and facilitating access to the active site. Moreover, each of the heteroatom modified catalysts was more active than the corresponding unsubstituted imidazolium‐based polystyrene benchmark as well as commercial samples of Pd/C. Catalyst generated in situ from either [PdCl4]@PPh2‐PIILP or its PEGylated counterpart [PdCl4]@PPh2‐PEGPIILP, by reduction with phenylboronic acid, outperformed their pre‐formed counterparts for the vast majority of substrates examined. The turnover frequency of 16,300 h−1 obtained at room temperature is one of the highest to be reported for palladium nanoparticle‐catalysed Suzuki‐Miyaura cross‐coupling between 4‐bromoacetophenone and phenylboronic acid in aqueous media under such mild conditions.

In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only partially ordered, as in many weak-memory models that describe multicore memory systems. In this paper, we present causal linearizability, a correctness condition for concurrent objects implemented in weak-memory models. We abstract from the details of specific memory models by defining our condition using Lamport's execution structures. We apply our condition to the C11 memory model, providing a correctness condition for C11 objects. We develop a proof method for verifying objects implemented in C11 and related models. Our method is an adaptation of simulation-based methods, but in contrast to other such methods, it does not require that the implementation totally order its events. We also show that causal linearizability reduces to linearizability in the totally ordered case.

Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.

Phosphino-decorated polymer immobilised ionic liquid phase stabilised palladium nanoparticles (PdNP@PPh2-PIILP) and their PEGylated counterparts (PdNP@PPh2-PEGPIILP) are remarkably active and exceptionally selective catalysts for the aqueous phase hydrogenation of α,β-unsaturated aldehydes, ketones, esters and nitriles with PdNP@PPh2-PEGPIILP giving complete conversion and 100% selectivity for reduction of the C[double bond, length as m-dash]C bond, under mild conditions. This is the most selective PdNP-based system to be reported for the aqueous phase hydrogenation of this class of substrates.

Changes of atmospheric methane total columns (CH4) since 2005 have been evaluated using Fourier transform infrared (FTIR) solar observations carried out at 10 ground-based sites, affiliated to the Network for Detection of Atmospheric Composition Change (NDACC). From this, we find an increase of atmospheric methane total columns of 0.31 ± 0.03 % year−1 (2σ level of uncertainty) for the 2005–2014 period. Comparisons with in situ methane measurements at both local and global scales show good agreement. We used the GEOS-Chem chemical transport model tagged simulation, which accounts for the contribution of each emission source and one sink in the total methane, simulated over 2005–2012. After regridding according to NDACC vertical layering using a conservative regridding scheme and smoothing by convolving with respective FTIR seasonal averaging kernels, the GEOS-Chem simulation shows an increase of atmospheric methane total columns of 0.35 ± 0.03 % year−1 between 2005 and 2012, which is in agreement with NDACC measurements over the same time period (0.30 ± 0.04 % year−1, averaged over 10 stations). Analysis of the GEOS-Chem-tagged simulation allows us to quantify the contribution of each tracer to the global methane change since 2005. We find that natural sources such as wetlands and biomass burning contribute to the interannual variability of methane. However, anthropogenic emissions, such as coal mining, and gas and oil transport and exploration, which are mainly emitted in the Northern Hemisphere and act as secondary contributors to the global budget of methane, have played a major role in the increase of atmospheric methane observed since 2005. Based on the GEOS-Chem-tagged simulation, we discuss possible cause(s) for the increase of methane since 2005, which is still unexplained.

Most work on the verification of concurrent objects for shared memory assumes sequential consistency, but most multicore processors support only weak memory models that do not provide sequential consistency. Furthermore, most verification efforts focus on the linearizability of concurrent objects, but there are existing implementations optimized to run on weak memory models that are not linearizable. In this paper, we address these problems by introducing causal linearizability, a correctness condition for concurrent objects running on weak memory models. Like linearizability itself, causal linearizability enables concurrent objects to be composed, under weak constraints on the client's behaviour. We specify these constraints by introducing a notion of operation-race freedom, where programs that satisfy this property are guaranteed to behave as if their shared objects were in fact linearizable. We apply these ideas to objects from the Linux kernel, optimized to run on TSO, the memory model of the x86 processor family., Full version of submission to SEFM 2016

International audience; Vaccination procedures within the cattle industry are important disease control tools to minimize economic and welfare burdens associated with respiratory pathogens. However, new vaccine, antigen and carrier technologies are required to combat emerging viral strains and enhance the efficacy of respiratory vaccines, particularly at the point of pathogen entry. New technologies, specifically metabolomic profiling, could be applied to identify metabolite immune-correlates representative of immune protection following vaccination aiding in the design and screening of vaccine candidates. This study for the first time demonstrates the ability of untargeted UPLC-MS metabolomic profiling to identify metabolite immune correlates characteristic of immune responses following mucosal vaccination in calves. Male Holstein Friesian calves were vaccinated with Pfizer Rispoval® PI3 + RSV intranasal vaccine and metabolomic profiling of post-vaccination plasma revealed 12 metabolites whose peak intensities differed significantly from controls. Plasma levels of glycocholic acid, N-[(3α,5β,12α)-3,12-Dihydroxy-7,24-dioxocholan-24-yl]glycine, uric acid and biliverdin were found to be significantly elevated in vaccinated animals following secondary vaccine administration, whereas hippuric acid significantly decreased. In contrast, significant upregulation of taurodeoxycholic acid and propionylcarnitine levels were confined to primary vaccine administration. Assessment of such metabolite markers may provide greater information on the immune pathways stimulated from vaccine formulations and benchmarking early metabolomic responses to highly immunogenic vaccine formulations could provide a means for rapidly assessing new vaccine formulations. Furthermore, the identification of metabolic systemic immune response markers which relate to specific cell signaling pathways of the immune system could allow for targeted vaccine design to stimulate key pathways which can be assessed at the metabolic level.