bluuebunny/crossref_metadata_2025 huggingface dataset:
Flood Potential Portal: A web tool for understanding flood variability and predicting peak discharges
Authors: Yochum Steven E. , Wible Tyler , Korsa Matthew , Ghanbari Mahshid , Arabi Mazdak
Published: July 2024

The Flood Potential Portal (https://floodpotential.erams.com/) has been developed for the contiguous United States, as a practitioner‐focused tool that uses observational data (streamgages) to enhance understanding of how floods vary in space and time, and assist users in making more informed peak discharge predictions for infrastructure design and floodplain management. This capability is presented through several modules. The Mapping module provides tools to explore variability using multiple indices, and provides detailed information, figures, and algorithms describing and comparing flooding characteristics. The Cross‐Section Analysis module allows users to cut regional‐scale sections to interpret the role of topography in driving flood variability. The Watershed Analysis module provides multiple methods for quantifying expected peak discharge magnitudes and flood frequency relationships at user‐selected locations, including the integration of observed trends in flood magnitudes due to climate change and other sources of nonstationarity into decision making. The Streamgage Analysis module performs streamgage flood‐frequency analyses. These modules are based in part on the flood potential method, through the use of 207 zones of similar flood response defined using more than 8200 streamgages with watershed areas <10,000 km2. Regression models that define each zone had high explained variance (average R2 = 0.93). An example is provided to illustrate use of the Flood Potential Portal for the design of a hypothetical bridge replacement.
More is (sometimes) merrier: Heterogeneity in demand spillovers and competition on a digital platform
Authors: Raj Manav
Published: July 2024

Research Summary

Platforms create value by connecting users to complementors offering goods or services. Complementors compete on platforms but may also benefit each other by drawing demand to the platform, which may then “spillover” from one complementor to another. This tension raises the question: When are relationships between complementors competitive versus complementary? To help address this question, I apply theory on agglomeration‐driven demand spillovers to examine when on‐platform demand spillovers created by peer product launch are larger versus smaller. Studying the Spotify platform, I find spillovers are larger, and peer album release more beneficial to an artist, when the peer stimulates greater demand expansion, platform‐mediated inter‐complementor proximity is higher, and the artist benefits more from consumer learning. Findings extend literature on on‐platform competition and inform complementor strategy.

Managerial Summary

On digital platforms, complementor product launch may hurt peer performance by causing substitution or may benefit peer performance by drawing demand to the platform which may then “spillover” from the complementor to a peer. Studying the Spotify platform, I examine when such spillovers are larger versus smaller, shedding light on when peer product launch is beneficial versus detrimental for complementors competing on digital platforms. On Spotify, demand spillovers are larger, and peer album release more beneficial to an artist, when peer album release draws listeners to the platform, Spotify recommendations connect the artist to the peer, and the artist reaches new or unfamiliar listeners. The findings suggest that, on platforms featuring demand spillovers, complementors can take strategic actions to leverage spillovers and improve performance.
Aramid‐Reinforced UV Curable Adhesive Resins for Use As an Interlayer in Laminated Glass
Authors: Lee Jineun , Lee Hanna , Kwak Giseop
Published: July 2024

Colorless, transparent, and mechanically robust aramid polymers are synthesized from two diamine monomers with strong electron‐withdrawing groups, using low‐temperature solution condensation with diacid chloride. The aramids dissolved very well in the liquid acrylamide monomers. When N,N‐dimethylacrylamide (DMA) is used as a reactive diluent, films with the desired features are produced from the hybrid aramid‐DMA resins via ultraviolet (UV) curing. The hybrid films are colorless and transparent in the visible region and showed an increase in the glass transition temperature, tensile strength, and elastic modulus in proportion to the aramid content. Laminated glass is manufactured using the hybrid resin as an interlayer, which exhibits very strong adhesion between the two sheets of glass, is not easily broken by an external impact, and do not scatter fragments. Moreover, the laminated glass do not distort images and functioned very effectively in UV blocking, soundproofing, and suppressing changes in the ambient temperature. Heat treatment further improves the light transmittance and impact resistance of the laminated glass. Laminated glass specimens with various fluorescence colors are also manufactured. Aramid‐reinforced films prepared using N,N‐diethylacrylamide as a reactive diluent underwent thermally induced phase separation in a wet state, providing smart glass with a privacy protection function.
Valorization of Agriculture Residues into Value‐Added Products: A Comprehensive Review of Recent Studies
Authors: Hoang Tuan‐Dung , Van Anh Nguyen , Yusuf Mohammad , Ali S. A Muhammed , Subramanian Yathavan , Hoang Nam Nguyen , Minh Ky Nguyen , Le Van‐Giang , Thi Thanh Huyen Nguyen , Abi Bianasari Alien , K Azad Abul
Published: July 2024

Global agricultural by‐products usually go to waste, especially in developing countries where agricultural products are usually exported as raw products. Such waste streams, once converted to “value‐added” products could be an additional source of revenue while simultaneously having positive impacts on the socio‐economic well‐being of local people. We highlight the utilization of thermochemical techniques to activate and convert agricultural waste streams such as rice and straw husk, coconut fiber, coffee wastes, and okara power wastes commonly found in the world into porous activated carbons and biofuels. Such activated carbons are suitable for various applications in environmental remediation, climate mitigation, energy storage, and conversions such as batteries and supercapacitors, in improving crop productivity and producing useful biofuels.
Delayed healing is common in in‐situ urethroplasty patients after artificial sphincter cuff erosion
Authors: Matz Ethan L. , Glover Banahene K. , Krug Aaron M. , Langford Brian T. , Franzen Bryce P. , Hudak Steven , VanDyke Maia , Morey Allen F.
Published: July 2024

Introduction

Urethral erosion is a known complication of artificial urinary sphincter (AUS) surgery. We performed an in‐situ urethroplasty (ISU) to reduce the healing time and time to reimplantation of the AUS. We sought to assess urethral integrity one month after ISU and to identify factors associated with delayed healing in our high‐volume tertiary referral center experience.

Methods

A retrospective review of our AUS database from 2009 to 2023 was conducted to identify all ISU cases. Patients were stratified as healed or non‐healed based on the absence of extravasation on voiding cystourethrogram (VCUG) obtained 4 weeks postoperatively. Background characteristics were evaluated including age, body mass index, diabetes, hypogonadism and smoking history. Operative variables included degree of erosion, location of defect, and the number of stitches required for repair.

Results

Among 98 patients undergoing an ISU, 61 underwent VCUG at one month. Of these, 34.4% (21/61) had evidence of delayed healing on VCUG requiring prolonged catheterization. Although a higher average number of repair sutures were used in ISU, this was not significant (p = 0.381). The most common complication in both groups was urinary tract infection (UTI). Non‐healed patients had a higher rate of UTI, without significant predilection towards fistula, stricture or diverticulum. No other patient or operative characteristic was significantly different between groups.

Conclusion

Despite an aggressive approach to management via ISU, many patients still require prolonged catheterization after AUS erosion to ensure complete healing of the defect.
The role of the forensic archeologist and anthropologist in recovery of human remains from fatal fires
Authors: Swales Diana , Hackman Lucina
Published: July 2024

Fatal fires pose complex challenges for responders due to the requirement to investigate all aspects of the fire using methods that maximize evidence recovery and integrity, including optimal and respectful recovery of the deceased. In this article, the authors consider the value of the inclusion of both forensic archeologists and forensic anthropologists in circumstances of fatal fire, identifying some of the challenges posed by these environments and what each can contribute.

This article is categorized under:

Crime Scene Investigation > Crime Scene Examination

Forensic Anthropology > Forensic Archaeology

Forensic Anthropology > Taphonomic Changes and the Environment
Enduring inequalities: Revascularization before and after the ACA
Authors: Gusmano Michael K. , Weisz Daniel , Palghat Swati , Rodwin Victor G.
Published: July 2024

The use of revascularization (coronary artery bypass surgery [CABG] and percutaneous coronary intervention [PCI]) in the United States is declining, but they remain important procedures for the treatment of patients with coronary artery disease. There are large and long‐standing disparities in the use of revascularization among patients hospitalized with heart disease. In this article, we investigate whether the implementation of the Patient Protection and Affordable Care Act (ACA) is associated with a reduction in disparities in the use of revascularization. We use data from the Agency for Healthcare Research and Quality (AHRQ)'s National Inpatient Sample (NIP) of the Healthcare Cost and Utilization Project (HCUP) project to compare the use of revascularization among patients 45 years and older in the United States in 2012 and 2018. For both years, we conducted multiple logistic regression analysis to assess the factors associated with coronary revascularization among patients hospitalized with heart disease. Hospitalizations for heart disease and the use of revascularization both fell between 2012 and 2018 at a rate that was greater than the reduction in heart disease deaths in the country. These findings are consistent with the clinical literature on the growth of medical management of heart disease. Disparities in the use of revascularization, by gender, insurance status, neighborhood, and race/ethnicity, were just as large after the implementation of the ACA in 2014. The expansion of insurance by the ACA, alone, was insufficient to reduce disparities in the use of revascularization in patients with diagnosed coronary heart disease in the United States.
Structures of Large Tin(IV) Oxo Clusters
Authors: Schubert Ulrich
Published: July 2024

The article reviews and categorizes the structures of tin oxo clusters with nuclearities ≥6 and compares them with oxo clusters of the other group 4 and 14 metals. Basic construction principles of the cluster core are worked out by comparing the different cluster types and by identifying smaller building blocks. The comparison also shows how the different cluster types are influenced by the interplay between the ligands which stabilize the cluster core and the bridging oxygen atoms.
Nation Branding, Digital Advocacy and Feminist Foreign Policy
Authors: Aggestam Karin , Rosamond Annika Bergman , Hedling Elsa
Published: July 2024

This chapter examines how Sweden’s feminist foreign policy was constructed and managed as a nation brand during its eight years of existence. This particular nation brand built on and was informed by Sweden’s longstanding state feminist tradition as well as its more recent digital sophistication. As the chapter shows, Sweden’s feminist foreign policy was an exercise in feminist branding, paired with a strong awareness that digital communication of feminist values required both pragmatism and policy adaptation. We analyse how strategies of hashtag feminism triggered resonance among global audiences not least in digital advocacy networks, drawing attention to and mobilising support for the distinct values and ambitions of Sweden’s feminist foreign policy. Finally, we examine how Sweden’s feminist foreign policy was contested by actors globally. To illustrate this process of contestation, we pay particular attention to a Swedish state visit to Iran in 2017, which triggered a range of strong online reactions.
Railway Demand Evaluation: HSR Induced Component
Authors: Russo Francesco , Moschella Marialuisa , Musolino Giuseppe
Published: July 2024

The introduction of High-Speed Rail (HSR) systems in different countries of the world has demonstrated to be a decisive solution for the sustainable development of the mobility and economic growth, and for the promotion of social inclusion. This paper aims to identify the main methodological approaches to evaluate travel demand induced by the presence of HSR services through a systematic review of the relevant scientific literature. The objective is the exploration of the proposed models and methodological gaps present in the existing research. The findings of this study provide a solid basis for future development in the study of induced demand generated by HSR services, suggesting necessary directions for the advancement of demand analysis methodologies, thus contributing to a more comprehensive analysis of the effects of high-speed rail systems.
Dynamic Structure of Fares for High Speed Rail Services
Authors: Russo Francesco , Sgro Domenico , Musolino Giuseppe
Published: July 2024

The entering of High Speed Rail (HSR) passenger services caused competition in the market with other conventional rail services, and other transport modes. The dynamic structure of fares in the HSR services assume a crucial role in the supply of scheduled transport services and influence travelers’ choice behavior. The HSR fare structures, similarly to the air services, is characterized by evolutions and changes over time due to several factors, such as travelers’ behavior; strategies of the companies supplying the HSR services. The results reported in the paper contain a framework for analysis of the evolution of fares over time in relation to the day of ticket purchase and of the day of trip. A sample representation of a pilot case study implemented on the existing HSR line between Rome and Milan (Italy), where two HSR companies operate and compete each other, is presented.

The aim of the study is to identify the characteristics fares evolution over time in the HSR market. This work is useful for support transport planners and decision-makers for the ex-ante evaluation of fare structure in terms of users’ behavior.
State of the Art of Sustainable Development of Railway Nodes: The High Speed Rail (HSR)
Authors: Panuccio Paola
Published: July 2024

High Speed Rail (HSR) is a new mode of transport and has a significant impact on the territory. The urban plan, in respect of the technical standards set by the rules, does not provide any indication for the inclusion of an important node in the territory, such as a station of an HSR line. Even the Sustainable Urban Mobility Plans (SUMPs) designed for metropolitan areas, in their strategic choices, often do not give indications on the HSR. It therefore happens that the territories are distorted by the effects caused by the location of such an important infrastructural node. Furthermore, the stations of the HSR are designed by “archi-star” architects who give a significant formal and visual mark on the territory. The paper underlines the importance of HSR through the analysis of two case studies, the effects that HSR cause on the territory. The first case of the Mediopadana High Speed Rail station in Reggio Emilia analyses the impact caused on a moderately anthropized territory. The second case of the High Speed Rail station of Naples Afragola analyses the impact caused on a highly anthropized territory. The analysis of these two projects concludes with considerations regarding the opportunity of an integrated urban and transport planning.
The MoXI Model Exchange Tool Suite
Authors: Johannsen Chris , Nukala Karthik , Dureja Rohit , Irfan Ahmed , Shankar Natarajan , Tinelli Cesare , Vardi Moshe Y. , Rozier Kristin Yvonne
Published: July 2024

We release the first tool suite implementingMoXI(Model eXchange Interlingua), an intermediate language for symbolic model checking designed to be an international research-community standard and developed by a widespread collaboration under a National Science Foundation (NSF) CISE Community Research Infrastructure initiative. Although we focus here on hardware verification, theMoXIlanguage is useful for software model checking and verification of infinite-state systems in general.MoXIbuilds on elements of SMT-LIB 2; it is easy to add new theories and operators. Our contributions include: (1) introducing the first tool suite of automated translators into and out of the new model-checking intermediate language; (2) composing an initial example benchmark set enabling the model-checking research community to build future translations; (3) compiling details for utilizing, extending, and improving upon our tool suite, including usage characteristics and initial performance data. Experimental evaluations demonstrate that compiling SMV-language models throughMoXIto perform symbolic model checking with the tools from the last Hardware Model Checking Competition performs competitively with model checking directly vianuXmv.
End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT
Authors: Yuan Shenghao , Besson Frédéric , Talpin Jean-Pierre
Published: July 2024

Modern operating systems have adopted Berkeley Packet Filters (BPF) as a mechanism to extend kernel functionalities dynamically, e.g., Linux’s eBPF or RIOT’s rBPF. The just-in-time (JIT) compilation of eBPF introduced in Linux eBPF for performance has however led to numerous critical issues. Instead, RIOT’s rBPF uses a slower but memory-isolating interpreter (a virtual machine) which implements a defensive semantics of BPF; and therefore trades performance for security. To increase performance without sacrificing security, this paper presents a fully verified JIT implementation for RIOT’s rBPF, consisting of: i/ an end-to-end refinement workflow to both proving the JIT correct from an abstract specification and by deriving a verified concrete C implementation; ii/ a symbolic CompCert interpreter for executing binary code; iii/ a verified JIT compiler for rBPF; iv/ a verified hybrid rBPF virtual machine. Our core contribution is, to the best of our knowledge, the first and fully verified rBPF JIT compiler with correctness guarantees from high-level specification to low-level implementation. Benchmarks on microcontrollers hosting the RIOT operating system demonstrate significant performance improvements over the existing implementations of rBPF, even in worst-case application scenarios.
A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Authors: Cho Chanhee , Zhou Yi , Bosamiya Jay , Parno Bryan
Published: July 2024

Many program verification tools provide automation via SMT solvers, allowing them to automatically discharge many proofs. However, when a proof fails, it can be hard to understand why it failed or how to fix it. The main feedback the developer receives is simply the verification result (i.e., success or failure), with no visibility into the solver’s internal state. To assist developers using such tools, we introduce ProofPlumber, a novel and extensible proof-action framework for understanding and debugging proof failures. Proof actions act on the developer’s source-level proofs (e.g., assertions and lemmas) to determine why they failed and potentially suggest remedies. We evaluate ProofPlumber by writing a collection of proof actions that capture common proof debugging practices. We produce 17 proof actions, each only 29–177 lines of code.
SMT-Based Symbolic Model-Checking for Operator Precedence Languages
Authors: Chiari Michele , Geatti Luca , Gigante Nicola , Pradella Matteo
Published: July 2024

Operator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in thePrecedence Oriented Temporal Logic(), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, SMT-based approach for model checking properties. While previous approaches construct the automaton for both the formula and the model of the program, we encode them into a (sequence of) SMT formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an SMT-solver, in a Bounded Model Checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.
On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Authors: Wang Chenglin , Lin Fangzhen
Published: July 2024

Loops are inductive constructs, which make them difficult to analyze and verify in general. One approach is to represent the inductive behaviors of the program variables in a loop by recurrences and try to solve them for closed-form solutions. These solutions can then be used to generate invariants or directly fed into an SMT-based verifier. One problem with this approach is that if a loop contains nondeterministic choices or complex operations such as non-linear assignments, then recurrences for program variables may not exist or may have no closed-form solutions. In such cases, an alternative is to generate recurrences for expressions, and there has been recent work along this line. In this paper, we further work in this direction and propose a template-based method for extracting polynomial expressions that satisfy some c-finite recurrences. While in general there are possibly infinitely many such polynomials for a given loop, we show that the desired polynomials form a finite union of vector spaces. We propose an algorithm for computing the bases of the vector spaces, and identify two cases where the bases can be computed efficiently. To demonstrate the usefulness of our results, we implemented a prototype system based on one of the special cases, and integrated it into an SMT-based verifier. Our experimental results show that the new verifier can now verify programs with non-linear properties.
Hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Authors: Dxo  , Soos Mate , Paraskevopoulou Zoe , Lundfall Martin , Brockman Mikael
Published: July 2024

We present , a symbolic execution engine for the EVM. can prove safety properties for EVM bytecode or verify semantic equivalence between two bytecode objects. It exposes a user-friendly API in Solidity that allows end-users to define symbolic tests using almost the same syntax as they would for their usual unit tests. We evaluate our framework against state-of-the-art tools, using a comprehensive set of benchmarks. Our empirical findings demonstrate that outperforms its counterparts, effectively solving a greater number of problems within competitive time frames.
SolTG: A CHC-Based Solidity Test Case Generator
Authors: Britikov Konstantin , Zlatkin Ilia , Fedyukovich Grigory , Alt Leonardo , Sharygina Natasha
Published: July 2024

Achieving high test coverage is important when developing blockchain smart contracts, but it could be challenging without automated reasoning tools. In this paper, we present SolTG, an automated test case generator for Solidity based on constrained Horn clauses (CHC). SolTG exhaustively enumerates symbolic path constraints from the contract’s CHC representation and makes calls to the Satisfiability Modulo Theories (SMT) solver to find input values under which the contract exhibits the corresponding behavior. Test cases synthesized by SolTG have the form of a sequence of function calls over concrete values of input parameters which lead to a specific execution scenario. The tool supports multiple Solidity-specific features and is capable of exhibiting a high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG based on the existing translation of smart contracts into a CHC representation. We also present the experimental results for test generation on the regression and industrial benchmarks.
Distributed SMT Solving Based on Dynamic Variable-Level Partitioning
Authors: Zhao Mengyu , Cai Shaowei , Qian Yuhang
Published: July 2024

Satisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT solvers. With the development of computing resources, a promising direction to boost performance is parallel and even distributed SMT solving. We explore this potential in a divide-and-conquer view and propose a novel dynamic parallel framework with variable-level partitioning. To the best of our knowledge, this is the first attempt to perform variable-level partitioning for arithmetic theories. Moreover, we enhance the interval constraint propagation algorithm, coordinate it with Boolean propagation, and integrate it into our variable-level partitioning strategy. Our partitioning algorithm effectively capitalizes on propagation information, enabling efficient formula simplification and search space pruning. We apply our method to three state-of-the-art SMT solvers, namely CVC5, OpenSMT2, and Z3, resulting in efficient parallel SMT solvers. Experiments are carried out on benchmarks of linear and non-linear arithmetic over both real and integer variables, and our variable-level partitioning method shows substantial improvements over previous partitioning strategies and is particularly good at non-linear theories.
Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement
Authors: Murphy Charlie , Kincaid Zachary
Published: July 2024

Checking satisfiability of formulae in the theory of linear arithmetic has far reaching applications, including program verification and synthesis. Many satisfiability solvers excel at proving and disproving satisfiability of quantifier-free linear arithmetic formulas and have recently begun to support quantified formulas. Beyond simply checking satisfiability of formulas, fine-grained strategies for satisfiability games enables solving additional program verification and synthesis tasks. Quantified satisfiability games are played between two players—SAT and UNSAT—who take turns instantiating quantifiers and choosing branches of boolean connectives to evaluate the given formula. A winning strategy for SAT (resp. UNSAT) determines the choices of SAT (resp. UNSAT) as a function of UNSAT ’s (resp. SAT ’s) choices such that the given formula evaluates to true (resp. false) no matter what choices UNSAT (resp. SAT) may make. As we are interested in both checking satisfiability and synthesizing winning strategies, we must avoid conversion to normal-forms that alter the game semantics of the formula (e.g. prenex normal form). We present fine-grained strategy improvement and strategy synthesis, the first technique capable of synthesizing winning fine-grained strategies for linear arithmetic satisfiability games, which may be used in higher-level applications. We experimentally evaluate our technique and find it performs favorably compared with state-of-the-art solvers.
Formally Certified Approximate Model Counting
Authors: Tan Yong Kiam , Yang Jiong , Soos Mate , Myreen Magnus O. , Meel Kuldeep S.
Published: July 2024

Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), $$\textsf{ApproxMC}$$
ApproxMC
, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of $$\textsf{ApproxMC}$$
ApproxMC
’s approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter’s stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints.

We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm’s PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of $$\textsf{ApproxMC}$$
ApproxMC
’s calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both $$\textsf{ApproxMC}$$
ApproxMC
and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify $$84.7\%$$

84.7
%

of instances with generated certificates when given the same time and memory limits as the counter.
LTL Learning on GPUs
Authors: Valizadeh Mojtaba , Fijalkow Nathanaël , Berger Martin
Published: July 2024

Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, a branch-free implementation of LTL that has $$O(\log n)$$

O
(
log
n
)

time complexity, where n is trace length, while previous implementations are $$O(n^2)$$

O
(

n
2

)

or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs—a realistic assumption on modern processors).
Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
Authors: Sato Sota , An Jie , Zhang Zhenya , Hasuo Ichiro
Published: July 2024

Techniques of light-weight formal methods, such as monitoring and falsification, are attracting attention for quality assurance of cyber-physical systems. The techniques require formal specs, however, and writing right specs is still a practical challenge. Commonly one relies ontrace synthesis—i.e. automatic generation of a signal that satisfies a given spec—to examine the meaning of a spec. In this work, motivated by 1) complex STL specs from an automotive safety standard and 2) the struggle of existing tools in their trace synthesis, we introduce a novel trace synthesis algorithm for STL specs. It combines the use of MILP (inspired by works on controller synthesis) and avariable-interval encodingof STL semantics (previously studied for SMT-based STL model checking). The algorithm solves model checking, too, as the dual of trace synthesis. Our experiments show that only ours has realistic performance needed for the interactive examination of STL specs by trace synthesis.
Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis
Authors: Ren Dejin , Liang Zhen , Wu Chenyu , Ding Jianqiang , Wu Taoran , Xue Bai
Published: July 2024

Inner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable estimation of the set of states that a system can reach from given initial states at a specific time instant. In this paper, we study the inner-approximate reachability analysis problem based on the set-boundary reachability method for systems modelled by ordinary differential equations, in which the computed inner-approximations are represented with zonotopes. The set-boundary reachability method computes an inner-approximation by excluding states reached from the initial set’s boundary. The effectiveness of this method is highly dependent on the efficient extraction of the exact boundary of the initial set. To address this, we propose methods leveraging boundary and tiling matrices that can efficiently extract and refine the exact boundary of the initial set represented by zonotopes. Additionally, we enhance the exclusion strategy by contracting the outer-approximations in a flexible way, which allows for the computation of less conservative inner-approximations. To evaluate the proposed method, we compare it with state-of-the-art methods against a series of benchmarks. The numerical results demonstrate that our method is not only efficient but also accurate in computing inner-approximations.
Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Authors: Wang Jiawan , Liu Wenxia , Zhang Muzimiao , Wei Jiaqi , Shi Yuhui , Bu Lei , Li Xuandong
Published: July 2024

Cyber-physical systems (CPSs) are used in many safety-critical areas, making it crucial to ensure their safety. However, with CPSs increasingly dynamically deployed and reconfigured during runtime, their safety analysis becomes challenging. For one thing, reconfigurable CPSs usually consist of multiple agents dynamically connected during runtime. Their highly dynamic system topologies are too intricate for traditional modeling languages, which, in turn, hinders formal analysis. For another, due to the growing size and uncertainty of reconfigurable CPSs, their system models can be huge and even unavailable at design time. This calls for runtime analysis approaches with better scalability and efficiency. To address these challenges, we propose a scenario-based hierarchical modeling language for reconfigurable CPS. It provides template models for agent inherent features, together with an instantiation mechanism to activate single agent’s runtime behavior, communication configurations for multiple agents’ connected behaviors, and scenario task configurations for their dynamic topologies. We also present a path-oriented falsification approach to falsify system requirements. It employs classification-model-based optimization to explore search space effectively and cut unnecessary system simulations and robustness calculations for efficiency. Our modeling and falsification are implemented in a tool called . Experiments have shown that it can largely reduce modeling time and improve modeling accuracy, and perform scalable CPS falsification with high success rates in seconds.
Probabilistic Access Policies with Automated Reasoning Support
Authors: Zhu Shaowei , Zhang Yunbo
Published: July 2024

Existing access policy languages like Cedar equipped with SMT-based automated reasoning capabilities are effective in providing formal guarantees about the policies. However, this scheme only supports access control based on deterministic information. Observing that certain information useful for access control can be described by random variables, we are motivated to develop a new paradigm of access control in which access policies contain rules about uncertainty, or more precisely, probabilities of random events. To compute these probabilities, we rely on probabilistic programming languages. Additionally, we show that the probabilistic part of these policies can be encoded in linear real arithmetic, which enables practical automated reasoning tasks such as proving relative permissiveness between policies. We demonstrate the advantages of the proposed probabilistic policies over the existing paradigm through two case studies on real-world datasets with a prototype implementation.
Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Authors: Lin Yi , Martinelli Tabajara Lucas , Vardi Moshe Y.
Published: July 2024

Inspired by recent progress in dynamic programming approaches for weighted model counting, we investigate a dynamic-programming approach in the context of boolean realizability and synthesis, which takes a conjunctive-normal-form boolean formula over input and output variables, and aims at synthesizing witness functions for the output variables in terms of the inputs. We show how graded project-join trees, obtained via tree decomposition, can be used to compute a BDD representing the realizability set for the input formulas in a bottom-up order. We then show how the intermediate BDDs generated during realizability checking phase can be applied to synthesizing the witness functions in a top-down manner. An experimental evaluation of a solver – DPSynth – based on these ideas demonstrates that our approach for Boolean realizabilty and synthesis has superior time and space performance over a heuristics-based approach using same symbolic representations. We discuss the advantage on scalability of the new approach, and also investigate our findings on the performance of the DP framework.
Bisimulation Learning
Authors: Abate Alessandro , Giacobbe Mirco , Schnitzer Yannik
Published: July 2024

We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.
Resummation of combined QCD-electroweak effects in Drell Yan lepton-pair production
Authors: Buonocore Luca , Rottoli Luca , Torrielli Paolo
Published: July 2024

Abstract

We consider neutral- and charged-current Drell Yan lepton-pair production at hadron colliders, and include dominant classes of electroweak and mixed QCD-electroweak corrections to all orders in perturbation theory. The accurate description of these physical effects is vital for a precise determination of fundamental Standard Model parameters, such as the W-boson mass and the electroweak mixing angle, as well as for a solid assessment of the associated theoretical uncertainties. Our state-of-the-art resummation reaches next-to-leading-logarithmic accuracy in both the electroweak and the mixed QCD-electroweak perturbative expansions, including constant terms at first order beyond Born level in both couplings, i.e. at order α and αsα. These effects are incorporated on top of QCD predictions at next-to-next-to-next-to-leading-logarithmic accuracy, which include constant terms at third order in the strong coupling. Our results retain, for the first time at this accuracy, full dependence on the kinematics of the final-state leptons, thereby enabling a realistic comparison with experimental analyses at the differential level in presence of fiducial cuts. We present a phenomenological analysis of the impact of electroweak corrections in relevant observables at the LHC. We find visible shape distortions in resummation-dominated kinematical regions with respect to pure-QCD predictions, highlighting the importance of a complete description, not limited to QCD, for precision Drell Yan physics.
A path integral formula of quantum gravity emergent from entangled local structures
Authors: Liu Jinglong , Alexander Stephon , Marcianò Antonino , Pasechnik Roman
Published: July 2024

Abstract

We couple to group field theory (GFT) a scalar field that encodes the entanglement between manifold sites. The scalar field provides a relational clock that enables the derivation of the Hamiltonian of the system from the GFT action. Inspecting the Hamiltonian, we show that a theory of emergent gravity arises, and that this can be recast according to the Ashtekar’s formulation of general relativity. The evolution of the GFT observables is regulated by the Shrödinger equation generated by the Hamiltonian. This is achieved by imposing a renormalization group (RG) flow that corresponds to a simplified Ricci flow. As a consequence of the quantization procedure, the Hamiltonian is recovered to be non-Hermitian, and can be related to the complex action formalism, in which the initial conditions and the related future evolution of the systems are dictated by the imaginary part of the action.
Seasonal patterns of hip fracture incidence and mortality rates across age groups of older adults in Israel
Authors: Yonai Yaniv , Masarwa Salim , Ben Natan Merav , Berkovich Yaron
Published: July 2024

Purpose

This study investigates the seasonal patterns of hip fracture occurrence and mortality rates in the elderly population of Israel.

Methods

In this retrospective study, we examined a random sample of 400 patients who underwent a hip fracture repair surgery at a 495-bed hospital in northern-central Israel during the years 2021–2022.

Results

Our findings reveal a heightened incidence of hip fractures during the spring (30.8%) in contrast to relatively consistent rates during other seasons (22-24.2%). Patients experiencing hip fractures in the spring were notably younger and had shorter hospital stays compared to those in other seasons. Furthermore, we identified seasonal variations in hip fracture incidence concerning gender, culture, and nationality. Over the 2-year follow-up period, 20% of patients had succumbed to mortality. The highest survival rate was associated with hip fractures sustained in the spring, while the lowest rates were observed in the autumn and winter.

Conclusion

While our study highlights significant seasonal variations in hip fracture occurrence and mortality rates among the elderly population in Israel, caution is warranted in interpreting the implications for post-fracture care and resource allocation. The observed heightened incidence of hip fractures during the spring, particularly among younger patients with shorter hospital stays, suggests the need for further investigation into potential risk factors and preventive measures specific to this season. Additionally, our identification of seasonal variations in hip fracture incidence across demographic factors underscores the importance of tailored interventions to address the diverse needs of different populations.
Structure-based humanization of a therapeutic antibody for multiple myeloma
Authors: Marino Stephen F. , Daumke Oliver
Published: July 2024

The optimal efficacy of xenogeneically generated proteins intended for application in humans requires that their own antigenicity be minimized. This necessary adaptation of antibodies to a humanized version poses challenges since modifications even distant from the binding sites can greatly influence antigen recognition and this is the primary feature that must be maintained during all modifications. Current strategies often rely on grafting and/or randomization/selection to arrive at a humanized variant retaining the binding properties of the original molecule. However, in terms of speed and efficiency, rationally directed approaches can be superior, provided the requisite structural information is available. We present here a humanization procedure based on the high-resolution X-ray structure of a chimaeric IgG against a marker for multiple myeloma. Based on in silico modelling of humanizing amino acid substitutions identified from sequence alignments, we devised a straightforward cloning procedure to rapidly evaluate the proposed sequence changes. Careful inspection of the structure allowed the identification of a potentially problematic amino acid change that indeed disrupted antigen binding. Subsequent optimization of the antigen binding loop sequences resulted in substantial recovery of binding affinity lost in the completely humanized antibody. X-ray structures of the humanized and optimized variants demonstrate that the antigen binding mode is preserved, with surprisingly few direct contacts to antibody atoms. These results underline the importance of structural information for the efficient optimization of protein therapeutics.

Key messages

Structure-based humanization of an IgG against BCMA, a marker for Multiple Myeloma.

Identification of problematic mutations and unexpected modification sites.

Structures of the modified IgG-antigen complexes verified predictions.

Provision of humanized high-affinity IgGs against BCMA for therapeutic applications.
Breeding and management of major resistance genes to stem canker/blackleg in Brassica crops
Authors: Vasquez-Teuber Paula , Rouxel Thierry , Mason Annaliese S. , Soyer Jessica L.
Published: July 2024

Blackleg (also known as Phoma or stem canker) is a major, worldwide disease of Brassica crop species, notably B. napus (rapeseed, canola), caused by the ascomycete fungus Leptosphaeria maculans. The outbreak and severity of this disease depend on environmental conditions and management practices, as well as a complex interaction between the pathogen and its hosts. Genetic resistance is a major method to control the disease (and the only control method in some parts of the world, such as continental Europe), but efficient use of genetic resistance is faced with many difficulties: (i) the scarcity of germplasm/genetic resources available, (ii) the different history of use of resistance genes in different parts of the world and the different populations of the fungus the resistance genes are exposed to, (iii) the complexity of the interactions between the plant and the pathogen that expand beyond typical gene-for-gene interactions, (iv) the incredible evolutionary potential of the pathogen and the importance of knowing the molecular processes set up by the fungus to “breakdown’ resistances, so that we may design high-throughput diagnostic tools for population surveys, and (v) the different strategies and options to build up the best resistances and to manage them so that they are durable. In this paper, we aim to provide a comprehensive overview of these different points, stressing the differences between the different continents and the current prospects to generate new and durable resistances to blackleg disease.