bluuebunny/crossref_metadata_2025_split huggingface dataset:
Polyurethane‐based nanocomposite for catalytic reduction of toxic dyes
Authors: Naseem Khalida , Abrar Eman , Haider Sajjad , Alam Kamran 
Published: April 2024

AbstractIn this work, we prepared AuNPs loaded polyurethane‐sodium alginate (Au‐PU‐ALg) composite polymers by casting and in‐situ reduction method. Successful fabrication of AuNPs was confirmed by UV–visible, Fourior transform infrared (FTIR) spectroscopy, X‐ray diffraction (XRD), field emission scanning elcetron microscopy (FESEM), and energy dispersive X‐ray (EDX) analysis along with the change in color of the suspension from yellow to dark purple. Thermo‐gravimetric analysis (TGA) also confirmed the loading of 7.44 % AuNPs of total nanocomposite contents. The catalytic activity of Au‐PU‐ALg nanocomposites was checked by reducing Rhodamine B (RhB) as a model reaction. It was seen that reduction of RhB was successfully done in the presence of NaBH4 and Au‐PU‐ALg nanocomposite in just 8 min with value of kapp found as 0.648 min−1. While the value of kapp for RhB reduction was found as 0.0008, 0.00221, and 0.0008 min−1 in the presence of catalyst, NaBH4 and polymer gel particles, respectively. Thus results show that the value of kapp for the reduction of RhB in the presence of NaBH4 and catalyst was found high as compared to the controlled reactions. Complex mixture of dyes such as RhB, crystal violet (CV), Congo red (CR), and dyes polluted industrial wastewater was become colorless in 10 and 3 min, respectively on mixing with catalyst and reducing agent. It was also observed that reduction of RhB followed pseudo first order kinetic model and Langmuir Hinshelwood mechanism.
Robust fault‐tolerant cooperative control for a class of interconnected systems with actuator faults based on dynamic event‐triggered
Authors: Wang Ke , Sun Chao , Huang Shengjuan , Wu Libing , Yi Suhuan 
Published: April 2024

AbstractIn this paper, the problem of fault estimation (FE) and fault‐tolerant control (FTC) for a class of systems with dynamic event‐triggered mechanism (ETM) and time delay in a network environment is studied. To shorten the time between events and minimize the amount of data transmitted, this paper introduces dynamic variables within the ETM. In order to ensure the interval between the system state and its estimation, a fault/state estimation observer considering time delay is designed, which improves the reliability and security of the system. On this basis, a fault‐tolerant controller considering time delay is constructed to compensate the impact of faults on the system. The observer, controller, and ETM are co‐designed to maintain system performance. By making full use of the information between subsystems, a continuous time interconnection systems is constructed and the cooperative control mechanism is redesigned on the basis of the above system. Through theoretical analysis, it has been demonstrated that Zeno phenomenon does not exist in the ETM in this paper. Finally, the main results are verified by numerical simulation, and the validity of the conclusions is demonstrated.
Liquid homeownership: Navigating future horizons to turn homeownership into assets in Bucharest, Romania
Authors: Ciocanel Alexandra 
Published: April 2024

AbstractThis article examines the financialization and assetization of housing in an Eastern European context by focusing on the specific temporally bounded financial strategies to maintain housing as an asset and vehicle for social reproduction. It proposes the concept of liquid homeownership to account for the varied associations of housing with liquidity and the expectations of future increased exchange value that play an essential role in shaping financial decisions in the present. Drawing on ethnographic research in Bucharest, the article argues that upper‐middle‐class mortgage borrowers strategize their leveraged housing investment by navigating between two future horizons. To ensure that housing is an asset in the long term, mortgage borrowers prefer to evacuate the long‐term of the mortgage contract through medium‐term financial strategies of early repayment. Given the importance attributed to future liquidity from homeownership for providing for old age or securing children's future, the article argues that liquid homeownership, at least for ordinary homebuyers, is a reflection less of short‐term financial interest and more of a long‐term social reproduction need, pointing to the complex intermix of financial calculations and domestic concerns in the context of financialization of housing.
2D Memory Selectors with Giant Nonlinearity Enabled by Van der Waals Heterostructures
Authors: Wang Xiaofan , Qiao Ruixi , Lu Huan , He Weiwei , Liu Ying , Zhou Tao , Wan Dongyang , Wang Qin , Liu Yanpeng , Guo Wanlin 
Published: April 2024

AbstractThe integration of one‐selector‐one‐resistor crossbar arrays requires the selectors featured with high nonlinearity and bipolarity to prevent leakage currents and any crosstalk among distinct cells. However, a selector with sufficient nonlinearity especially in the frame of device miniaturization remains scarce, restricting the advance of high‐density storage devices. Herein, a high‐performance memory selector is reported by constructing a graphene/hBN/WSe2heterostructure. Within the temperature range of 300–80 K, the nonlinearity of this selector varies from ≈103 – ≈104under forward bias, and increases from ≈300 – ≈105under reverse bias, the highest reported nonlinearity among 2D selectors. This improvement is ascribed to direct tunneling at low bias and Fowler–Nordheim tunneling at high bias. The tunneling current versus voltage curves exhibit excellent bipolarity behavior because of the comparable hole and electron tunneling barriers, and the charge transport polarity can be effectively tuned from N‐type or P‐type to bipolar by simply changing source‐drain bias. In addition, the conceptual memory selector exhibits no sign of deterioration after 70 000 switching cycles, paving the way for assembling 2D selectors into modern memory devices.
A Highly Robust and Conducting Ultramicroporous 3D Fe(II)‐Based Metal–Organic Framework for Efficient Energy Storage
Authors: Khan Soumen , Chand Santanu , Sivasakthi Pandiyan , Samanta Pralok K. , Chakraborty Chanchal 
Published: April 2024

AbstractExploitation of metal–organic framework (MOF) materials as active electrodes for energy storage or conversion is reasonably challenging owing to their poor robustness against various acidic/basic conditions and conventionally low electric conductivity. Keeping this in perspective, herein, a 3D ultramicroporous triazolate Fe‐MOF (abbreviated as Fe‐MET) is judiciously employed using cheap and commercially available starting materials. Fe‐MET possesses ultra‐stability against various chemical environments (pH‐1 to pH‐14 with varied organic solvents) and is highly electrically conductive (σ = 0.19 S m−1) in one fell swoop. By taking advantage of the properties mentioned above, Fe‐MET electrodes give prominence to electrochemical capacitor (EC) performance by delivering an astounding gravimetric (304 F g−1) and areal (181 mF cm−2) capacitance at 0.5 A g−1 current density with exceptionally high cycling stability. Implementation of Fe‐MET as an exclusive (by not using any conductive additives) EC electrode in solid‐state energy storage devices outperforms most of the reported MOF‐based EC materials and even surpasses certain porous carbon and graphene materials, showcasing superior capabilities and great promise compared to various other alternatives as energy storage materials.
A Comprehensive Specification and Verification of the L4 Microkernel API
Authors: Zhang Leping , Zhao Yongwang , Li Jianxin 
Published: April 2024

AbstractThe L4 API (Application Programming Interface) is a core component of the operating system, which serves as the interface between user-level processes and the microkernel, facilitating communication and interaction. It is crucial to ensure the correctness and reliability of the API. This paper proposes a comprehensive formal specification and verification for the L4 microkernel API. The specification is reusable for all implementations on architectures supported by the microkernel. To further improve reusability (e.g., for the L4 family), a parameterized model is abstracted, which mainly includes variables related to L4 components and safety properties built on them. The desired properties are composed of 350 functional correctness and 39 safety properties, where the safety properties cover existing invariants of the microkernel. Several rewriting rules and reasoning steps are proposed for verification to improve proof efficiency. The proofs of the specification w.r.t these properties are accomplished in the theorem prover Isabelle/HOL, and the results show that all definitions, lemmas, and proofs pass the prover’s check. During modeling and verification, 10 bugs in the source code are found, all of which are fixed in this paper.
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
Authors: Mertens Hannah , Katoen Joost-Pieter , Quatmann Tim , Winkler Tobias 
Published: April 2024

AbstractWe study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration and topological approaches known from the computation of reachability probabilities and expected rewards. We further study applications of expected visiting times, including the sound computation of the stationary distribution and expected rewards conditioned on reaching multiple goal states. The implementation of our methods in the probabilistic model checker scales to large systems with millions of states. Our experiments on the quantitative verification benchmark set show that the computation of stationary distributions via expected visiting times consistently outperforms existing approaches — sometimes by several orders of magnitude.
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation
Authors: Lin Shang-Wei , Wang Tzu-Fan , Chen Yean-Ru , Hou Zhe , Sanán David , Teo Yon Shin 
Published: April 2024

AbstractBoolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover’s algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexityO(m), linear to the number of clausesm,per Grover iteration. In this work, we develop aparallelquantum SAT solver, which reduces the time complexity in each iteration to constant timeO(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We prove the correctness of our approaches and evaluate them in simulations and real quantum computers.
Scalable Tree-based Register Automata Learning
Authors: Dierl Simon , Fiterau-Brostean Paul , Howar Falk , Jonsson Bengt , Sagonas Konstantinos , Tåquist Fredrik 
Published: April 2024

AbstractExisting active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present $${SL}^{\lambda }$$

SL

λ

, an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented $${SL}^{\lambda }$$

SL

λ

as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$

SL

∗

, the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.
Small Test Suites for Active Automata Learning
Authors: Kruger Loes , Junges Sebastian , Rot Jurriaan 
Published: April 2024

AbstractA bottleneck in modern active automata learning is to test whether a hypothesized Mealy machine correctly describes the system under learning. The search space for possible counterexamples is given by so-called test suites, consisting of input sequences that have to be checked to decide whether a counterexample exists. This paper shows that significantly smaller test suites suffice under reasonable assumptions on the structure of the black box. These smaller test suites help to refute false hypotheses during active automata learning, even when the assumptions do not hold. We combine multiple test suites using a multi-armed bandit setup that adaptively selects a test suite. An extensive empirical evaluation shows the efficacy of our approach. For small to medium-sized models, the performance gain is limited. However, the approach allows learning models from large, industrial case studies that were beyond the reach of known methods.
Accelerated Bounded Model Checking Using Interpolation Based Summaries
Authors: Solanki Mayank , Chatterjee Prantik , Lal Akash , Roy Subhajit 
Published: April 2024

AbstractWe propose a novel lazy bounded model checking (BMC) algorithm, Trace Inlining, that identifies relevant behaviors of the program to compute partial proofs as procedural summaries. Whenever procedures are reused in other contexts, Trace Inlining attempts to construct safety proofs using these summaries. If the current summaries are sufficient to complete the proof, it gains both in solving times and smaller encodings. If the summaries are found to be insufficient, they are automatically refined for future use. The partial proofs are enabled by a sequence of alternating underapproximation and overapproximation rounds until the program verification condition is found to be unsatisfiable. We evaluate our Trace Inlining algorithm on real-world benchmarks consisting of Windows and Linux device drivers. Our results show that the proposed algorithm is able to solve 12% additional benchmarks that were unsolved by state-of-the-art lazy BMC solvers Corral and Legion. Further, Trace Inlining is 6$$\times $$
×
faster than Corral and 3$$\times $$
×
faster than Legion in terms of verification time. The virtual best of all three verifiers is 4$$\times $$
×
faster than the virtual best of Corral and Legion, implying that our technique significantly improves on what is possible today.
Bubaak-SpLit: Split what you cannot verify (Competition contribution)
Authors: Chalupa Marek , Richter Cedric 
Published: April 2024

AbstractBubaak-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top ofBubaak, a tool designed for running combinations of verifiers in parallel. In contrast toBubaak, that directly invokes verifiers on the inputs,Bubaak-SpLit first starts by splitting the input program into multiple modified versions calledprogram splits. During the splitting process,Bubaak-SpLit utilizes aweakverifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number ofhard-to-verifyprogram splits is generated or a splitting limit is reached. During the main verification phase, we run a combination ofBubaak-LeeandSlowbeastin parallel on the remaining unsolved parts of the verification task.
ESBMC v7.4: Harnessing the Power of Intervals
Authors: Menezes Rafael Sá , Aldughaim Mohannad , Farias Bruno , Li Xianzhiyu , Manino Edoardo , Shmarov Fedor , Song Kunjian , Brauße Franz , Gadelha Mikhail R. , Tihanyi Norbert , Korovin Konstantin , Cordeiro Lucas C. 
Published: April 2024

AbstractESBMC implements many state-of-the-art techniques that combine abstract interpretation and model checking. Here, we report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC now employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, and forward-backward contractors. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.
NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
Authors: Cosler Matthias , Hahn Christopher , Omar Ayham , Schmitt Frederik 
Published: April 2024

AbstractWe introduce , a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis problem. To ensure soundness, the neural engine is coupled with model checkers verifying the predictions of the underlying neural models. The open-source implementation of provides an integration framework for reactive synthesis in which new neural and state-of-the-art symbolic approaches can be seamlessly integrated. Extensive experiments demonstrate its efficacy in handling challenging specifications, enhancing the state-of-the-art reactive synthesis solvers, with contributing novel solves in the current SYNTCOMP benchmarks.
Observational Equality Meets CIC
Authors: Pujet Loïc , Tabareau Nicolas 
Published: April 2024

AbstractEquality is at the heart of dependent type theory, as it plays a fundamental role in specifications and mathematical reasoning. The standard way to handle it in mainstream proof assistants such as Agda, Lean or Coq is based on Martin-Löf’s identity type, which comes straight out of the ’70s—its elegance and simplicity have earned it a long-standing use, despite a major discrepancy with traditional mathematical formulations: it does not satisfy any extensionality principles. Recently, the work on observational equality has regained interest as a new way to encode equality in proof assistants that support a universe of definitionally proof-irrelevant propositions; however it has yet to be integrated in any major proof assistant, because it is not fully compatible with another important feature of type theory: indexed inductive types. In this paper, we propose a systematic integration of indexed inductive types with an observational equality, and show that this integration can only be completely satisfactory if the observational equality satisfies the computational rule of Martin-Löf’s identity type. The second contribution of this paper is a formal proof that this additional computation rule, although not present in previous works on observational equality, can be integrated to the system without compromising the decidability of conversion.
Deciding Subtyping for Asynchronous Multiparty Sessions
Authors: Li Elaine , Stutz Felix , Wies Thomas 
Published: April 2024

AbstractMultiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relation for asynchronous MSTs with communicating state machines (CSMs) as implementation model. We address two problems: when can a local implementation safely substitute another, and when does an arbitrary CSM implement a global type? We define safety with respect to a given global type, in terms of subprotocol fidelity and deadlock freedom. Our implementation model subsumes existing work which considers local types with restricted choice. We exploit the connection between MST subtyping and refinement to formulate concise conditions that are directly checkable on the candidate implementations, and use them to show that both problems are decidable in polynomial time.
Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
Authors: Lundén Daniel , Hummelgren Lars , Kudlicka Jan , Eriksson Oscar , Broman David 
Published: April 2024

AbstractUniversal probabilistic programming languages (PPLs) make it relatively easy to encode and automatically solve statistical inference problems. To solve inference problems, PPL implementations often apply Monte Carlo inference algorithms that rely on execution suspension. State-of-the-art solutions enable execution suspension either through (i) continuation-passing style (CPS) transformations or (ii) efficient, but comparatively complex, low-level solutions that are often not available in high-level languages. CPS transformations introduce overhead due to unnecessary closure allocations—a problem the PPL community has generally overlooked. To reduce overhead, we develop a new efficient selective CPS approach for PPLs. Specifically, we design a novel static suspension analysis technique that determines parts of programs that require suspension, given a particular inference algorithm. The analysis allows selectively CPS transforming the program only where necessary. We formally prove the correctness of the analysis and implement the analysis and transformation in the Miking CorePPL compiler. We evaluate the implementation for a large number of Monte Carlo inference algorithms on real-world models from phylogenetics, epidemiology, and topic modeling. The evaluation results demonstrate significant improvements across all models and inference algorithms.
Higher-Order LCTRSs and Their Termination
Authors: Guo Liye , Kop Cynthia 
Published: April 2024

AbstractLogically constrained term rewriting systems (LCTRSs) are a formalism for program analysis with support for data types that are not (co)inductively defined. Only imperative programs have been considered through the lens of LCTRSs so far since LCTRSs were introduced as a first-order formalism. In this paper, we propose logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order generalization of LCTRSs, which suits the needs of representing and analyzing functional programs. We also study the termination problem of LCSTRSs and define a variant of the higher-order recursive path ordering (HORPO) for the newly proposed formalism.