bluuebunny/crossref_metadata_2025_split huggingface dataset:
Multifunctional Liposomes Remodeling Tumor Immune Microenvironment for Tumor Chemoimmunotherapy
Authors: Li Xinyang , Luo Yang , Huang Zhengjie , Wang Yi , Wu Jian , Zhou Shaobing 
Published: April 2023

AbstractIn the treatment of solid tumors, the complex barriers composed of cancer‐associated fibroblasts (CAFs) prevent drug delivery and T cells infiltration into tumor tissues. Although nanocarriers hold great prospects in drug delivery, fibrosis causes the biological barrier and immunosuppressive tumor microenvironment (ITM) that impairs the anti‐tumor efficacy of nanocarriers. Here, a small dendritic macromolecule loaded with doxorubicin (PAMAM‐ss‐DOX) (DP) is synthesized and encapsulated into pH‐responsive nanoliposome, together with adjuvant toll‐like receptor 7/8 (TLR7/8) agonist resiquimod (R848) and losartan (LOS). The pH‐responsive liposome facilitates the simultaneous and effective delivery of DP, R848, and LOS, which can decompose and release these drugs under the acidic tumor microenvironment. The small sized DP (≈25 nm) with the ability to penetrate into tumor tissue and immunogenic cell death (ICD) can reverse the ITM and elicit immune response, which is equivalent to the effect of an in situ vaccine. Moreover, LOS reduces the activity of CAFs effectively, which can contribute to the infiltration of T cells. Therefore, this nano‐platform provides a new therapeutic strategy for enhanced chemo‐immunotherapy.
Unerwartete Ermüdungsrisse an Hauptträgern einer Eisenbahnbrücke – Dehnungsmessungen unter Betrieb und bruchmechanische Analyse
Authors: Unterweger Harald , Derler Christoph 
Published: April 2023

AbstractAn einer im Jahr 1960 erbauten und in Betrieb genommenen stählernen Eisenbahnbrücke zeigten sich an einigen Quersteifenanschlussdetails zum Hauptträgeruntergurt Ermüdungsrisse im Stegblech. Dies, obwohl das Anschlussdetail den damaligen Empfehlungen der nationalen Norm zum Ermüdungsnachweis entsprechend ausgeführt wurde. Im Beitrag werden die umfangreichen Dehnungsmessungen unter Bahnbetrieb dargestellt, die eine eindeutige Analyse des lokalen Spannungsfelds am kritischen Detailpunkt erlauben, mit einer möglichen Zuordnung zum Phänomen des distortion‐induced fatigue cracking, jedoch mit unerwartet hohen resonanzartigen Biegebeanspruchungen im Stegblech. Mittels bruchmechanischer Analyse und Einbindung der Messwerte für die globalen und lokalen Spannungsfelder aus Bahnbetrieb sowie der bruchmechanischen Kennwerte aus entnommenen Materialproben erfolgte eine Beurteilung der noch verbleibenden Restlebensdauer. Dabei zeigten sich positive Ergebnisse, die auch in Zukunft einen uneingeschränkten Bahnbetrieb erlauben. Es zeigte sich jedoch auch, dass die komplexe Mixed‐Mode‐Beanspruchung am Riss erfasst werden muss und eine alleinige Erfassung des sog. Mode I, der alleinigen Querzugbeanspruchung an der Rissspitze, mitunter unsichere Ergebnisse liefern würde.
Smart cement‐sensor composite: The evolution of nanomaterial in developing sensor for structural integrity
Authors: Kanagasundaram Karthikeyan , Solaiyan Elavenil 
Published: April 2023

AbstractThe integration of self‐sensing ability and different functional properties of nanomaterials into construction materials leads to smart and multifunctional cementitious sensor composites. Significant evolution of the Structural Health Monitoring (SHM) has helped to elevate the life span and mitigate damages of the structure. Developing smart cementitious sensor composite with electrical properties as a parent element and embedding it in the structural components have proved to be advantageous in terms of evaluating the damages, monitoring the periodic health and life assessment of the structures. In this review, the copious development processes and various methods of designing smart‐sensing cementitious composites have been scrutinized. This work recapitulates the principle of self‐sensing technique, typical functional fillers, trends of percolation threshold, dispersing material, dispersion technology, and also describes the required sensing ability of the sensors using the conduction theory. Subsequently application of smart cement‐sensors in structural components for SHM is discussed. In addition, this review article provides comprehensive information on the effects of nano materials and their dispersion in the development for smart and multifaceted cementitious sensor composites with enhanced sensitivity parameters and economic benefits that are suitable for future prospects.
Using drones to detect and quantify wild pig damage and yield loss in corn fields throughout plant growth stages
Authors: Friesenhahn Bethany A. , Massey Lori D. , DeYoung Randy W. , Cherry Michael J. , Fischer Justin W. , Snow Nathan P. , VerCauteren Kurt C. , Perotto‐Baldivieso Humberto L. 
Published: April 2023

AbstractPresently, there are an estimated 6.9 million wild pigs (Sus scrofa) in the U.S., which cause over US$1 billion in damage to agriculture, environmental impacts, and control costs. However, estimates of damage have varied widely, creating a need for standardized monitoring and a method to accurately estimate the economic costs of direct wild pig damage to agriculture. The goal of our study was to integrate remotely sensed imagery from drones and crop harvest data to quantify wild pig damage in corn fields. We used drones with natural color (red, green, blue) cameras to monitor corn fields at different growth stages in an agricultural matrix in Delta County, Texas, USA, during 2019–2020. We flew 36 drone missions and classified wild pig damage in 18 orthomosaics by a combination of manually digitizing and deep‐learning algorithms. We compared estimates of damage from drone imagery to those derived from ground‐based transect surveys, to verify pig damage. Finally, we compared damaged areas of fields to maps of collected real‐time yields at harvest to estimate yield loss. All classified drone orthomosaics of pig damage had >80% overall accuracy for all growth stages. Ground transect surveys, which subsampled 2.6–4.1% of the field, were found to miss damage compared to the complete field coverage provided by drone imagery. Most damage occurred in latter growth stages, when corn ears were maturing, seed was most nutritious, and producers had already invested in the majority of annual crop inputs. Wild pigs damaged up to 9.2% of a single monitored field, which resulted in a mean loss of 3,416 kg of corn/ha and a direct cost to producers of US$17.18–48.24 per ha of damage. Drone imagery, when combined with spatially‐ explicit, harvest yield data, provides an accurate assessment of crop damage and yield loss due to wild pigs in the currency required for the cost‐benefit evaluation of management actions.
Materials in the Drive Chain – Modeling Materials for the Internet of Production
Authors: Rajaei Ali , Becker Marco , Deng Yuanbin , Schenk Oliver , Rooein Soheil , de Oliveira Löhrer Patricia , Reinisch Niklas , Viehmann Tarik , Abouridouane Mustapha , Fernández Mauricio , Broeckmann Christoph , Bergs Thomas , Hirt Gerhard , Lakemeyer Gerhard , Schmitz Georg 
Published: April 2023

AbstractIn this chapter, the focus lies on a predictive description of the material response to the thermomechanical loads within different process steps by means of physical and data-driven models. The modeling approaches are demonstrated in examples of innovative production technologies for components of a drive chain: Fine blanking of parts; powder metallurgical (PM) production of gears; open-die forging and machining of drive shafts. In fine blanking, material, process, and quality data are acquired to model interactions between process and material with data-driven methods. Interpretable machine learning is utilized to non-destructively characterize the initial material state, enabling an optimization of process parameters for a given material state in the long-term. The PM process chain of the gear includes sintering, pressing, surface densification, case hardening, and finishing by grinding. Several modeling and characterization approaches are applied to quantitatively describe the microstructure evolutions in terms of porosity during sintering, density profile after cold rolling, hardness and residual stresses after heat treating and grinding and the tooth root load bearing capacity. In the example of the open-die forging, a knowledge-based approach is developed to support the decision-making process regarding the choice of the proper material and optimized pass schedules. Considering the microstructure of the forged shaft, the elastoplastic material behavior is described by a dislocation-based, multiscale modeling approach. On this basis, process simulations could be carried out to predict the process forces, chip form, residual stresses, and the tool life among other output data.
Verification-guided Programmatic Controller Synthesis
Authors: Wang Yuning , Zhu He 
Published: April 2023

AbstractWe present a verification-based learning framework VEL that synthesizes safe programmatic controllers for environments with continuous state and action spaces. The key idea is the integration of program reasoning techniques into controller training loops. VEL performs abstraction-based program verification to reason about a programmatic controller and its environment as a closed-loop system. Based on a novel verification-guided synthesis loop for training, VEL minimizes the amount of safety violation in the proof space of the system, which approximates the worst-case safety loss, using gradient-descent style optimization. Experimental results demonstrate the substantial benefits of leveraging verification feedback for synthesizing provably correct controllers.
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
Authors: Jaber Nouraldin , Wagner Christopher , Jacobs Swen , Kulkarni Milind , Samanta Roopsha 
Published: April 2023

AbstractDistributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class.In this paper, we present a synthesis-driven tool, Cinnabar, to help system designers building DAB systems ensure that their intended designs belong to an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, Cinnabar generates sketch completions using a counterexample-guided procedure. The core technique relies on compactly encoding root-causes of counterexamples to varied properties such as efficient-decidability and safety. We demonstrate Cinnabar ’s effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems including a distributed key-value store and a distributed consortium system.
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
Authors: Larsen Casper Abild , Schmidt Simon Meldahl , Steensgaard Jesper , Jakobsen Anna Blume , de Pol Jaco van , Pavlogiannis Andreas 
Published: April 2023

AbstractDecomposing a directed graph to its strongly connected components (SCCs) is a fundamental task in model checking. To deal with the state-space explosion problem, graphs are often represented symbolically using binary decision diagrams (BDDs), which have exponential compression capabilities. The theoretically-best symbolic algorithm for SCC decomposition is Gentilini et al’s $$\textsc {Skeleton}$$ algorithm, that uses O(n) symbolic steps on a graph of n nodes. However, $$\textsc {Skeleton}$$ uses $$\Theta (n)$$ symbolic objects, as opposed to (poly-)logarithmically many, which is the norm for symbolic algorithms, thereby relinquishing its symbolic nature. Here we present $$\textsc {Chain}$$, a new symbolic algorithm for SCC decomposition that also makes O(n) symbolic steps, but further uses logarithmic space, and is thus truly symbolic. We then extend $$\textsc {Chain}$$ to $$\textsc {ColoredChain}$$, an algorithm for SCC decomposition on edge-colored graphs, which arise naturally in model-checking a family of systems. Finally, we perform an experimental evaluation of $$\textsc {Chain}$$ among other standard symbolic SCC algorithms in the literature. The results show that $$\textsc {Chain}$$ is competitive on almost all benchmarks, and often faster, while it clearly outperforms all other algorithms on challenging inputs.
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
Authors: Winkler Tobias , Katoen Joost-Pieter 
Published: April 2023

AbstractProbabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem ofcertifyingthat these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with$$> 10^4$$production rules.
Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis
Authors: Apinis Kalmer , Vojdani Vesal 
Published: April 2023

AbstractWe show how to generate a constraint system of symbolic expressions as part of an inter-procedural constraint-system–based program analysis such that any chosen slice of the intended analysis may be computed through the evaluation of the symbolic constraints. Thus, our method ensures that the computed expressions provide genuine explanations for the chosen analysis slice. The resulting system is then annotated with program location information, translated into closed-form expressions, and simplified to yield a human-readable justification for the analyzer’s verdict. Justifications are given using program locations, constants from the program, abstract lattice operations, loops in the analysis, and computed results.
Bubaak: Runtime Monitoring of Program Verifiers
Authors: Chalupa Marek , Henzinger Thomas A. 
Published: April 2023

AbstractThe main idea behind Bubaak is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.At SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why Bubaak only ran several analyses in parallel, without any coordination. Still, Bubaak won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.
Korn—Software Verification with Horn Clauses (Competition Contribution)
Authors: Ernst Gidon 
Published: April 2023

AbstractKorn is a software verifier that infers correctness certificates and violation witnesses sutomatically using state-of-the-art Horn-clause solvers, such as Z3 and Eldarica. The solvers are used in a portfolio together with cheap random sampling where the latter can be very effective at finding counterexamples. Korn perfomend best in the sub-category of SV-COMP 2023.
VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution)
Authors: Darke Priyanka , Chimdyalwar Bharti , Agrawal Sakshi , Kumar Shrawan , Venkatesh R , Chakraborty Supratik 
Published: April 2023

AbstractWe present VeriAbsL, a reachability verifier that performs verification in three stages. First, it slices the input code using a combination of two slicers, then it verifies the slices using predicted strategies, and at last, it composes the result of verifying the individual slices. We introduce a novel shallow slicing technique that uses variable reference information of the program, and data and control dependencies of the entry function to generate slices. We also introduce a novel strategy prediction technique that uses machine learning to predict a strategy. It uses boolean features to describe a program to a neural network that predicts a strategy. We use the portfolio of VeriAbs, a reachabiltiy verifier with manually defined strategies. In sv-comp 2023, VeriAbsL verified 227 (Without witness validation.) more programs than VeriAbs, and 475 (Without witness validation.) programs that VeriAbs could not verify.
VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution)
Authors: Metta Ravindra , Yeduru Prasanth , Karmarkar Hrishikesh , Medicherla Raveendra Kumar 
Published: April 2023

AbstractIn VeriFuzz 1.4, we implemented two new techniques for checking Non-termination and Termination. VeriFuzz 1.4 won the Termination category of SV-COMP 2023.
Specification and Validation of Normative Rules for Autonomous Agents
Authors: Yaman Sinem Getir , Burholt Charlie , Jones Maddie , Calinescu Radu , Cavalcanti Ana 
Published: April 2023

AbstractA growing range of applications use autonomous agents such as AI and robotic systems to perform tasks deemed dangerous, tedious or costly for humans. To truly succeed with these tasks, the autonomous agents must perform them without violating the social, legal, ethical, empathetic, and cultural (SLEEC) norms of their users and operators. We introduce SLEECVAL, a tool for specification and validation of rules that reflect these SLEEC norms. Our tool supports the specification of SLEEC rules in a DSL [1] we co-defined with the help of ethicists, lawyers and stakeholders from health and social care, and uses the CSP refinement checker FDR4 to identify redundant and conflicting rules in a SLEEC specification. We illustrate the use of SLEECVAL for two case studies: an assistive dressing robot, and a firefighting drone.
Yet Another Model! A Study on Model’s Similarities for Defect and Code Smells
Authors: Santos Geanderson , Santana Amanda , Vale Gustavo , Figueiredo Eduardo 
Published: April 2023

AbstractSoftware defect and code smell prediction help developers identify problems in the code and fix them before they degrade the quality or the user experience. The prediction of software defects and code smells is challenging, since it involves many factors inherent to the development process. Many studies propose machine learning models for defects and code smells. However, we have not found studies that explore and compare these machine learning models, nor that focus on the explainability of the models. This analysis allows us to verify which features and quality attributes influence software defects and code smells. Hence, developers can use this information to predict if a class may be faulty or smelly through the evaluation of a few features and quality attributes. In this study, we fill this gap by comparing machine learning models for predicting defects and seven code smells. We trained in a dataset composed of 19,024 classes and 70 software features that range from different quality attributes extracted from 14 Java open-source projects. We then ensemble five machine learning models and employed explainability concepts to explore the redundancies in the models using the top-10 software features and quality attributes that are known to contribute to the defects and code smell predictions. Furthermore, we conclude that although the quality attributes vary among the models, the complexity, documentation, and size are the most relevant. More specifically, Nesting Level Else-If is the only software feature relevant to all models.
Concolic Testing of Front-end JavaScript
Authors: Li Zhe , Xie Fei 
Published: April 2023

AbstractJavaScript has become the most popular programming language for web front-end development. With such popularity, there is a great demand for thorough testing of client-side JavaScript web applications. In this paper, we present a novel approach to concolic testing of front-end JavaScript web applications. This approach leverages widely used JavaScript testing frameworks such as Jest and Puppeteer and conducts concolic execution on JavaScript functions in web applications for unit testing. The seamless integration of concolic testing with these testing frameworks allows injection of symbolic variables within the native execution context of a JavaScript web function and precise capture of concrete execution traces of the function under test. Such concise execution traces greatly improve the effectiveness and efficiency of the subsequent symbolic analysis for test generation. We have implemented our approach on Jest and Puppeteer. The application of our Jest implementation on Metamask, one of the most popular Crypto wallets, has uncovered 3 bugs and 1 test suite improvement, whose bug reports have all been accepted by Metamask developers on Github. We also applied our Puppeteer implementation to 21 Github projects and detected 4 bugs.
Efficient Bounded Exhaustive Input Generation from Program APIs
Authors: Politano Mariano , Bengolea Valeria , Molina Facundo , Aguirre Nazareno , Frias Marcelo F. , Ponzio Pablo 
Published: April 2023

AbstractBounded exhaustive input generation (BEG) is an effective approach to reveal software faults. However, existing BEG approaches require a precise specification of the valid inputs, i.e., a , that must be provided by the user. Writing s for BEG is challenging and time consuming, and they are seldom available in software.In this paper, we introduce , an efficient approach that employs routines from the API of the software under test to perform BEG. Like API-based test generation approaches, creates sequences of calls to methods from the API, and executes them to generate inputs. As opposed to existing BEG approaches, does not require a to be provided by the user. To make BEG from the API feasible, implements three key pruning techniques: (i) discarding test sequences whose execution produces exceptions violating API usage rules, (ii) state matching to discard test sequences that produce inputs already created by previously explored test sequences, and (iii) the automated identification and use of a subset of methods from the API, called builders, that is sufficient to perform BEG.Our experimental assessment shows that ’s efficiency and scalability is competitive with existing BEG approaches, without the need for s. We also show that can assist the user in finding flaws in s, by (automatically) comparing inputs generated by with those generated from a . Using this approach, we revealed several errors in s taken from the assessment of related tools, demonstrating the difficulties of writing precise s for BEG.