ABSTRACT. For many software engineering researchers, the need to verify software formally does not take much convincing. Between intellectual acceptance to practical application, however, the gap is wide. With notable exceptions, particularly in life-critical software, industry does not use much formal verification. For several decades Eiffel users have been convinced that at least a degree of formality is essential, and have seen the benefits in the quality of the systems they produce. This experience has largely been based on run-time verification, but the development of the AutoProof environment is making the goal of static proofs more realistic.

To succeed, static verification (that is to say, proofs) should move from its current “heroic” status to a normal, almost casual, component of the software engineer’s everyday routine, at the same level of obviousness and acceptance as, for example, type checking or configuration management: it should become “Verification As A Matter Of Course” (VAMOC) or, to coin a shorter name, Invisible Verification.

How realistic a goal is it? This talk will examine lessons from the Eiffel experience including the automated proofs of entire libraries, present the AutoProof architecture, examine frankly the remaining scientific and engineering obstacles, and sketch a possible path towards widespread Invisible Verification.

ABSTRACT. Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method. This article provides definitions, operators, and proofs of properties about relations and orders with a focus on monomial orders, that are total orders compatible with the monoid operation. More than its definition and proved properties, we define several of them, among them the lexicographic and grevlex orders. For the sake of genericity, we formalize the grading of an order, a high-level operator that transforms a binary relation into another one, and we prove that grading an order preserves many of its properties, such as the monomial order property. This leads us to the definition and properties of four different graded orders, with very factorized proofs. We therefore provide a comprehensive and user-friendly Rocq library about orders, including monomial and graded orders, that contains more than 700 lemmas.

ABSTRACT. Dynamic memory allocation is widely used in C programs, but it increases runtime-management complexity and complicates reasoning about allocation lifetime and pointer propagation. This paper presents an allocation-oriented escape analysis implemented on top of Frama-C and its Eva plug-in for identifying heap allocations that can be conservatively promoted to stack storage. The analysis records allocation sites, aliases, de-allocation points, propagation through function calls, assignments to global variables, writes through output parameters, and return-based escape paths.

Unlike traditional compiler optimizations that operate on internal intermediate representations, the proposed approach exports allocation behavior as structured and explainable JSON summaries suitable for external tools and source-level transformation workflows. Based on these summaries, we implement an experimental heap-to-stack promotion pipeline that selects non-escaping allocations, rewrites eligible heap allocations into stack-based local declarations, and removes obsolete de-allocation calls.

The approach is intentionally conservative: uncertain propagation paths are treated as escaping in order to preserve transformation safety. The workflow is evaluated on seventeen open-source C repositories, including cmark and pvsneslib, where the generated summaries successfully guide repository-scale source-to-source transformations. The results show that allocation-oriented escape summaries can support explainable source-level memory refactoring and practical heap-to-stack promotion workflows for existing C codebases.

ABSTRACT. Serverless platforms execute fine-grained functions on demand, but real applications must compose many functions into workflows. The interfaces used for this today—AWS Step Functions, Azure Durable Functions, Apache OpenWhisk Composer—describe compositions as verbose JSON or host-language glue, run them through an external orchestrator, and perform no static checking of the data exchanged between functions, so wiring mistakes surface only at run time, after a container has been provisioned and the request billed. We present Dagular, a system that rethinks serverless orchestration along three axes. (i) A concise functional DSL expresses workflows with let-bindings, conditionals, parallel map, first-class and curried functions, and action invocation as ordinary expressions, compiling to a JSON abstract syntax tree (AST). (ii) A native runtime embedded in the OpenWhisk controller interprets that AST in continuation-passing style over futures, so that independent sub-expressions execute concurrently by default and let-bound results are computed once and shared: parallelism is the default and serialisation is what costs a data dependency. (iii) A gradually-typed front-end adds, before deployment, an import system, a gradual type checker, existence validation of referenced actions, a self-bootstrapping Redis-backed schema store populated from ordinary use, and a common-subexpression-elimination (CSE) pass that removes redundant invocations of pure actions. On a single-node OpenWhisk deployment the front-end rejects six of seven representative error classes before deployment (against none for the untyped baseline), adds compile overhead linear in program size and bounded by a factor below two, and deterministically removes redundant billed pure invocations; the runtime realises implicit parallelism, running a k-way independent workflow in ≈T rather than ≈kT; and the DSL expresses common workflow patterns in a fraction of the lines mainstream interfaces require.

ABSTRACT. This paper studies two techniques for building a fast, instrumentable instruction-set interpreter, using a Nintendo Game Boy emulator (Mithril, written in Zig) as the testbed. First, we exploit the regular octal bitfield structure (x, y, z, p, q) of the Sharp LR35902/Zilog Z80 opcode space to replace a hand-enumerated switch dispatcher of more than 500 arms with a compact, parameterized decoder. In a same-codebase controlled benchmark over 50 million iterations, the algorithmic decoder runs at 10.77 ns/op (92.7 Mops/s) against the dispatcher’s 18.75 ns/op (53.3 Mops/s), a 1.74× improvement; we attribute a structurally certain share to an eliminated metadata-materialization-and-double-dispatch stage and advance the remaining micro-architectural effects as hypotheses rather than measured facts. Second, we present a concurrent, blocked-by-default Lua instrumentation engine that dispatches hook callbacks to a host thread pool while suspending the emulation thread at the exact instruction boundary where a hook fires, via an atomic barrier and condition-variable protocol. We describe the protocol formally and argue, on classical monitor/happens-before grounds, that it yields deterministic, race-free state inspection and patching without degrading host frame rates. Correctness is validated against the Blargg CPU test suite, the dmg-acid2 PPU test, and Game Boy Doctor register-parity auditing; the source and benchmark are publicly available.

ABSTRACT. Rewriting logic, and its implementation in the rewriting engine Maude, provides a flexible semantic and logical framework that has been extensively used for the analysis of a wide range of systems, from programming languages to cyber-physical systems. Although pure type systems have been specified in rewriting logic as object logics, and state monads have been shown to be definable in Maude, there is still no full implementation in Maude of higher-order functions that is sufficiently flexible for general users. In this paper, we show how higher-order programming can be made available in Maude through a natural and declarative encoding of higher-order iterators and lambda functions. We present two alternative approaches to achieve this goal, and compare them in terms of expressiveness and efficiency. Our ultimate objective is to give Maude specifiers not only the possibility of writing higher-order functions directly in Maude, but also the infrastructure needed to simplify the specification of rewrite-theory transformations. Such transformations are a common task in verification tasks using Maude and they could substantially benefit from the modules proposed in this paper.

ABSTRACT. Missing regions turn visual description into an underdetermined reasoning problem: a model must distinguish visible evidence from a plausible account of content it cannot see. We present Reasoning Behind Reconstruction, an English--Romanian benchmark built from 1,000 synthetically masked artworks and 3,000 independent bilingual annotations. Each annotation records visible cues, a hypothesis about the hidden region, and judgments of abstention, confidence, and difficulty. We evaluate Qwen2-VL with zero-shot prompting, three retrieved demonstrations, and low-rank adaptation. On the fixed test split, adaptation improves all 12 reported field--language--metric entries over zero-shot inference and gives the best score in 10. Hidden-content CIDEr rises from 0.0364 to 0.3079 in English and from 0.0043 to 0.2418 in Romanian, while three-shot prompting gives the highest English hidden-content token-F1. Qualitative examples show why text similarity alone is insufficient: globally plausible descriptions can still refer to the wrong image region. These results establish reference alignment, not calibrated uncertainty or historical validity. The benchmark supplies aligned variables for future grounding, bilingual-consistency, and abstention constraints.

ABSTRACT. We propose a data-aware candidate selection method for NL2SQL translation based on separating instances and provenance.

We implement this approach and evaluate it against three natural baselines on a subset of BIRD-DEV.

Experiments show that our method significantly outperforms baselines when only two or three candidates are given and no consistency score is available. The code of our prototype can be found at https://github.com/staskikotx/SISelection.

ABSTRACT. Medical pre-triage lies at the intersection of user-facing digital health, natural language processing, and machine-learning support for early care guidance. Existing symptom-checking workflows still face important gaps related to ambiguous free-text descriptions, variable triage reliability, and the insufficient separation between automated classification and clinical decision-making. This paper presents an intelligent medical pre-triage assistant based on natural language processing. The system assigns symptom descriptions to three orientative levels of care: self-monitoring, consultation with a general practitioner, and urgent care. The classification component evaluates Transformer models through full fine-tuning and parameter-efficient fine-tuning, including low-rank adaptation, bottleneck adapters, and frozen encoder training. The triage classifier is preceded by an input validation layer that combines deterministic rules with intent classification, and the output is complemented by semantic retrieval from a medical question answering resource. The experimental evaluation uses a fixed train, validation, and test split derived from SymCAT, with 701 examples and a final test set of 106 examples. BioMedBERT achieves the best full fine-tuning result, with an F1-score of 0.8512 and an area under the curve of 0.9272. Among efficient methods, the BioMedBERT bottleneck adapter reaches an F1-score of 0.8506, while low-rank adaptation is highly competitive for DistilBERT and RoBERTa. The results indicate that specialized biomedical Transformers are effective for this task, but compact or parameter-efficient variants can provide competitive alternatives for interactive applications. The system remains orientative and does not replace clinical evaluation.

ABSTRACT. This paper does not introduce a new framework. Instead, it critically evaluates a previously proposed approach through formal analysis and independent simulations informed by patient-derived data. Our study makes three main contributions. First, we provide a mathematical formulation of the original three-stage workflow and specify the interactions among agents at a finer level of detail, thereby improving methodological clarity and reproducibility. The second thing that we do is analyze results reported on RadGenome-ChestCT. We have taken the authors' numbers as well as images and re-done them to show more clearly what actually is going on: CE-F1 score for clinically effectiveness goes from 0.253 to 0.399, which is a relative improvement of 57.7\% and linguistic scores don't change much. What is behind this, we believe, is the structure of clinical reports. As the third contribution, we did our own experiments using real disorder-prevaluation information taken from 2,000 RadGenome-ChestCT cases and artificial reader models. We have simulated the same improvement step after the initial step that was reported by the main research, F1 score rises to 0.937 from 0.754, and showed that pooling of multiple agents rather than repeating discussions without evidence can explain most improvements. Throughout the whole work, we clearly mark which parts refer to the results of the source study and which are the main parts with our contributions. In addition, we point out some practical issues, quality of retrieval, computation expenses, and the importance of human checking, and argue that our paper can be the backbone for understanding the underlying mechanisms of hierarchical consensus and as well as be a guide for doing a fair assessment when weights of models are kept confidential.

ABSTRACT. Deep convolutional networks achieve high accuracy on chest X-ray classification, but their predictions are often driven by regions outside the clinically relevant anatomy, which limits trust in automated diagnosis. I propose a two-stage pipeline that first trains a ResNet18 classifier and uses Score-CAM, a gradient-free class activation mapping method, to localize the region of interest (ROI) associated with the predicted class. The extracted ROI is then passed to a lightweight convolutional network equipped with a Convolutional Block Attention Module (CBAM), trained to refine the diagnosis using only the localized region. I evaluate the approach on the Kaggle Chest X-Ray Images (Pneumonia) dataset. Preliminary results show that the baseline ResNet18 classifier converges rapidly, reaching a training accuracy of 99.67% after 5 epochs. I report early convergence behaviour and describe the full experimental protocol for the ROI+attention stage, whose quantitative comparison against the baseline is part of ongoing evaluation.

ABSTRACT. Foundation models can encode rich medical-image representations, yet whether their latent geometry captures biologically meaningful tumor architecture beyond established clinicopathological markers remains unclear. We present EndoFormer, a biologically grounded neuro-symbolic framework for interrogating computed-tomography foundation-model (CT-FM) representations in adrenocortical carcinoma (ACC). Tumor-centered volumetric patches from the public Adrenal-ACC-Ki67-Seg cohort were encoded using a frozen CT-FM, and their patient-level and intratumoral representation geometry was examined to identify latent architectural phenotypes associated with tumor biology. Exploratory analyses revealed relationships between CT-FM representation architecture, tumor burden, and imaging heterogeneity, motivating size-adjusted characterization of intratumoral representation dispersion. To address optimism arising from exploratory concept discovery, incremental predictive information was subsequently assessed using a nested, leakage-resistant out-of-fold evaluation. Adding the nested CT-FM architectural descriptor to tumor size and Ki-67 yielded an out-of-fold area under the receiver operating characteristic curve of 0.829 versus 0.761 for the clinicopathological baseline and average precision increased from 0.315 to 0.528, while reducing the Brier score from 0.116 to 0.092 and log-loss from 0.371 to 0.308. Stratified bootstrap resampling showed a consistent directional advantage for the extended model across metrics, with 93.7-97.9% of replicates favoring incorporation of CT-FM information; the highest proportion (97.9%) was observed for improvement in logarithmic loss; leave-one-metastatic-case-out sensitivity analysis preserved positive AUC and average-precision increments in all seven analyses. Paired model-swap randomization supported improvement in probabilistic log-loss (P=0.042), although uncertainty around the AUC increment remained substantial because only seven metastatic events were available. These findings suggest that pretrained CT representations encode an intratumoral architectural phenotype that provides information complementary to conventional markers of ACC aggressiveness and illustrate a leakage-aware pathway from foundation-model representations toward biologically interpretable reasoning in rare-cancer artificial intelligence.

ABSTRACT. Programmable Logic Controllers (PLCs) are used within many applications across various industries: examples include monitoring solar cells, robot control (spraying toxic chemical substances; washing the face glasses of skyscrapers), packaging and labelling systems, nuclear power plants, railway control systems.

The International Electrotechnical Commission specifies syntax and semantics of programming languages for such programmable controllers in its standard IEC 61131, part 3. This standard covers the graphical language “Ladder Diagrams”, often also called Ladder Logic. According to a 2022 article in the journal “Manufacturing Tomorrow”, “Ladder Logic is the main programming method used for PLCs”.

The invited talk will cover how to provide a formal semantics to Ladder Logic programs running on a PLC, how to define a logic expressing safety properties, and discuss various methods for verifying that a program is safe, including the IC3 algorithm. It turns out that software model checking of real-world programs is feasible, i.e., Ladder Logic verification provides a success story where a Formal Methods scales to industrial needs. Verification examples from the railway domain will illustrate the approach.

ABSTRACT. Electoral Manipulation under Media Influence (EMMI) models a setting in which an attacker selects a set of costly media strategies in order to persuade voters and make a designated candidate successful. Each strategy influences a subset of voters. A voter switches to the designated candidate once the number of selected strategies influencing that voter reaches a prescribed threshold. In this paper, we study the deterministic threshold model of EMMI under the plurality rule and the co-winner convention, focusing on the minimum-cost formulation.

We first obtain logarithmic inapproximability for Minimum-Cost EMMI, even for two candidates, unit strategy costs, and unit voter thresholds, and show that NP-hardness persists when every strategy influences only three voters. On the positive side, we formulate the unit-threshold case as an instance of Submodular Set Cover, obtaining a greedy $(1+\ln n)$-approximation for an arbitrary number of candidates, matching the logarithmic lower bound.

We further study the case where the influence sets are laminar. We prove that EMMI-Laminar is NP-hard when the number of candidates is part of the input, even under unit costs and unit thresholds. On the positive side, we give a polynomial-time algorithm for the two-candidate unit-cost unit-threshold laminar case. We then extend our algorithmic results to a fixed number of candidates, obtaining exact algorithms for the unit-cost unit-threshold case. We also give parameterized algorithms for unit-cost instances with arbitrary thresholds using chain decompositions. Finally, we present an integer linear programming formulation that provides an exact mathematical model for the problem.

ABSTRACT. We motivate an axiomatic definition of probabilistic algorithms (PAs) by four postulates covering random branching time, abstract states, background, and random bounded exploration. Then, we introduce probabilistic Abstract State Machines (pASMs) and show that they specify PAs. Finally, we prove that every PA satisfying these postulates can be simulated step-by-step by a behaviourally equivalent pASM with the same signature and background.

ABSTRACT. We present a formal proof, carried out in F*, of the soundness and the completeness of an LTL model checking algorithm based on SCC decomposition. This algorithm is a critical component in model checking, where it is used for the verification of temporal properties of systems. We begin by introducing the original formulation of the algorithm and we provide a faithful implementation in F*. We then identify the key invariants required for verification and state the essential lemmas that guide the annotation of the program, ultimately enabling a mechanized proof of both soundness and completeness within F*.

ABSTRACT. Determining exactly the reliability of a network is known to be a daunting task (#P-complete in general). That is why approximate solutions have started to be investigated since quite some time, and artificial neural networks approaches have also been suggested. Still, learning the exact coefficients of the associated reliability polynomials is an approach which has not been pursued before. The starting point should be a database of such coefficients (for training), while, unfortunately, none seems to be available. That is why, in this paper, we are going to introduce an algorithm which counts the number of shortest paths from input (start) to output (terminus) for a particular class of two-terminal networks known as hammocks. These numbers are the first non-zero coefficients of the reliability polynomials of hammock networks, hence an essential step towards building a training database. We prove the optimality of the algorithm and use it to generate our first training dataset, while eying the second coefficient as the next step. Conclusions and future directions of research are going to end the paper.

ABSTRACT. Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.

ABSTRACT. We present the Fibonacci-Mandelbrot (FM) Forward Operator, an O(N) time and space complexity algorithm that bypasses the O(N^2) overhead of standard dense matrix-vector multiplication. With low arithmetic intensity, the algorithm minimizes floating-point round-off accumulation, resulting in a backward stable operator. The O(N) complexity and computational stability allow us to apply the operator in standard power iteration up to a recursion depth of n=44 (order N > 7 x 10^8). We use power iteration to measure the performance of the operator; this application reveals that the iteration sequence traces out a trajectory on a toroidal manifold. These periodic cycles become invariant for matrices with defective eigenspaces (n < 12). This paper establishes the computational foundations of the Forward Operator; subsequent work will introduce a paired O(N) inverse operator.

ABSTRACT. Human activity and exercise recognition using data collected from wearable sensors is central to remote monitoring and rehabilitation medicine. There are several obstacles which limit real-world deployment: the scarcity of labeled data and the high variability of execution between executions of the same exercise. This paper proposes to study these obstacles through multiple complementary experiments, to ensure different point of views for a better justification and result explanation.

We make five contributions: (i) evaluating time-domain augmentations and signal reconstruction on model performance, (ii) pairing REBAR self-supervised pretraining with a representation-quality analysis, (iii) examining cross-dataset transfer with supervised pretraining and domain aligmnent (MDD, DANN), (iv) investigating inter-patient variability via patient-aware few-shot assessment, and (v) testing pseudo-labeling for unlabeled target evaluation.

ABSTRACT. Emergency departments operate under variable and often difficult-to-predict demand, which can affect waiting times, staff workload, and resource allocation. This paper investigates daily emergency department attendance in Cluj-Napoca, Roma- nia, during the 2020–2023 period, with a focus on temporal, calendar-related, seasonal, and climate-related factors. Medical records were aggregated at daily level and integrated with climate variables, including daily mean, minimum, and maximum tem- perature, as well as minimum and maximum Universal Thermal Climate Index values. Temperature outliers were identified using historical daily percentile thresholds computed from the 1995– 2024 period. The analysis first examines baseline temporal patterns in emer- gency attendance. A statistically significant weekend–weekday difference was identified, with fewer reported emergency cases during weekends. The study then evaluates whether climate- related variables add predictive information beyond temporal and calendar-related predictors. For this purpose, a HistGradi- entBoostingRegressor was used to compare a baseline calendar model with an extended calendar–climate model. The inclusion of climate variables modestly improved predictive performance, reducing MAE from 15.34 to 14.83 and increasing R2 from 0.653 to 0.673. Feature-importance analysis showed that day of week and lagged attendance variables remained dominant, while climate-related variables provided a weaker additional signal.

ABSTRACT. This study investigates a hierarchical deep learning approach for classifying Alzheimer’s disease stages from brain MRI scans using convolutional neural networks. The original four-class problem (NonDemented, VeryMildDemented, MildDemented and ModerateDemented) is decomposed into a binary classifier (NonDemented vs Demented) followed by a subtype classifier for the three dementia-related classes. The experiments use the Augmented Alzheimer MRI Dataset V2, which presents notable class imbalance. Transfer learning models based on VGG16 and ResNet50, pretrained on ImageNet, are adapted with additional dense layers, batch normalization, dropout and selective fine-tuning. Performance is evaluated using accuracy, confusion matrices, precision, recall and F1-score. The hierarchical VGG16 model achieves an overall accuracy of 99.16% and markedly reduces misclassification of VeryMildDemented cases as NonDemented compared with a direct multiclass baseline, while the hierarchical ResNet50 model attains lower but acceptable performance. These findings indicate that hierarchical CNN-based classification can enhance MRI-based staging of Alzheimer’s disease.

ABSTRACT. The rapid development of autonomous driving and intelligent transportation systems requires perception modules that remain reliable under adverse environmental conditions. Relying on a single sensor modality, such as RGB cameras or LiDAR, can lead to performance degradation under challenging conditions. This paper presents a modular RGB–LiDAR fusion framework for road traffic scenes, combining YOLOv8m for 2D object detection with the TED-S transformation-equivariant 3D detector for LiDAR point clouds. Fusion is performed at decision level by projecting TED-S 3D bounding boxes onto the image plane and associating them with YOLOv8m outputs using IoU-constrained Hungarian matching and confidence re-weighting. The system is evaluated on the TUMTraf dataset, after converting its OpenLABEL annotations to a KITTI/OpenPCDet-compatible format, and complemented by baseline experiments on KITTI. The results demonstrate that the proposed multimodal pipeline effectively combines 2D and 3D information to maintain accurate detections and consistent spatial localization in complex urban intersection scenarios, supporting robust monitoring in smart traffic infrastructure.

ABSTRACT. Ground deformation caused by precipitation is influenced by numerous factors, such as geology, soil properties, urban infrastructure, and the delayed response of the ground to accumulated rainfall. This study investigates the relationship between accumulated precipitation and ground deformation in Câmpina, Romania, using Persistent Scatterer Interferometric Synthetic Aperture Radar (PS-InSAR) time series provided by the European Ground Motion Service, recorded between 2020 and 2024. These Persistent scatterers were selected from regions identified as critical on the landslide risk map provided by the municipality. The Bayesian Estimator of Abrupt Change, Seasonal Change, and Trend (BEAST) method was used to detect change points in both the deformation and the accumulated precipitation time series. First, univariate BEAST was applied separately to the PS-InSAR and precipitation data. The results were then compared with those obtained using the experimental multivariate implementation of BEAST which models deformation and precipitation simultaneously. The multivariate approach detected fewer deformation change points, produced lower posterior probabilities, and much wider confidence intervals than the univariate analysis. Only five deformation change points were common to both methods in the PS-InSAR time series, while no common precipitation change points were identified. These results indicate that, for the investigated area, the current multivariate implementation introduces greater uncertainty than the univariate approach. This study provides a quantitative comparison of both methods and examines their suitability to investigate the effects of rainfall on ground motion. Several change points corresponding to increased subsidence rates occurred during or shortly after periods of high accumulated precipitation, suggesting a triggering effect for accelerated ground deformation.

ABSTRACT. Monitoring cultural heritage sites, such as Romanian churches, helps support their conservation over time. Since manually inspecting satellite imagery over large geographical areas is impractical, automated methods can substantially reduce the effort required for large-scale monitoring. This paper investigates whether combining a localization model with an image classifier improves church detection in satellite images. We train and evaluate three individual models: ResNet18 for classification, YOLOv8n for object detection, and U-Net for semantic segmentation; then compose them into two hybrid pipelines: one pairing U-Net with ResNet18, and another pairing YOLOv8n with ResNet18. Individual models are assessed via Stratified K-Fold Cross Validation; the hybrid pipelines are compared head-to-head on a held-out test set. The experimental results show that the U-Net + ResNet18 pipeline provides a more reliable solution than the YOLOv8n + ResNet18 pipeline for the data set considered.

ABSTRACT. Various Data Science problems, like regression, classification, or image reconstruction, could be equivalently formulated as optimization problems or variational inequality problems. In order to build iterative schemes for solving the later problems, it is convenient in many instances to transform them into appropriate fixed point problems $x = T(x)$, which naturally generate the Picard fixed point algorithm $x_{n+1}=T (x_n)$, $n\geq 0$. The main aim of this paper is to discuss the role of nonexpansive type mappings $T$ in designing convergent fixed point algorithms with applications to Data Science problems.

ABSTRACT. This research paper is about a custom DVRP framework and three adapted metaheuristics and the comparison between how each of them handle the problem. Each metaheuristic is adapted and improved for the problem and in the research it's showcased how each manages different test data.

ABSTRACT. The Montgomery ladder inherently resists simple power analysis (SPA) and, although originally designed for Montgomery curves, applies to any abelian group. Twisted Edwards curves are widely used for efficient digital signatures and encryption, yet ladder-based scalar multiplication on them has been little explored beyond the Edwards and generalized Edwards subfamilies. In this work we introduce the first native differential formulas for the full twisted Edwards family $E_{a,d}$ in the $(Y,Z)$ projective representation, generalizing the construction from Edwards curves. We investigate co‑$Z$ arithmetic and optimize the formulas for $E_{-1,d}$, achieving doublings of $1M + 4S + 2C$ that match Montgomery efficiency and improve over $(W,Z)$ by a factor of $6\times$, making them directly applicable to isogeny-based post-quantum protocols. For classical ECDH, addition remains costlier than $(W,Z)$, although co‑$Z$ on $E_{-1,d}$ yields $8M + 4S + 6C$, the lightest among $(Y,Z)$ methods, conditional on a multiplication‑free synchronization map. Future work will develop co‑$Z$ techniques for $(W,Z)$ and design a projective coordinate system that, via a cheap isomorphism, absorbs partial products during $Z$-coordinate synchronization.

ABSTRACT. We present a floating-point error and throughput study of four-bit (NVFP4) and eight-bit (FP8) low-precision inference for large language models on the NVIDIA GB10 Grace Blackwell superchip, a unified-memory desktop platform whose numerical behavior has not been characterized: published evaluations of these formats target datacenter GPUs. Low-bit formats promise large memory and bandwidth savings, but what accuracy they cost on this class of hardware, and where in the network the error arises, was unknown. We first derive an error model for NVFP4's two-level block scaling and propagate it through the transformer matrix-multiply stack, then validate the model's predictions with a per-layer error budget, end-to-end accuracy, and serving throughput measured on three open-weight Gemma 4 models. The measurements confirm the predictions: quantization error is approximately constant in the matrix contraction length, accuracy loss stays near one percentage point despite large per-layer numerical error, and FP8 delivers about 1.5 times the decode throughput of the 16-bit baseline. We also document a platform-specific kernel limitation that forces four-bit inference onto a weight-only fallback path. All results follow a pre-registered protocol with confidence intervals and paired significance tests, and a run manifest is released for reproducibility.

ABSTRACT. We study the Mackey-Glass delay differential equa- tion with Hill exponent n = 10, delay τ = 2, and final time T = 200. A method-of-steps Runge-Kutta solver is compared with a data-assisted, windowed physics-informed neural network trained on coarse trajectory samples and constrained by the differential equation residual. The PINN uses Fourier features, sine activations, ten overlapping time windows, delay-aware stitching, a residual-weight curriculum, and Adam followed by L-BFGS optimization in each window. Errors are measured with respect to a dense fixed-step Runge-Kutta trajectory used as a common scoring reference. On our hardware, the classical solver is both faster and more accurate, reaching a mean squared error of about 0.051 in a few seconds of CPU time. The PINN reaches an average mean squared error of about 0.121 over five random seeds and requires roughly 50-55 minutes of GPU training for a full stitched run. Although the method-of-steps error contains localized mid-horizon spikes, the PINN error is less spike-dominated on [50, 200] while remaining substantially larger near the initial segment. Overall, the results highlight the practical trade-off between accurate classical integration and a mesh-free differentiable surrogate that is considerably more expensive to train.

ABSTRACT. In this paper we will present some new fixed point theorems for nonself multi-valued contraction type operators in complete strong $b$-metric spaces endowed with a $b$-convex structure. Notice that a strong $b$-metric space is a set $X$ endowed with a functional $d:X\times X\to \mathbb{R}_+$ which satisfies the classical axioms of the metric, with the following modification of the triangle inequality axiom: $$d(x,y)\le d(x,z)+sd(z,y), \mbox{ for all } x,y,z\in X.$$ In this context, if $(X,d,s)$ is a strong $b$-metric space with coefficient $s\ge 1$, then we say that $X$ is endowed with a $b$-convexity structure if for every $x,y \in X$ with $x \ne y$ there exists $z \in X$ with $x \ne z \ne y$ such that $$d(x,y) = s\big( d(x,z) + d(z,y) \big).$$ One of the main result of this work is the following theorem: {\bf Theorem.} {\it Let $(X,d,s)$ be a complete strong b-metric space with coefficient $s \ge 1$, endowed with a $b$-convexity structure. Let $K \subset X$ be nonempty and compact and $F:K\to P_{b,cl}(X)$ be a multi-valued $\delta$-contraction, with $\delta\in [0,1)$. Suppose that, if $x\in \partial K$ then $F(x)\subset K$. Then $F$ has at least one fixed point.}

ABSTRACT. We consider the framework of a complete metric space. The following two classes of operators are important in our approach.

\begin{definition} Let $(X,d)$ be a metric space, $F:X\to P(X)$ be a multi-valued operator, $\beta\in (0,1)$ and $x\in X$. Consider the set $$I_\beta^x:=\{y\in F(x) : \beta d(x,y)\le D(x,F(x)) \}.$$ Then $F$ is called a multi-valued Feng-Liu $(\alpha,\beta)$-contraction if there exists $\alpha\in (0,\beta)$ such that for each $x\in X$ there is $y\in I^x_\beta$ satisfying $$D(y,F(y))\le \alpha d(x,y).$$ \end{definition}

\begin{definition}\label{Def1} {\rm (}\cite{KS}{\rm )} Let $\eta:[0,1)\to (\frac{1}{2},1]$ be a function defined by $\eta(a):=\frac{1}{1+a}$. Let $(X,d)$ be a metric space. Then $F:X\to P_{b,cl}(X)$ is called a multi-valued Kikkawa-Suzuki $\alpha$-contraction if $\alpha\in [0,1)$ and $$ x,y\in X \mbox{ with } \eta(\alpha) D(x,F(x))\le d(x,y) \mbox{ implies } H(F(x),F(y))\le \alpha d(x,y).$$ \end{definition}

In this paper we will discuss some fixed point theorems for two classes of cyclic multi-valued contractions: Feng-Liu type contractions and Kikkawa-Suzuki type contractions. An application to the best proximity points problem is given. Some stability properties for the fixed point inclusion, such as Ulam-Hyers stability, well-posedness in the sense of Reich and Zaslavski, and data dependence of the fixed point set are also proved. Finally, an extension of the Feng-Liu and Kikkawa-Suzuki approaches is given and a fixed point result for a Feng-Liu-Kikkawa-Suzuki contraction is obtained.

References:

[1] Feng, Y., Liu, S.: Fixed point theorems for multi-valued contractive mappings and multi-valued Caristi type mappings, J. Math. Anal. Appl. {\bf 317}, 103-112 (2006)

[2] Kikkawa, M., Suzuki, T.: Three fixed point theorems for generalized contractions with constants in complete metric spaces, Nonlinear Anal. {\bf 69}, 2942-2949 (2008)

ABSTRACT. In this talk, we will introduce a strict fixed point principle for multivalued Ćirić type contractions, similar with the strict fixed point result for $\alpha-$ contractions given by A. and G. Petrușel in Theorem 5.5 from [3]. The interested reader can find the detailed proof of the result for multivalued Ćirić type contraction type operators, as well as the discussion regarding well-posedness of the strict fixed point problem, Ulam-Hyers and Ostrowski stability, or data dependence in [2].

Then, using the admissible perturbation technique introduced by Professor I. A. Rus in [4], we will extend the result for operators that are not Ćirić type contractions, but one can construct a perturbation that satisfy the Ćirić type contraction condition. The consistency of the theory is motivated by some relevant examples (see also [1]). We will give another strict fixed point result for multivalued operators using the admissible perturbation technique, and discuss the well-posedness of strict fixed point problem, data dependence and stability results.

References: [1] Gheorghe, C.: "Strict fixed point and stability results for multivalued operators via the admissible perturbation technique", The Journal of Analysis, accepted (to appear 2026); [2] Gheorghe, C., Petrușel, A.: "Strict fixed point problem, stability results and retraction displacement condition for Picard operators", J. Nonlinear Convex Anal. 26(12) (2025), 3337–3348; [3] Petrușel, A., Petrușel, G.: "Some variants of the contraction principle for multi-valued operators, generalizations and applications", J. Nonlinear Convex Anal.20(10) (2019), 2187–2203; [4] Rus, I.A.: "An abstract point of view on iterative approximation of fixed points: Impact on the theory of fixed point equations", Fixed Point Theory 13, (2012),179–192.

ABSTRACT. The study of operators on Banach spaces, particularly nonexpansive ones and their extensions, highlights deep connections between classical results and modern research directions. In this paper, we present some results about the approximation of fixed points of enriched nonexpansive operators. For approximation of fixed points of enriched nonexpansive mappings in the framework of Banach space, we introduce a new three-step iteration scheme and establish convergence results. Further, we show that the new iteration process is faster than a number of existing iteration processes. To support the claim, we consider a numerical example and approximated the fixed point numerically by computer using Matlab. Enriched nonexpansive type operators are extremely important in the metric fixed point theory, both the theoretical point of view and especially for their large areas of applications.

ABSTRACT. Financial forecasting remains challenging due to changing market conditions and unstable relationships in finan- cial time series data. While recent studies increasingly employ complex machine learning and deep learning architectures, it remains unclear whether increased model complexity improves forecast stability over time. This study investigates the effec- tiveness of adaptive retraining strategies for improving predic- tive accuracy and temporal robustness in commodity spread forecasting. Using the Mitsui Commodity Prediction Challenge dataset, multiple forecasting approaches are evaluated, including Ridge regression, LightGBM, LSTM, CNN-LSTM, and ensemble models. Adaptive strategies based on rolling-window retraining and time-decay weighting are compared against static training configurations. Model performance is evaluated using the Infor- mation Coefficient (IC), rolling IC standard deviation, temporal regime gap, and volatility regime sensitivity. Experimental results show that adaptive retraining significantly improves forecast stability and predictive accuracy compared to static models. In particular, rolling-window Ridge regression achieves the best overall trade-off between accuracy and stability. In contrast, feature engineering, ensemble modeling, and increased model complexity fail to produce consistent improvements, with deep learning and gradient boosting models often underperforming simple regularized linear models. The findings suggest that adapting to changing market conditions plays a more significant role than model complexity in financial forecasting and emphasize adaptive retraining as a practical and robust strategy for unstable financial environments.