bluuebunny/crossref_metadata_2025_split huggingface dataset:
Abundant Dislocation Layered Double Hydroxides Synthesis by Molten Salt with Bound Water Boosting Oxygen Evolution
Authors: Chen Yi , Li Yuwen , Cui Yuanjing , Qian Guodong 
Published: August 2022

AbstractOptimizing the adsorption free energy and promoting the active phase transition to further enhance the oxygen evolution reaction (OER) activity remain significant challenges. The adsorption free energy can be optimized by modulating the electronic structure and adjusting the crystal configuration. Meanwhile, the transformation of the active phase can be promoted by introducing strain energy. The theoretical calculations are conducted to verify the rational envisage. However, it is still a great obstacle to introducing strain into the electrocatalysts and avoiding destruction. The stress field caused by dislocation can realize both of the above. Hence, the molten salt with the bound water method is proposed and the abundant dislocation layered double hydroxides (D‐NiFe LDH) are constructed. The in situ characterizations further verify the dislocations significantly affect the generation of the active phase and the state of electronic structure. Consequently, the D‐NiFe LDH exhibits outstanding OER activity and obtains 10 mA cm−2, only requiring 199 mV overpotential with fabulous stability (100 mA cm−2 more than 24 h). The work paves a new avenue for the rational introduction dislocations to optimize the crystal configuration and boost the active phase formation, significantly enhancing the OER performance.
Facile Synthesis of Conductive Metal−Organic Frameworks Nanotubes for Ultrahigh‐Performance Flexible NO Sensors
Authors: Wang Liangjie , Chen Xin , Yi Zhengran , Xu Rui , Dong Junjie , Wang Shuai , Zhao Yan , Liu Yunqi 
Published: August 2022

AbstractCu‐benzenehexathiol (Cu‐BHT) has attracted significant attention due to its record high electrical conductivity and crystal defects Cu2c. However, the nonporous structure and small specific surface area of Cu‐BHT with two‐dimensional kagome lattice invariably limit its practical application in sensing and catalysis. In this work, Cu‐BHT nanotubes (Cu‐BHT‐NTs) are designed and prepared via a facile homogeneous reaction to solve these problems. Compared with the traditional nanorod‐like structure, the Cu‐BHT‐NTs not only have a higher specific surface area but also possess a higher proportion of crystal defects (66.6%). The successfully configured DPPTT/Cu‐BHT‐NTs heterostructure organic field‐effect transistor (OFET)‐based sensor exhibits excellent sensitivity as high as 13 610%, a minimum detection limits down to 5 ppb, and exceptional selectivity to nitric oxide (NO) toxic gases. Theoretical analysis systematically shows that Cu2c sites in the Cu‐BHT‐NTs increase the number of electrons transferred from the heterostructure to NO molecules, confirming that the high sensitivity and selectivity result from the high binding between Cu‐BHT‐NTs and NO molecules. Furthermore, a fully flexible device based on the heterojunction OFET sensor is prepared to ensure the convenience of wearing and carrying gas sensors, opening up a new avenue for the next generation of wearable intelligent electronics.
Chaotic neural networks and farfalle construction based parallel keyed secure hash function
Authors: Belal Mohamad Mulham , Maitra Tanmoy , Giri Debasis , Das Ashok Kumar 
Published: August 2022

AbstractParallel computing of hash functions along with the security requirements have great advantage in order to reduce the time consumption and overhead of the CPU. In this article, a keyed hash function based on farfalle construction and chaotic neural networks (CNNs) is proposed, which generates a hash value with arbitrary (defined by user) length (eg, 256 and 512 bits). The proposed hash function has parallelism merit because it is built over farfalle construction which avoids the dependency between the blocks of a given message. Moreover, the proposed hash function is chaos based (ie, it relies on chaotic maps and CNNs which have non‐periodic behavior). The security analysis shows that the proposed hash function is robust and satisfies the properties of hash algorithms, such as random‐like (non‐periodic) behavior, ideal sensitivity to original message and secret key, one‐way property and optimal diffusion effect. The speed performance of the hash function is also analyzed and compared with a hash function which was built based on sponge construction and CNN, and compared with secure hash algorithm (SHA) variants like SHA‐2 and SHA‐3. The results have shown that the proposed hash function has lower time complexity and higher throughput especially with large size messages. Additionally, the proposed hash function has enough resistance to multiple attacks, such as collision attack, birthday attack, exhaustive key search attack, preimage and second preimage attacks, and meet‐in‐the‐middle attack. These advantages make it ideal to be used as a good collision‐resistant hash function.
Effect of superabsorbent polymers on mechanical strength and cracking of mortar and concrete with water to cement ratios of 0.4 and 0.5
Authors: Borito Said Mirgan , Zhu Han , Yu Yong , Al‐shawafi Ali 
Published: August 2022

AbstractMost studies of adding superabsorbent polymers (SAP) into concrete focus on high‐strength concrete, while this paper aims to understand the influence of SAP on “ordinary concrete” at a w/c ratio being 0.4 or 0.5. The proposed experiments include the effect of particle size, mixing methods, and dosages on the restrained shrinkage and mechanical properties of mortar and concrete. Mortar with varying dosages of SAP (0.1, 0.2, and 0.3 wt.%) and two types of SAP (type‐a of 30–60 mesh and type‐d of 300–400 mesh) was studied to evaluate the effect of SAP on mortar's cracking and strength. Two mixing processes of SAP (dry and pre‐wetted) were used to examine the effect of SAP on the mortar's shrinkage and mechanical properties. Furthermore, concrete specimens with a w/c ratio of 0.5 were prepared to investigate the cracking performance of concrete using the restrained squared concentric ring test method, a new approach which can predict the cracks location and pattern to evaluate the restrained shrinkage of concrete. The result revealed that the addition of SAP in a prewetted state decreased the mechanical properties at early curing age. The addition of 0.3 wt.% SAP was found to have mitigated the restrained shrinkage while prolonging the time to cracking of cementitious composites. The major finding is that adding SAP to ordinary concrete reduces shrinkage and improves mechanical strength, which should be further looked into and explored in its application in engineering work.
Corporate social responsibility in the water industry: A critical review
Authors: Figueroa Cindy , Lee Kyungsun , Jepson Wendy 
Published: August 2022

AbstractThe public demand for companies to assume responsibility for social and environmental impacts of their operations has led to an increase in the number of industries adopting corporate social responsibility (CSR) strategies. The water industry, defined in this article as public and private suppliers of water, holds the unique responsibility to manage a critical natural resource. As such, a review of scholarship on CSR in the water industry provides an entry point to assess the specific role the water industry plays in addressing societal and environmental concerns. This review identifies three prominent themes that appear in the existing literature. The first theme investigates the motivations for the water industry to utilize CSR strategies; the second describes the limitations of current CSR frameworks; and the last is an assessment of whether CSR policies and practices differ between public and private water companies. Through a critical review of each theme, this article evaluates the level of CSR engagement in the water industry, and if CSR activity supports further privatization. Taken together, this review article provides a summary of the current state of research on CSR within the water industry, analyses limitations on current evaluation methods and frameworks, and connects the literature to broader themes on the privatization of water and market environmentalism. We conclude with a discussion of future research topics such as CSR barriers to implementation, water‐related CSR indicators, and the relationship of CSR policies to remunicipalization of water providers.This article is categorized under:
Human Water > Water Governance
A Billion SMT Queries a Day (Invited Paper)
Authors: Rungta Neha 
Published: August 2022

AbstractAmazon Web Services (AWS) is a cloud computing services provider that has made significant investments in applying formal methods to proving correctness of its internal systems and providing assurance of correctness to their end-users. In this paper, we focus on how we built abstractions and eliminated specifications to scale a verification engine for AWS access policies, Zelkova, to be usable by all AWS users. We present milestones from our journey from a thousand SMT invocations daily to an unprecedented billion SMT calls in a span of five years. In this paper, we talk about how the cloud is enabling application of formal methods, key insights into what made this scale of a billion SMT queries daily possible, and present some open scientific challenges for the formal methods community.
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Authors: Kori Mayuko , Urabe Natsuki , Katsumata Shin-ya , Suenaga Kohei , Hasuo Ichiro 
Published: August 2022

AbstractWe present LT-PDR, a lattice-theoretic generalization of Bradley’s property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious combination of verification and refutation attempts based on the Knaster–Tarski and Kleene theorems. We introduce four concrete instances of LT-PDR, derive their implementation from a generic Haskell implementation of LT-PDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances.
Software Verification of Hyperproperties Beyond k-Safety
Authors: Beutner Raven , Finkbeiner Bernd 
Published: August 2022

AbstractTemporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (infinite-state) software, the analysis of temporal hyperproperties has, so far, been limited tok-safety properties, i.e., properties that stipulate the absence of a bad interaction between anyktraces. In this paper, we present an automated method for the verification of$$\forall ^k\exists ^l$$∀k∃l-safety properties in infinite-state systems. A$$\forall ^k\exists ^l$$∀k∃l-safety property stipulates that for anyktraces, thereexistltraces such that the resulting$$k+l$$k+ltraces do not interact badly. This combination of universal and existential quantification enables us to express many properties beyondk-safety, including, for example, generalized non-interference or program refinement. Our method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction. Notably, our framework allows for mutual dependence of strategy and reduction.
PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party Computation
Authors: Fan Yuxin , Song Fu , Chen Taolue , Zhang Liangfeng , Liu Wanwei 
Published: August 2022

AbstractSecure multi-party computation (MPC) is a promising technique for privacy-persevering applications. A number of MPC frameworks have been proposed to reduce the burden of designing customized protocols, allowing non-experts to quickly develop and deploy MPC applications. To improve performance, recent MPC frameworks allow users to declare variables secret only for these which are to be protected. However, in practice, it is usually highly non-trivial for non-experts to specify secret variables: declaring too many degrades the performance while declaring too less compromises privacy. To address this problem, in this work we propose an automated security policy synthesis approach to declare as few secret variables as possible but without compromising security. Our approach is a synergistic integration of type inference and symbolic reasoning. The former is able to quickly infer a sound—but sometimes conservative—security policy, whereas the latter allows to identify secret variables in a security policy that can be declassified in a precise manner. Moreover, the results from symbolic reasoning are fed back to type inference to refine the security types even further. We implement our approach in a new tool PoS4MPC. Experimental results on five typical MPC applications confirm the efficacy of our approach.
Program Verification with Constrained Horn Clauses (Invited Paper)
Authors: Gurfinkel Arie 
Published: August 2022

AbstractMany problems in program verification, Model Checking, and type inference are naturally expressed as satisfiability of a verification condition expressed in a fragment of First-Order Logic called Constrained Horn Clauses (CHC). This transforms program analysis and verification tasks to the realm of first order satisfiability and into the realm of SMT solvers. In this paper, we give a brief overview of how CHCs capture verification problems for sequential imperative programs, and discuss CHC solving algorithm underlying the Spacer engine of SMT-solver Z3.
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Authors: Banno Ryotaro , Matsuoka Kotaro , Matsumoto Naoki , Bian Song , Waga Masaki , Suenaga Kohei 
Published: August 2022

AbstractIn many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct oblivious online monitoring—online monitoring conducted without revealing the private information of each party to the other—against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring with the DFA. Based on fully homomorphic encryption (FHE), we propose two online algorithms (Reverse and Block) to run a DFA obliviously. We prove the correctness and security of our entire protocol. We also show the scalability of our algorithms theoretically and empirically. Our case study shows that our algorithms are fast enough to monitor blood glucose levels online, demonstrating our protocol’s practical relevance.
RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
Authors: Goubault Eric , Putot Sylvie 
Published: August 2022

AbstractWe present a unified approach, implemented in the RINO tool, for the computation of inner and outer-approximations of reachable sets of discrete-time and continuous-time dynamical systems, possibly controlled by neural networks with differentiable activation functions. RINO combines a zonotopic set representation with generalized mean-value AE extensions to compute under and over-approximations of the robust range of differentiable functions, and applies these techniques to the particular case of learning-enabled dynamical systems. The AE extensions require an efficient and accurate evaluation of the function and its Jacobian with respect to the inputs and initial conditions. For continuous-time systems, possibly controlled by neural networks, the function to evaluate is the solution of the dynamical system. It is over-approximated in RINO using Taylor methods in time coupled with a set-based evaluation with zonotopes. We demonstrate the good performances of RINO compared to state-of-the art tools Verisig 2.0 and ReachNN* on a set of classical benchmark examples of neural network controlled closed loop systems. For generally comparable precision to Verisig 2.0 and higher precision than ReachNN*, RINO is always at least one order of magnitude faster, while also computing the more involved inner-approximations that the other tools do not compute.
Data-Driven Invariant Learning for Probabilistic Programs
Authors: Bao Jialu , Trivedi Nitesh , Pathak Drashti , Hsu Justin , Roy Subhajit 
Published: August 2022

AbstractMorgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task.We propose a new view of invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. Guided by this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach can learn piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper- or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature.
Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
Authors: Chatterjee Krishnendu , Goharshady Amir Kafshdar , Meggendorfer Tobias , Žikelić Đorđe 
Published: August 2022

AbstractWe consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold $$p \in [0, 1],$$

p
∈
[
0
,
1
]
,

we aim for certificates proving that the program terminates with probability at least $$1-p$$

1
-
p

. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset $$ SI $$

SI

of program states such that (i) the probability of the program ever leaving $$ SI $$

SI

is no more than p, and (ii) almost-surely, the program either leaves $$ SI $$

SI

or terminates.While stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.Our prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods.
Example Guided Synthesis of Linear Approximations for Neural Network Verification
Authors: Paulsen Brandon , Wang Chao 
Published: August 2022

AbstractLinear approximations of nonlinear functions have a wide range of applications such as rigorous global optimization and, recently, verification problems involving neural networks. In the latter case, a linear approximation must be hand-crafted for the neural network’s activation functions. This hand-crafting is tedious, potentially error-prone, and requires an expert to prove the soundness of the linear approximation. Such a limitation is at odds with the rapidly advancing deep learning field – current verification tools either lack the necessary linear approximation, or perform poorly on neural networks with state-of-the-art activation functions. In this work, we consider the problem of automatically synthesizing sound linear approximations for a given neural network activation function. Our approach is example-guided: we develop a procedure to generate examples, and then we leverage machine learning techniques to learn a (static) function that outputs linear approximations. However, since the machine learning techniques we employ do not come with formal guarantees, the resulting synthesized function may produce linear approximations with violations. To remedy this, we bound the maximum violation using rigorous global optimization techniques, and then adjust the synthesized linear approximation accordingly to ensure soundness. We evaluate our approach on several neural network verification tasks. Our evaluation shows that the automatically synthesized linear approximations greatly improve the accuracy (i.e., in terms of the number of verification problems solved) compared to hand-crafted linear approximations in state-of-the-art neural network verification tools. An artifact with our code and experimental scripts is available at: https://zenodo.org/record/6525186#.Yp51L9LMIzM.
"Image missing""Image missing"
Verifying Neural Networks Against Backdoor Attacks
Authors: Pham Long H. , Sun Jun 
Published: August 2022

AbstractNeural networks have achieved state-of-the-art performance in solving many problems, including many applications in safety/security-critical systems. Researchers also discovered multiple security issues associated with neural networks. One of them is backdoor attacks, i.e., a neural network may be embedded with a backdoor such that a target output is almost always generated in the presence of a trigger. Existing defense approaches mostly focus on detecting whether a neural network is ‘backdoored’ based on heuristics, e.g., activation patterns. To the best of our knowledge, the only line of work which certifies the absence of backdoor is based on randomized smoothing, which is known to significantly reduce neural network performance. In this work, we propose an approach to verify whether a given neural network is free of backdoor with a certain level of success rate. Our approach integrates statistical sampling as well as abstract interpretation. The experiment results show that our approach effectively verifies the absence of backdoor or generates backdoor triggers.