Search

Static analysis is an essential component of many modern software development tools. Unfortunately, the ever-increasing complexity of static analyzers makes their coding error-prone. Even analysis tools based on rigorous mathematical techniques, such as abstract interpretation, are not immune to bugs. Ensuring the correctness and reliability of software analyzers is critical if they are to be inserted in production compilers and development environments. While compiler validation has seen notable success, formal validation of static analysis tools remains relatively unexplored. In this paper, we propose a method for testing abstract interpretation-based static analyzers. Broadly, it consists in checking, over a suite of benchmarks, that the properties inferred statically are satisfied dynamically. The main advantage of our approach lies in its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework, and its blended static/dynamic assertion checking approach. We demonstrate that in this setting, the analysis can be tested with little effort by combining the following components already present in the framework: 1) the static analyzer, which outputs its results as the original program source with assertions interspersed; 2) the assertion run-time checking mechanism, which instruments a program to ensure that no assertion is violated at run time; 3) the random test case generator, which generates random test cases satisfying the properties present in assertion preconditions; and 4) the unit-test framework, which executes those test cases. We have applied our approach to the CiaoPP static analyzer, resulting in the identification of many bugs with reasonable overhead. Most of these bugs have been either fixed or confirmed, helping us detect a range of errors not only related to analysis soundness but also within other aspects of the framework., Comment: Under consideration in Theory and Practice of Logic Programming (TPLP). Extended, revised version of our work published in LOPSTR (Casso et al. 2021)

The RESISTO project represents a pioneering initiative in Europe aimed at enhancing the resilience of the power grid through the integration of advanced technologies. This includes artificial intelligence and thermal surveillance systems to mitigate the impact of extreme meteorological phenomena. RESISTO endeavors to predict, prevent, detect, and recover from weather-related incidents, ultimately enhancing the quality of service provided and ensuring grid stability and efficiency in the face of evolving climate challenges. In this study, we introduce one of the fundamental pillars of the project: a monitoring system for the operating temperature of different regions within power transformers, aiming to detect and alert early on potential thermal anomalies. To achieve this, a distributed system of thermal cameras for real-time temperature monitoring has been deployed in The Do\~nana National Park, alongside servers responsible for the storing, analyzing, and alerting of any potential thermal anomalies. An adaptive prediction model was developed for temperature forecasting, which learns online from the newly available data. In order to test the long-term performance of the proposed solution, we generated a synthetic temperature database for the whole of the year 2022. Overall, the proposed system exhibits promising capabilities in predicting and detecting thermal anomalies in power electric transformers, showcasing potential applications in enhancing grid reliability and preventing equipment failures.

The RESISTO project, a pioneer innovation initiative in Europe, endeavors to enhance the resilience of electrical networks against extreme weather events and associated risks. Emphasizing intelligence and flexibility within distribution networks, RESISTO aims to address climatic and physical incidents comprehensively, fostering resilience across planning, response, recovery, and adaptation phases. Leveraging advanced technologies including AI, IoT sensors, and aerial robots, RESISTO integrates prediction, detection, and mitigation strategies to optimize network operation. This article summarizes the main technical aspects of the proposed solutions to meet the aforementioned objectives, including the development of a climate risk detection platform, an IoT-based monitoring and anomaly detection network, and a fleet of intelligent aerial robots. Each contributing to the project's overarching objectives of enhancing network resilience and operational efficiency.

We prove Sobolev-Poincar\'e and Poincar\'e inequalities in variable Lebesgue spaces $L^{p(\cdot)}(\Omega)$, with $\Omega\subset{\mathbb R}^n$ a bounded John domain, with weaker regularity assumptions on the exponent $p(\cdot)$ that have been used previously. In particular, we require $p(\cdot)$ to satisfy a new \emph{boundary $\log$-H\"older condition} that imposes some logarithmic decay on the oscillation of $p(\cdot)$ towards the boundary of the domain. Some control over the interior oscillation of $p(\cdot)$ is also needed, but it is given by a very general condition that allows $p(\cdot)$ to be discontinuous at every point of $\Omega$. Our results follows from a local-to-global argument based on the continuity of certain Hardy type operators. We provide examples that show that our boundary $\log$-H\"older condition is essentially necessary for our main results. The same examples are adapted to show that this condition is not sufficient for other related inequalities. Finally, we give an application to a Neumann problem for a degenerate $p(\cdot)$-Laplacian.

Let $\A$ be a $\k$-algebra where $\k$ a field of arbitrary characteristic, and let $\mathscr{A}_\k$ be a full subcategory of $\A$-Mod, the abelian category of left $\A$-modules.Following M. Kleiner and I. Reiten, $\mathscr{A}_\k$ is {\it Hom-finite} if the hom-space between any two objects in $\mathscr{A}_\k$ is finite-dimensional over $\k$. We further say that $\mathscr{A}_\k$ is {\it Ext-finite} if $\dim_\k\Ext^i_\A(X,Y)<\infty$ for all objects $X$ and $Y$ in $\mathscr{A}_\k$. Let $V$ be an object in $\mathscr{A}_\k$. In this note we prove that if $\End_\A(V)$ is isomorphic to $\k$, then $V$ has a universal deformation ring $R(\A,V)$, which is a local complete Noetherian commutative $\k$-algebra whose residue field is also isomorphic to $\k$. We use this result to prove that if $\A$ is a local two-point infinite dimensional gentle $\k$-algebra (in the sense of V. Bekkert et al), then $R(\A,V)$ is isomorphic either to $\k$, to $\k[\![t]\!]/(t^2)$ or to $\k[\![t]\!]$.

Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many useful program properties. Such properties include modes, determinacy, non-failure, cost, etc. This has motivated significant work on developing abstract domains to improve the precision and performance of sharing analyses. Much of this work has centered around the family of set-sharing domains, because of the high precision they offer. However, this comes at a price: their scalability to a wide set of realistic programs remains challenging and this hinders their wider adoption. In this work, rather than defining new sharing abstract domains, we focus instead on developing techniques which can be incorporated in the analyzers to address aspects that are known to affect the efficiency of these domains, such as the number of variables, without affecting precision. These techniques are inspired in others used in the context of compiler optimizations, such as expression reassociation and variable trimming. We present several such techniques and provide an extensive experimental evaluation of over 1100 program modules taken from both production code and classical benchmarks. This includes the Spectector cache analyzer, the s(CASP) system, the libraries of the Ciao system, the LPdoc documenter, the PLAI analyzer itself, etc. The experimental results are quite encouraging: we have obtained significant speed-ups, and, more importantly, the number of modules that require a timeout was cut in half. As a result, many more programs can be analyzed precisely in reasonable times., Comment: 61 pages, 10 figures, 7 tables, submitted to ICLP 2024

We present a scheme for the implementation of fast arbitrary qubit gates in the ground state of the negatively charged nitrogen-vacancy (NV$^-$) defect in diamond. The protocol is especially useful in the low-field regime and for high-frequency sensing applications. It constitutes an extension to the NV-ERC technique, which has demonstrated efficient initialization and readout of the double quantum transition with no leakage to any third level thanks to an effective Raman coupling. Here we derive a full theoretical framework of the scheme, identifying the complete unitary associated to the approach, and more specifically the relevant basis change for each of two characteristic pulse durations. Based on this insight, we propose a scheme to perform fast qubit transformations in the double quantum transition. We study its robustness with respect to pulse-timing errors resulting from faulty identification of system parameters or phase-control limitations. We finally demonstrate that the technique can also be implemented in the presence of unknown electric or strain fields., Comment: 26 pages, 6 figures, comments welcome

We study the relative asymptotics of two sequences of multiple orthogonal polynomials corresponding to two Nikishin systems of measures on the real line, the second one of which is obtained from the first one perturbing the generating measures with non-negative integrable functions. Each Nikishin system consists of two measures., Comment: 21 pages

Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours., Comment: Preprint of a paper accepted at SAS 2024

Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and many for other languages), as CiaoPP, are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with state-of-the-art solvers, including Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning (sparse-linear and symbolic) regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check if it is actually a solution of the recurrence. Our prototype implementation and its experimental evaluation within the context of the CiaoPP system show quite promising results. Overall, for the considered benchmarks, our approach outperforms state-of-the-art cost analyzers and recurrence solvers, and solves recurrences that cannot be solved by them. Under consideration in Theory and Practice of Logic Programming (TPLP)., Comment: Under consideration in Theory and Practice of Logic Programming (TPLP). Extended, revised version of our work published in ICLP (Klemen et al. 2023, arXiv:2309.07259). arXiv admin note: text overlap with arXiv:2309.07259

Advances in natural language processing techniques, such as named entity recognition and normalization to widely used standardized terminologies like UMLS or SNOMED-CT, along with the digitalization of electronic health records, have significantly advanced clinical text analysis. This study presents ClinLinker, a novel approach employing a two-phase pipeline for medical entity linking that leverages the potential of in-domain adapted language models for biomedical text mining: initial candidate retrieval using a SapBERT-based bi-encoder and subsequent re-ranking with a cross-encoder, trained by following a contrastive-learning strategy to be tailored to medical concepts in Spanish. This methodology, focused initially on content in Spanish, substantially outperforming multilingual language models designed for the same purpose. This is true even for complex scenarios involving heterogeneous medical terminologies and being trained on a subset of the original data. Our results, evaluated using top-k accuracy at 25 and other top-k metrics, demonstrate our approach's performance on two distinct clinical entity linking Gold Standard corpora, DisTEMIST (diseases) and MedProcNER (clinical procedures), outperforming previous benchmarks by 40 points in DisTEMIST and 43 points in MedProcNER, both normalized to SNOMED-CT codes. These findings highlight our approach's ability to address language-specific nuances and set a new benchmark in entity linking, offering a potent tool for enhancing the utility of digital medical records. The resulting system is of practical value, both for large scale automatic generation of structured data derived from clinical records, as well as for exhaustive extraction and harmonization of predefined clinical variables of interest.

With a single circulating vector-borne virus, the basic reproduction number incorporates contributions from tick-to-tick (co-feeding), tick-to-host and host-to-tick transmission routes. With two different circulating vector-borne viral strains, resident and invasive, and under the assumption that co-feeding is the only transmission route in a tick population, the invasion reproduction number depends on whether the model system of ordinary differential equations possesses the property of neutrality. We show that a simple model, with two populations of ticks infected with one strain, resident or invasive, and one population of co-infected ticks, does not have Alizon's neutrality property. We present model alternatives that are capable of representing the invasion potential of a novel strain by including populations of ticks dually infected with the same strain. The invasion reproduction number is analysed with the next-generation method and via numerical simulations., Comment: 37 pages and 4 figures

The liberalisation of the European passenger railway markets through the European Directive EU 91/440/EEC states a new scenario where different Railway Undertakings compete with each other in a bidding process for time slots. The infrastructure resources are provided by the Infrastructure Manager, who analyses and assesses the bids received, allocating the resources to each Railway Undertaking. Time slot allocation is a fact that drastically influences the market equilibrium. In this paper, we address the time slot allocation problem within the context of a liberalized passenger railway market as a multi-objective model. The Infrastructure Manager is tasked with selecting a point from the Pareto front as the solution to the time slot allocation problem. We propose two criteria for making this selection: the first one allocates time slots to each company according to a set of priorities, while the second one introduces a criterion of fairness in the treatment of companies to incentive competition. The assessment of the impact of these rules on market equilibrium has been conducted on a liberalized high-speed corridor within the Spanish railway network., Comment: 32 pages and 6 figures

For the Riesz and logarithmic potentials, we consider greedy energy sequences $(a_n)_{n=0}^\infty$ on the unit circle $S^1$, constructed in such a way that for every $n\geq 1$, the discrete potential generated by the first $n$ points $a_0,\ldots,a_{n-1}$ of the sequence attains its minimum value (say $U_n$) at $a_n$. We obtain asymptotic formulae that describe the behavior of $U_n$ as $n\to\infty$, in terms of certain bounded arithmetic functions with a doubling periodicity property. As previously shown in \cite{LopMc2}, after properly translating and scaling $U_n$, one obtains a new sequence $(F_n)$ that is bounded and divergent. We find the exact value of $\liminf F_n$ (the value of $\limsup F_n$ was already given in \cite{LopMc2}), and show that the interval $[\liminf F_n,\limsup F_n]$ comprises all the limit points of the sequence $(F_n)$., Comment: 20 pages. Some minor text modifications and typos were corrected

Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and other languages) are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions that are equivalent to (or a bound on) them. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with current solvers, such as Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning sparse regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check whether such function is actually a solution of the recurrence. We have implemented a prototype and evaluated it with recurrences generated by a cost analysis system (the one in CiaoPP). The experimental results are quite promising, showing that our approach can find closed-form solutions, in a reasonable time, for classes of recurrences that cannot be solved by such a system, nor by current CASs., Comment: In Proceedings ICLP 2023, arXiv:2308.14898

In this paper we prove the null controllability of a one-dimensional degenerate parabolic equation with a weighted Robin boundary condition at the left endpoint, where the potential has a singularity. We use some results from the singular Sturm-Liouville theory to show the well-posedness of our system. We obtain a spectral decomposition of a degenerate parabolic operator with Robin conditions at the endpoints, we use Fourier-Dini expansions and the moment method introduced by Fattorini and Russell to prove the null controllability and to obtain an upper estimate of the cost of controllability. We also get a lower estimate of the cost of controllability by using a representation theorem for analytic functions of exponential type., Comment: arXiv admin note: substantial text overlap with arXiv:2304.00178, arXiv:2302.01197

We begin our analysis with the study of two collections of lattice paths in the plane, denoted $\mathcal{D}_{[n,i,j]}$ and $\mathcal{P}_{[n,i,j]}$. These paths consist of sequences of $n$ steps, where each step allows movement in three directions: upward (with a maximum displacement of $q$ units), rightward (exactly one unit), or downward (with a maximum displacement of $p$ units). The paths start from the point $(0,i)$ and end at the point $(n,j)$. In the collection $\mathcal{D}_{[n,i,j]}$, it is a crucial constraint that paths never go below the $x$-axis, while in the collection $\mathcal{P}_{[n,i,j]}$, paths have no such restriction. We assign weights to each path in both collections and introduce weight polynomials and generating series for them. Our main results demonstrate that certain matrices of size $q\times p$ associated with these generating series can be expressed as matrix continued fractions. These results extend the notable contributions previously made by P. Flajolet and G. Viennot in the scalar case $p=q=1$. The generating series can also be interpreted as resolvents of one-sided or two-sided difference operators of finite order. Additionally, we analyze a class of random banded matrices $H$, which have $p+q+1$ diagonals with entries that are independent and bounded random variables. These random variables have identical distributions along diagonals. We investigate the asymptotic behavior of the expected values of eigenvalue moments for the principal $n\times n$ truncation of $H$ as $n$ tends to infinity., Comment: 48 pages, 3 figures

Ordinary differential equation (ODE) models used in mathematical epidemiology assume explicitly or implicitly large populations. For the study of infections in a hospital this is an extremely restrictive assumption as typically a hospital ward has a few dozen, or even fewer, patients. This work reframes a well-known model used in the study of the spread of antibiotic-resistant bacteria in hospitals, to consider the pathogen transmission dynamics in small populations. In this vein, this paper proposes a Markov chain model to describe the spread of a single bacterial species in a hospital ward where patients may be free of bacteria or may carry bacterial strains that are either sensitive or resistant to antimicrobial agents. We determine the probability law of the \emph{exact} reproduction number ${\cal R}_{exact,0}$, which is here defined as the random number of secondary infections generated by those patients who are accommodated in a predetermined bed before a patient who is free of bacteria is accommodated in this bed for the first time. Specifically, we decompose the exact reproduction number ${\cal R}_{exact,0}$ into two contributions allowing us to distinguish between infections due to the sensitive and the resistant bacterial strains. Our methodology is mainly based on structured Markov chains and the use of related matrix-analytic methods. This guarantees the compatibility of the new, finite-population model, with large population models present in the literature and takes full advantage, in its mathematical analysis, of the intrinsic stochasticity., Comment: 30 pages, 9 figures

We prove the null controllability of a one-dimensional degenerate parabolic equation with drift and a singular potential. Here, we consider a weighted Neumann boundary control at the left endpoint, where the potential arises. We use a spectral decomposition of a suitable operator, defined in a weighted Sobolev space, and the moment method by Fattorini and Russell to obtain an upper estimate of the cost of controllability. We also obtain a lower estimate of the cost of controllability by using a representation theorem for analytic functions of exponential type., Comment: 19 pages. arXiv admin note: substantial text overlap with arXiv:2302.01197

We prove the null controllability of a one dimensional degenerate parabolic equation with drift and a singular potential. We study the case the potential arises at the left end point and the weighted Dirichlet boundary control is located at this point. We get a spectral decomposition of a suitable operator, defined in a weighted Sobolev space, involving Bessel functions and their zeros, then we use the moment method by Fattorini and Russell to obtain an upper estimate of the cost of controllability. We also obtain a lower estimate of the cost of controllability by using a representation theorem for analytic functions of exponential type., Comment: 17 pages

We consider several non-standard discrete and continuous Green energy problems in the complex plane and study the asymptotic relations between their solutions. In the discrete setting, we consider two problems; one with variable particle positions (within a given compact set) and variable particle masses, the other one with variable masses but prescribed positions. The mass of a particle is allowed to take any value in the range $0\leq m\leq R$, where $R>0$ is a fixed parameter in the problem. The corresponding continuous energy problems are defined on the space of positive measures $\mu$ with mass $\|\mu\|\leq R$ and supported on the given compact set, with an additional upper constraint that appears as a consequence of the prescribed positions condition. It is proved that the equilibrium constant and equilibrium measure vary continuously as functions of the parameter $R$ (the latter in the weak-star topology). In the unconstrained energy problem we present a greedy algorithm that converges to the equilibrium constant and equilibrium measure. In the discrete energy problems, it is shown that under certain conditions, the optimal values of the particle masses are uniquely determined by the optimal positions or prescribed positions of the particles, depending on the type of problem considered., Comment: This is a revised and improved version of the paper. Accepted for publication in Analysis and Mathematical Physics. 29 pages

Audio fingerprinting is a technique used to identify and match audio recordings based on their unique characteristics. It involves creating a condensed representation of an audio signal that can be used to quickly compare and match against other audio recordings. The fingerprinting process involves analyzing the audio signal to extract certain features, such as spectral content, tempo, and rhythm, among other things. In this paper, we present SpectroMap, an open-source GitHub repository for audio fingerprinting written in Python programming language. It is composed of a peak search algorithm that extracts topological prominences from a spectrogram via time-frequency bands. In this paper, we introduce the algorithm functioning with two experimental applications in a high-quality urban sound dataset and environmental audio recordings to describe how it works and how effective it is in handling the input data. Finally, we have posed two Python scripts that would reproduce the proposed case studies in order to ease the reproducibility of our audio fingerprinting system., Comment: 12 pages, 5 figures

We study certain inequalities and a related result on weighted Sobolev spaces on bounded John domains in $\mathbb{R}^n$. Namely, we prove the existence of a right inverse for the divergence operator, along with the corresponding a priori estimate, the improved and the fractional Poincar\'e inequalities, the Korn inequality and the local Fefferman-Stein inequality. All these results are obtained on weighted Sobolev spaces, where the weight is a power of the distance to the boundary. In all cases the exponent of the weight $d(\cdot,\partial\Omega)^{\beta p}$ is only required to satisfy the restriction: $\beta p>-(n-\dim_A(\partial\Omega))$, where $p$ is the exponent of the Sobolev space and $\dim_A(\partial\Omega)$ is the Assouad dimension of the boundary of the domain. According to our best knowledge, this condition is less restrictive than the ones in the literature., Comment: 21 pages, 2 figures

Light-harvesting complexes in natural photosynthetic systems, such as those in purple bacteria, consist of photo-reactive chromophores embedded in densely packed "antenna" systems organized in well-defined nanostructures. In the case of purple bacteria, the chromophore antennas are composed of natural J-aggregates such as bacteriochlorophylls and carotenoids. Inspired by the molecular composition of such biological systems, we create a library of organic materials composed of densely packed J-aggregates in a polymeric matrix, in which the matrix mimics a protein scaffold. This library of organic materials shows polaritonic properties which can be tuned from the visible to the infrared by choice of the model molecule. Inspired by the molecular architecture of the light-harvesting complexes of \textit{Rhodospirillum molischianum} bacteria, we study the light-matter interactions of J-aggregate-based nanorings with similar dimensions to the analogous natural nanoscale architectures. Electromagnetic simulations show that these nanorings of J-aggregates can act as resonators, with subwavelength confinement of light while concentrating the electric field in specific regions. These results open the door to bio-inspired building blocks for all-organic metamaterials while offering a new perspective on light-matter interactions at the nanoscale in densely packed organic matter in biological organisms including photosynthetic organelles., Comment: Including supplementary information

Frouros is an open-source Python library capable of detecting drift in machine learning systems. It provides a combination of classical and more recent algorithms for drift detection: both concept and data drift. We have designed it with the objective of making it compatible with any machine learning framework and easily adaptable to real-world use cases. The library is developed following a set of best development and continuous integration practices to ensure ease of maintenance and extensibility. The source code is available at https://github.com/IFCA/frouros., Comment: 11 pages, 1 table