ABSTRACT. Matching logic (ML) is a minimal, foundational logic built around the notion of patterns — formulas interpreted as sets of elements — with native support for a least-fixpoint operator. Its expressive power and uniform treatment of structure and constraints make it a compelling substrate for domain-specific reasoning.

In this talk, we show how matching logic serves as a unifying foundation for inference systems across several domains. We begin with a self-contained introduction to matching logic: its syntax, semantics, and proof system. We then develop three case studies: (1) initial algebra semantics, where structural induction and primitive recursion are derived as theorems within matching logic rather than imposed as external rules; (2) rewrite-theory-generic reachability logic, where constrained constructor patterns are faithfully captured as matching logic theories; and (3) the K framework, where high-level language definitions are formally translated into matching logic theories, providing a rigorous denotational semantics for the K frontend.

Together, these results demonstrate that matching logic is a practical platform for deriving and certifying domain-specific reasoning systems within a single logical framework.

ABSTRACT. Generalization of two or more objects (terms, trees, forests, graphs, formulas, proofs, programs, …) is an object, which keeps common features of the given objects and shows how they differ. It is a fundamental concept for tasks where one is interested in extracting a common general pattern from the given concrete examples.

Anti-unification is a logic-based method to compute generalizations. It was introduced in the 1970s, motivated by an application in inductive reasoning. In recent years, there has been growing interest in anti-unification due to novel applications in various subareas of artificial intelligence and computer science, where anti-unification-based techniques have been successfully applied in analogical reasoning, logic-based learning, term set compression, program synthesis, programming by examples, software code clone detection, automated program repair, library learning, etc.

In this talk, we will give a survey on recently developed generalization algorithms in first-order and higher-order theories, consider their applications, and discuss some interesting research problems in this area.

ABSTRACT. Rewriting logic is a powerful and general, yet simple and intuitive, logic for specifying dynamic systems, and is particularly suitable to specify distributed computer systems in an object-oriented style. In rewriting logic, data types are defined by equational specifications (which operationally can be seen as rich term rewrite systems), while dynamic behaviors are specified by (possibly conditional) rewrite rules.

Maude is a programming/modeling language and high-performance analysis tool for rewriting logic. Maude supports a range of analysis methods for distributed systems formalized in rewriting logic, including: (a) simulation by rewriting; (b) reachability analysis by search; (c) various forms of temporal logic model checking; (d) symbolic analysis; and (e) various forms of theorem proving using associated tools. In addition, Maude models can also be subjected to statistical model checking using the umaudemc tool, so that Maude can analyze both the correctness and performance of distributed systems, with good predictive power.

Maude has been successfully applied to a wide range of sophisticated systems, including: large transport protocols, industrial cloud-based distributed transaction systems, biological systems, human cognition, programming and modeling language semantics and analysis, cyber-physical systems, and so on.

Maude’s generality and intuitive formalism also extends to real-time and cyber-physical systems, so that rewriting logic and Maude complements popular, but much less expressive, formalisms such as timed/hybrid automata and time(d) Petri nets, with the ability to formalize wide ranges of large real-time systems, as well as to provide formal semantics and analysis features to industrial modeling languages.

This tutorial gives an introduction to specification and analysis in Maude for first distributed systems and then to real-time systems. It also provides a sample of applications of Maude to such systems.

ABSTRACT. Visitor reviews are a valuable source of feedback for cultural institutions, yet the volume of free text accumulated by art museums makes manual interpretation infeasible. This paper presents an artificial-intelligence framework for binary sentiment classification of reviews of art museums in the United Kingdom. The text is vectorised with the pretrained Gensim Word2Vec Google News model (GN300), which represents every token by a vector of 300 numerical values. The resulting features are classified with the Extreme Gradient Boosting (XGBoost) algorithm, whose hyperparameter tuning is an NP-hard problem. To address this, a modified Sinh Cosh Optimizer, the Quasi-Reflexive Genetic SCHO (QGSCHO), is proposed; it combines quasi-reflexive learning initialisation with a uniform-crossover genetic replacement operator. Benchmarked against five competing optimisers on a public, class-imbalanced dataset using the Matthews correlation coefficient as objective, the QGSCHO-tuned XGBoost achieved the best central-tendency results, reaching an MCC of 0.7330 and an accuracy of 88.30 percent, and the improvements were confirmed by the Wilcoxon signed-rank test against several competitors.

ABSTRACT. Today, the agriculture industry faces multiple chal- lenges such as climate change, environmental regulations and cost reduction. A specific goal is to increase efficiency with respect to the consumption and application of herbicides in agricultural fields. The traditional method for distributing the herbicide is to spray herbicide uniformly in that area. This study proposes tackling this challenge by developing methods using Computer Vision and Machine Learning for precision spot herbicide spraying, reducing the consumption of herbicide, lowering the costs for farmers and improving the environment. In this study the aim was to train a semantic segmentation model, using the SegFormer architecture with the MiT-B5 encoder pretrained on ImageNet, with over 16,000 images of maize and weeds and their pixel-wise masks annotated in a process of pseudo-labeling where OpenCV was used. The trained model was applied within a distributed system, on drone footage and also integrated on an Edge AI system using NVIDIA Jetson Orin Nano Super for precision spraying.

ABSTRACT. Cultural heritage institutions increasingly look toward generative artificial intelligence as a means of deepening visitor engagement. Yet, most existing digital-museum solutions remain limited to passive content delivery. In prior work, we proposed a hybrid head-and-face swap pipeline combining Stable Diffusion-based inpainting, conditioned through IP-Adapter and ControlNet, with an InsightFace-established identity refinement stage. We demonstrated in an offline manner that the hybrid approach achieves higher biometric similarity than single-stage alternatives, while preserving the visual integrity of the artefact. The present paper reports the applied extension of that pipeline into a museum platform, piloted at the Oltenia Museum in Craiova, Romania. The core novel challenge we address is that the swap target scenes are themselves AI-generated recreations of historical contexts and must therefore be prepared in advance across a structured attribute space, including visitor age range, gender and skin tone, so that scene and visitor are visually coherent. We describe the attribute extraction pipeline applied to the visitor’s selfie, the visitor confirmation interface that handles classification uncertainty and the scene-selection logic that matches confirmed attributes to the closest available one. We further address the data-security and privacy model governing selfie and result storage. Images are transmitted over TLS, stored in encrypted form, processed transiently in server memory and deleted automatically upon result delivery, with no long-term retention of personally identifiable images.

ABSTRACT. Generative AI can be used for the contextualization of museum artefacts in historically inspired scenes. Such generated images could reflect expert opinions on the potential use of the artefacts and improve the interest of the visitors. However, direct generation does not always obey object geometry, texture, scale and placement. This paper introduces a pipeline for integrating museum vases into AI-generated environments inspired from the Bronze Age. The method detects vase-like objects in a starting scene using YOLOv8, segments it and removes it through LaMa inpainting and inserts a transparent museum-artefact image at the recovered location. A harmonization step then combines Stable Diffusion inpainting, Canny ControlNet and IP-Adapter to match the inserted artefact to the present lighting conditions. We evaluate the approach on 100 samples generated from 20 scenes and 5 museum artefacts, using MUSIQ and MANIQA for no-reference image quality, LPIPS for perceptual change, and DINOv2 cosine similarity for artefact preservation. The findings indicate that the proposed pipeline offers a practical method for producing cultural-heritage visualizations and avoids thus any hallucinations that are often related to generative AI for image generation.

ABSTRACT. Industrial environments are home to thousands of devices from dozens of vendors, and cataloguing them remains a largely manual, error-prone task. This paper presents IRIS (Industrial Recognition and Identification System), a registrydriven, multi-modal computer vision pipeline that identifies device vendors from screenshots taken with a headless browser without requiring model retraining when new vendors are introduced. IRIS combines two complementary evidence streams: a vision leg that pairs a YOLOv8-based logo detector fine-tuned on the IRIS Industrial Dataset with CLIP ViT-B/32 embedding similarity against a per-vendor reference image library, and an OCR leg powered by PaddleOCR with position-weighted fuzzy matching against a human-maintained registry. This zeroretraining extensibility means adding a new vendor requires only updating the registry and supplying reference images, with no training cycle. On the IRIS Industrial Dataset, the fused pipeline correctly identifies the device vendor in 95.5% of cases, ahead of either evidence stream on its own.

ABSTRACT. Reassembling a 3D object from its fragments is a key problem in archaeology, palaeontology, and medicine. The current work proposes four modular extensions to Jigsaw, the first end-to-end framework for multi-piece fracture assembly: (1)a pair attention bias acting as a learned soft regularizer; (2)gated double attention for iterative feature refinement; (3)Gabriel graph filtering for surface-faithful PointNet++ neighborhoods; and (4)ICP refinement for pairwise poses. On the Breaking Bad dataset, these modifications consistently improve out-of-distribution performance, with double attention yielding +2 to 5 points under data scarcity and Gabriel filtering reducing cross-domain chamfer distance by up to 10%. Data quantity remains the dominant factor, exceeding reduced-subset results by over 10 points.

ABSTRACT. As Human Action Recognition (HAR) models transition to privacy-sensitive Ambient Assisted Living (AAL) environments, preserving user identity becomes critical. Standard models operating on raw visual data are poorly suited for deployment due to privacy leaks. Therefore, we need to understand the behavior of these models on visual anonymization. In this paper, we develop a privacy-oriented evaluation framework for analyzing how video action recognition models behave under severe non-photorealistic anonymization. We present extensive empirical evaluations on two standard benchmarks, while both representatives are fine-tuned specifically on the anonymized datasets. Our findings revealed the capability of each representative for preserving the kinematic trajectories, essential for action recognition in the absence of textural and chromatic cues, along with the accuracy degradation under this severe abstraction.

ABSTRACT. Significant research studies have been assigned to advance the field of real-time semantic segmentation by designing deep learning architectures that exceed a 30 Frames per Second performance threshold. Recently, vision Mamba has shown great potential in modeling long-range dependencies at a lower computational cost, and limited research has been dedicated to vision Mamba models in real-time semantic segmentation for autonomous driving datasets. In this paper, we propose a hybrid convolutional-mamba network, HCMNet, that effectively combines a CNN-based encoder, for generating high-quality feature maps, with a vision Mamba-based decoder, to address the need for efficient long-range dependency modeling in real-time systems. Specifically, we develop a 2D optimized scanning technique, OS2D, for an efficient global context modeling, and an attention-based fusion module that combines the global and local information for enhanced reconstruction of the initial image resolution. The proposed model demonstrates an optimal balance between accuracy and inference speed through extensive experiments conducted on two representative autonomous driving datasets, Cityscapes and CamVid.

ABSTRACT. Autonomous vehicle perception requires both the detection of surrounding objects and an accurate estimate of their distance, yet no single sensor handles both tasks well: cameras detect and classify vehicles reliably but cannot measure depth from a single frame, while LiDAR provides precise 3D measurements but requires complex architectures and costly 3D annotations for object classification. This paper proposes an early fusion approach that assigns each task to the sensor best suited for it: a YOLOv8n network trained on camera images produces 2D bounding boxes, which are then used as spatial masks for the LiDAR point cloud via geometric projection onto the image plane. The DBSCAN clustering algorithm isolates the compact cluster corresponding to the vehicle surface within each masked subset, removing road reflections and background noise before distance estimation. The pipeline is developed and evaluated in the CARLA simulator on a custom dataset with automatically generated ground truth, and its robustness is assessed through an original five-level degradation protocol that progressively removes LiDAR points and injects Gaussian noise to emulate adverse weather. The detection module reaches a precision of 0.986 and mAP50 of 0.974 on in-domain data at approximately 200 FPS. Under degradation, DBSCAN filtering achieves an MAE of 0.617 m at 70% point loss versus 0.749 m for a simple median baseline, and consistently outperforms it until point density falls below approximately 150 points per bounding box, identified experimentally as the operational threshold of the system and directly usable as a functional specification for adaptive method switching in real deployments.

ABSTRACT. Problematic Internet Use (PIU) among adolescents represents a growing public health concern, yet current diagnostic methods rely predominantly on subjective self-report question- naires. This paper studies four-class ordinal PIU severity predic- tion on the Child Mind Institute Healthy Brain Network dataset (n = 3,960; ages 5–22) as a machine learning problem with noisy labels, structured input missingness, and extreme class imbalance. We design and evaluate three uncertainty-aware components: (1) Reliability-Calibrated Label Distribution Learning (RC- LDL), which derives soft label distributions analytically from the published test-retest reliability of the PCIAT instrument and trains against them through a masked hybrid loss implemented as a custom gradient-boosting objective; (2) reliability-weighted expert fusion gated on per-subject data quality; and (3) selective prediction via margin-based abstention. A central finding is that the QWK ≈ 0.55 reported in prior literature is attributable to label leakage from PCIAT sub-items: once leakage is removed, the leakage-free baseline achieves QWK = 0.389 ± 0.057, and a leakage dose-response analysis shows that a single PCIAT sub-item nearly doubles QWK. While the full framework does not improve aggregate QWK over this baseline, component- level analysis locates where each mechanism acts: RC-LDL is the only condition recovering any severe-class signal (class- 3 F1 = 0.083 vs. 0.000) and reliably improves severe-class probability calibration (RPS = 0.245 vs. 0.311, non-overlapping 95% CIs), an advantage no post-hoc recalibration of the baseline reproduces. These findings establish a reproducible, leakage- free benchmark and identify class imbalance and actigraphy missingness as the primary obstacles to clinical deployment.

ABSTRACT. Abstract—News-augmented forecasting systems typically feed a raw sentiment polarity score into a predictive model, implicitly treating every score as equally trustworthy. Yet a news signal can be internally inconsistent, when a headline and its body disagree, or built from very few articles, and unfiltered sentiment often adds noise rather than signal. This paper proposes and evaluates a set of sentiment-quality features that model the reliability of the signal rather than only its polarity. Two families are introduced: narrative-consistency features that quantify the disagreement between the FinBERT score of an article’s headline and that of its summary, and coverage-density shrinkage, which applies Bayesian shrinkage to the daily sentiment estimate, pulling it toward a ticker-specific prior when few articles are available. The features are fused with eleven technical indicators in an LSTM classifier and evaluated through a progressive ablation with an identical backbone across all conditions, on a cross- sectional relative-volatility task under five-fold walk-forward cross-validation over a 13-ticker, five-sector, eight-year panel (10,895 out-of-sample windows). The full method reaches 60.7% pooled accuracy at a one-week horizon (+5.3 pp over a standard sentiment baseline, p = 7 × 10^{−21}) and 67.4% at one month (+9.3 pp, p = 3×10^{−58}). Two pre-registered subgroup hypotheses are confirmed: the gain is largest on high-divergence and low- coverage days, exactly where the features were designed to help. As a negative result, binary price-direction prediction stays near chance for every condition and horizon, consistent with the efficient-market hypothesis at short horizons.

ABSTRACT. Although comparative studies of Roman settlements across the Empire have highlighted their diversity in terms of layout structure, spatial organization, and orientation, they have also identified common patterns. This exploratory study investigates the retrieval of Roman settlements using Content-Based Image Retrieval (CBIR) based on image similarity and the integration of image and orientation data across Google Earth imagery, archaeological plans, and masks. Preliminary results show that the Canny-HOG approach retrieved settlements sharing similar layouts and/or orientations across different regions of the Roman Empire. The incorporation of orientation data improved retrieval rankings and mean similarity, while reducing the retrieval frequency of settlements with different walled structures and/or orientation characteristics.

ABSTRACT. As urbanization and industrial activity intensify, the monitoring of air quality has become increasingly important in both environmental and operational domains. Employing machine learning methods for anomaly detection in air quality data is crucial for many applications, as traditional fixed-threshold approaches lack robustness. While recent approaches show good results, they often rely solely on deep learning models, which may be prone to overfitting, leading to performance degradation. In this paper we present an air quality anomaly detection methods that combines a 1D CNN - GRU model with a shallow technique that detects major changes in short-term intervals of time-series data. Experimental results showed that the introduced hybrid approach achieved recall scores higher by an average of 0.07 compared to each method's component when used separately.

ABSTRACT. Sandwich attacks on decentralized exchanges (DEXs) exploit public transaction ordering to extract value from ordinary traders, yet automated detection remains difficult due to severely incomplete ground-truth labels and continuously evolving attack strategies. We construct a full-year 2023 dataset of 1.93 million Uniswap V3 USDC/ETH swaps, enriched with exact intra-block ordering via the Alchemy eth_getBlockReceipts API. Attack labels are assembled from two independent sources: Flashbots-verified traces and an on-chain heuristic detector based on Zhou et al., yielding 16,263 union labels at a 0.84% anomaly rate. We apply TranAD, a dual-decoder Transformer trained exclusively on normal transaction windows, evaluated under strict chronological splitting to prevent temporal leakage. Across three random seeds, TranAD achieves mean AUC-ROC of 0.8865 ± 0.0152 and AUC-PR of 0.2220 ± 0.0459, with a coefficient of variation of 1.7% confirming stable performance across initializations. Per-feature reconstruction analysis identifies price impact ratio and tick jump as the strongest anomaly signals, consistent with known Automated Market Maker (AMM) sandwich mechanics. These findings demonstrate that one-class reconstruction models can detect sandwich attack signatures without labeled attack data during training, offering a detection pathway applicable to novel or private-channel attacks that forensic label sources cannot capture.

ABSTRACT. The first part of the talk is an overview of the theory of recognisability for words, ground terms and graphs. A set S is recognisable if its membership problem “does x belong to S?” can be answered using an amount of memory that does not depend on x. For words and ground terms, recognisability is equivalent to the existence of an automaton that traverses the input structure in a predefined order, while labelling its constituent substructures with finitely many states. For graphs, there is no universally-accepted notion of automata, mainly because graphs do not have canonical traversal orders, in general. In this case, one defines recognisability using homomorphisms into finite algebras.

A definition of recognisability is considered to be “robust” if it has a logical characterisation. For words and ground terms, recognisability coincides with definability in Monadic Second Order (MSO) logic. For graphs, in general, there is no known equivalence between recognisability and logical definability. However, for graphs of bounded tree-width, recognisability coincides with definability in MSO extended with modulo constraints on the cardinality of sets, a fragment called Counting MSO (CMSO).

The second part of the talk presents new results, for graphs of tree-width at most k, where k=2 (and perhaps also k=3, if science will advance more by September). We introduce regular grammars and regular expressions that provide compact syntactic representations of (all) recognisable sets of graphs of tree-width at most k. We show that these representations can be converted into recogniser algebras of singly-exponential size, which provides EXPTIME-algorithms for the problems of emptiness, intersection and inclusion between sets of graphs represented in these ways. The effectiveness of these algorithms has been tested on a prototype implementation, with encouraging results. We conclude with a number of open problems, both theoretical and practical.

ABSTRACT. Modern endpoint malware detection is distributed: a lightweight agent on each endpoint collects features from a scanned file or process, sends them to a remote server for analysis, and then enforces the returned verdict locally by blocking, quarantining, or disinfecting. Because the endpoint acts on the verdict, the distributed machinery surrounding detection must never turn a transient server failure into a wrong action. We present a formal model, in Promela, of the endpoint decision pipeline of such a system, abstracted from a production architecture at Bitdefender. The model captures the system's graceful-degradation fallback chain: when the primary analysis server times out, the endpoint falls back to an older legacy-protocol server, and failing that to a reduced-signature local scan, before enforcing a verdict. Assuming detection signatures are sound, we specify six safety and liveness properties in linear temporal logic (LTL) and verify them exhaustively with the SPIN model checker. We prove that the fallback machinery never causes a false positive (an enforcement action against a benign file), commits to exactly one verdict per scan even when timed-out responses arrive late, weakens detection strength only in an explicit and ordered way, and always terminates in an enforcement decision, so the pipeline is deadlock-free. Each property is checked to hold non-vacuously, and we report how the state space grows with concurrent scans and endpoints. The work shows how model checking can give strong correctness guarantees for the failure-handling logic of a production security system, a layer that has received little direct formal attention.

ABSTRACT. Structural analysis is a core method in Petri Net (PN) research, complementing state-space techniques while avoiding many of their drawbacks. It is well studied for classical PNs but far less so for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, enabling symbolic reachability graphs (and lumped Markov chains in stochastic SN) as well as symbolic discrete-event simulation. Over the past two decades, SN-specific structural techniques have been developed, notably in the SNexpression tool. This tool implements a formal calculus for computing symbolic structural relations such as conflict and causality. We propose to use this calculus to semi-automatically verify symbolic structural invariants, which is currently possible only for certain restricted SN subclasses. We focus on (semi)flows and outline how, at least in theory, a flow-generating family can be constructed. We also sketch a framework for formally verifying a broader class of invariant properties. This relies on an extended SN formalism (ESN) that is closed under fundamental functional operators. Representative examples illustrate the main concepts