This paper was published at the 40th IEEE/ACM International Conference on Automated Software Engineering (ASE 2025), one of the leading and most selective venues in software engineering, particularly for research on automated analysis, formal methods, and verification. ASE is widely recognized for shaping both theoretical advances and practical tooling in the field. In 2025, the conference received 1,190 submissions, all of which underwent a rigorous multi-stage peer-review process involving detailed reviews, author responses, and in-depth discussions. At the end of this process, 113 papers were directly accepted, while 140 additional papers were invited for major revision. This paper was among those directly accepted.

The paper makes a foundational contribution to automated software verification by addressing a long-standing gap in the standardization of non-termination witnesses. While verification witnesses are central to certifying algorithms and have been widely adopted for safety properties, the absence of a precise and well-defined format for certifying non-termination had limited interoperability between tools and undermined the reliability of validation. This work closes that gap by introducing a principled extension of the widely adopted witness format 2.0, providing clear syntax and semantics for non-termination witnesses directly over real programs. In addition to the format design, the paper demonstrates the practicality of the approach by implementing witness generation and validation in several state-of-the-art verification and validation tools that rely on different underlying techniques. A comprehensive experimental evaluation on the SV-COMP 2025 termination benchmarks shows that the proposed witnesses are both effective and efficient, enabling independent validation and often significantly faster confirmation than full verification.

The added value of this work lies in its combination of conceptual clarity, practical relevance, and immediate community adoption. The extended witness format improves the informativeness and trustworthiness of non-termination arguments, even in minimal witnesses, and enables meaningful exchange of results between independently developed tools. Beyond the paper itself, the work has already had concrete impact through its integration into witness format version 2.1, contributions to shared documentation and tooling infrastructure, and its role in enabling certified non-termination results in future editions of SV-COMP. By strengthening the foundations of certifying non-termination, this paper advances the broader goal of reproducible, interoperable, and trustworthy automated software verification.

This paper was published as a competition contribution in the SV-COMP track of TACAS 2025 (Tools and Algorithms for the Construction and Analysis of Systems). TACAS is one of the premier international conferences in formal methods, verification, and automated reasoning, and the SV-COMP (Software Verification Competition) track plays a central role in benchmarking, standardizing, and advancing software verification tools. SV-COMP is widely regarded as a driving force in the field: it shapes research directions, encourages reproducibility, promotes fair tool comparison, and provides a large-scale shared benchmark infrastructure used by both academia and industry. Acceptance into the TACAS proceedings indicates strong technical quality and relevance; while exact acceptance rates vary by year, TACAS is generally highly selective, typically accepting only a fraction of submitted papers.

The paper presents a comprehensive reproduction study of SV-COMP 2025, evaluating the reliability, portability, and robustness of the competition’s results and infrastructure. We reproduced verification and validation results for 33 verifiers and 33 validators, executing hundreds of thousands of benchmark tasks on an independent HPC environment. The study confirms that the core competition infrastructure is sound, but also uncovers systemic reproducibility and reusability issues in multiple participating tools.

Beyond identifying problems, the paper proposes concrete, actionable recommendations to improve SV-COMP’s long-term sustainability, such as enforcing package declarations, formalizing allowed file modifications, tightening artifact retention rules, and requiring tools to run outside SV-COMP’s execution environment. These contributions matter because SV-COMP’s credibility depends on reproducibility: if competition results cannot be independently reproduced, trust in rankings, research claims, and downstream scientific comparisons is weakened. The work strengthens the foundations on which future verification research and benchmarking depend.

This work stands out as one of the most thorough independent reproducibility studies of SV-COMP to date. It provides public artifacts, datasets, ranking analyses, and performance statistics, supporting open science.

The paper has immediate practical impact on competition organizers, tool developers, and benchmarking researchers. Its findings directly inform policy improvements for SV-COMP, help tool authors make their systems more portable and reusable, and support broader adoption of SV-COMP’s infrastructure for research benchmarking beyond the competition. The published Zenodo artifact and result tables create a durable resource for follow-up work and long-term evaluation .

Overall, the paper strengthens scientific rigor, transparency, and trust in one of the most influential benchmarking efforts in software verification, amplifying its impact across the formal methods community.

Our vision paper, titled Unified Timing-Aware Program Verification, was accepted for the 29th International Conference on Fundamental Approaches to Software Engineering (FASE 2026). FASE is an established series of international conferences with more than 30 years of tradition. The acceptance rate for this year was 31%. FASE is focused primarily on formal models and methods, often involving reasoning about code, design, and the associated processes.

In our paper, we present a vision for unified timing-aware program verification to formalize and verify properties concerning both the functional behavior and scheduling. We propose a C language extension incorporating first-class clock variables and timing constraints, present a verification workflow, and identify key research directions and challenges.

Our approach enables verification of properties currently inexpressible in existing program verifiers, including safety properties ensured by timing constraints, such as races eliminated by execution time separation; real-time properties including deadline satisfaction and schedulability; and timing-dependent security properties, such as timing side channels. For the first time, these properties can be verified directly on C programs while preserving full language semantics.

This vision paper draws a connection between multiple distinct areas in new ways, including worst-case execution analysis, counterexample-guided abstraction refinement, timed automata, and multi-threaded C programs. It was received well by the research community, and the identified challenges provide many clear directions for further research.

This paper was published in the BPM Forum track of the 23rd International Conference on Business Process Management (BPM 2025), held in Seville, Spain. BPM is recognized as the premier international forum for researchers and practitioners in business process management, running continuously since 2003. The conference maintains a rigorous peer-review process with an average acceptance rate of approximately 20%, making it a highly selective venue that attracts top-tier contributions from computer science, information systems engineering, and management disciplines (OpenResearch). The proceedings are published in Springer's Lecture Notes in Business Information Processing (LNBIP, volume 564) series, which is indexed across major academic databases. This paper introduces the concept of collaboration self-orchestration for BPMN business processes, presenting a novel peer-to-peer protocol model that enables cross-organizational collaborations without centralized workflow engines or smart contract-based orchestration. The key contributions include the introduction of Verifiable Process History Credentials (VphCs) and Non-Invoked Transition Credentials (NiTCs) as mechanisms to maintain cryptographically verifiable process state and prevent malicious process bifurcation—analogous to the double-spending problem in cryptocurrencies. The participants issue, verify, and revoke these credentials during the collaboration, passing them to each other in a peer-to-peer manner. The proposed protocol leverages the qualities found in emerging Self-Sovereign Identity ecosystems, specifically Verifiable Credentials and blockchain backed, cryptographic accumulator based revocation registries, to potentially provide trust guarantees while maintaining minimal on-chain footprint and strong privacy properties. This work stands out by proposing an entirely new usage modality for Verifiable Credentials: expanding from simple challenge-response claim verification scenarios to complex, structured process execution traces and evidences of protocol compliance. Unlike existing smart contract-based approaches that expose process state on-chain or require per-collaboration contract deployments, our model maintains constant-sized on-chain state through cryptographic accumulators while preserving process confidentiality from external parties. The approach bridges two rapidly evolving technological domains—business process management and self-sovereign identity—opening new research areas at their intersection. The protocol provides practical applicability through compatibility with SSI frameworks such as Hyperledger Indy, AnonCreds, and DIDComm, hopefully lowering the barriers to implementation. As the European Digital Identity Wallet initiative accelerates VC adoption across the continent, this research positions decentralized business process orchestration as a compelling application domain for these emerging trust infrastructures.

The paper is published at ESANN, a well-established European conference with a strong focus on neural networks, machine learning, and computational intelligence. ESANN regularly features work on graph learning and ensemble-based approaches, which makes it a natural fit for research on scalable and explainable methods for structured data.

The work introduces GraphTreeBoost, a gradient-boosted ensemble of soft decision trees designed for graph-structured data. It combines spectral graph filtering, via Chebyshev and heat-kernel expansions, with soft decision trees, enabling graph-aware learning without relying on eigendecomposition. All spectral aggregation is instead performed directly in feature space using sparse graph operations. Training relies on analytic second-order leaf updates together with AdamW optimization for both routing and filter parameters. At the same time, the model remains interpretable through explicit thresholds, routing probabilities, and per-node gain scores, and it extends naturally to edge-level learning through normalized 1-Hodge Laplacian operators.

Overall, the approach unifies interpretability, graph structure, and scalability within a single framework. It provides a transparent alternative to graph neural networks, especially in settings with heterophilous or noisy graphs. Empirically, it consistently outperforms feature-only baselines and achieves performance competitive with GCNs on several benchmarks. The method scales linearly with the number of edges and runs efficiently on CPU hardware, making it both practical and theoretically appealing. More broadly, it opens a new line of work on interpretable, tree-based models for graph learning.

Impact Statement Venue & Significance: The paper “Automated and Complete Generation of Traffic Scenarios at Road Junctions Using a Multi-level Danger Definition” is published in Software and Systems Modeling (SoSyM). SoSyM is a leading journal in software and systems engineering, particularly known for publishing high-quality work on modeling foundations, formal methods, and model-based techniques for complex and safety-critical systems. It is a natural venue for research that combines formal definitions with practical validation challenges in domains such as autonomous and cyber-physical systems. SoSyM is widely regarded as a selective Q1 journal with a rigorous multi-round review process, an acceptance rate of approximately 20-30%, and an impact factor of around 3.2.

Summary of Contributions: This paper addresses a central challenge in the certification of autonomous driving systems (ADSs): the need to systematically test ADS behavior across a comprehensive set of potentially dangerous traffic scenarios. Existing scenario generation approaches typically rely on search-based optimization techniques to find scenarios with a high likelihood of unsafe interactions, but they often lack guarantees regarding completeness and coverage. Focusing on road junctions, the paper hypothesizes that danger primarily arises from overlapping paths of traffic participants executing their intended high-level maneuvers. Based on this insight, the paper proposes a method to derive a complete set of potentially dangerous logical scenarios for a given junction. These scenarios are defined as all permutations of overlapping abstract maneuvers assigned to the ADS and surrounding actors. Building on this logical level, the approach then systematically derives concrete-level exact paths that actors must follow, enabling targeted simulation-based testing of collision-prone situations. The paper provides formal definitions of traffic scenarios, danger conditions at multiple abstraction levels, and completeness, forming the basis of a principled, automated generation process. The theoretical foundations of the approach and the theoretical groundwork for the solver algorithm were developed by Oszkár Semeráth, who also contributed through consultations. Attila Ficsor contributed to the experimental evaluation by providing a subset of the measurements and performing data analysis. Dániel Varró also contributed to the theoretical background and through consultations. The remaining modeling, formalization, implementation, and integration work was carried out primarily by Aren A. Babikian.

Added Value & Impact: The key contribution of this work is the combination of formal completeness guarantees with practical, simulation-ready scenario generation. The approach is evaluated through experiments on two realistic road junctions with increasing numbers of external actors and compared against the state-of-the-art Scenic scenario generation. The results show that the proposed approach outperforms Scenic in both scenario coverage and runtime, while also revealing systematic variations in unsafe ADS behavior depending on abstract scenario properties. By explicitly connecting abstract maneuvers, concrete trajectories, and observed safety outcomes, the paper offers valuable insights for ADS validation and certification. Given the growing regulatory and industrial emphasis on scenario-based testing, this work provides a strong foundation for future research and practical adoption in safety assurance workflows.

Venue & Significance This paper, “On the Gap Between Technical Execution and Legal Compliance in Blockchain-Based Business Processes: A Review,” was submitted to BLOCKCHAIN’25: 7th International Congress on Blockchain and Applications, hosted by the University of Lille, France on 25th-27th June, 2025. BLOCKCHAIN’25 forum brings together researchers and practitioners working on blockchain and distributed ledger technologies (DLT) and their applications across various domains. The congress explicitly promotes interdisciplinary research combining blockchain with other disruptive technologies addressing governance, privacy, security, and regulatory challenges. The conference’s publication model-Springer proceedings indexed in major scholarly databases-positions it as a recognized venue for disseminating peer-reviewed, methodologically sound research with both academic and applied relevance. In particular, the workshop BL-LEGAL - Interleaving Legal and Technology Aspects - Regulation Blocks was a perfect fit for our research interests at the time, which focused on bridging technical innovation and regulatory or legal considerations.

Summary of Contributions The paper provides a systematic review of blockchain-based execution of business processes modeled using BPMN, with a specific focus on processes that include financial transactions or a payment step. Our central contribution is the identification and structured analysis of a critical gap in literature: while decentralized orchestration via smart contracts has matured technically, issues of legal enforceability and regulatory compliance remain largely unaddressed. In the paper, we used a two-layer evaluation framework. First, we analyze the technical dimensions of prior work, including application domains, blockchain execution platforms, and the nature of financial intent (e.g., simple payments, escrow mechanisms, or fully automated smart-contract payments). Second, we evaluate the same corpus from a legal and regulatory perspective, assessing whether studies explicitly address compliance requirements (e.g., GDPR, KYC/AML), provide auditability mechanisms, and treat process execution as legally binding agreements. The results demonstrate that only a small fraction of existing literature meaningfully address legal semantics, despite operating in domains where regulatory obligations and contractual accountability are fundamental.

Added Value & Impact We offer a comprehensive review of what is missing from current research literature and why this gap limits real-world adoption. We portray blockchain-based business process automation as not merely a technical challenge, but a socio-technical and regulatory problem too, providing a roadmap for future research on compliance-aware smart contracts, audit-ready decentralized workflows, and legally meaningful process execution. We argue that BPMN’s extensibility (introducing dedicated syntax and semantics) can be leveraged systematically to encode rights, obligations, governance structures, and regulatory constraints directly into process models and execution semantics. For practitioners and policymakers, the paper clarifies why explicit treatment of legal enforceability and regulatory conformance is important for successful adoption of blockchain-based automation, particularly in light of evolving frameworks such as MiCA, DORA, and the DLT Pilot Regime.

1. Venue & Significance

- Where was the paper published? The paper “Theta as a Horn Solver” was submitted to HCVS 2025 (Horn Clauses for Verification and Synthesis).

- Why is this venue important in your field? HCVS is a well-established international workshop that brings together researchers working on Horn clauses as a unifying formalism for verification and synthesis. It is closely aligned with major community efforts such as CHC-COMP and serves as a key forum for discussing CHC solver architectures, algorithmic advances, and practical experiences with Horn-based verification. The workshop attracts both tool developers and theoreticians.

- Acceptance rate (if known): The acceptance rate for HCVS is not publicly disclosed. The workshop follows a selective single-blind peer-review process.

2. Summary of Contributions

- Key contributions of the paper:

A systematic description of the algorithms, design choices, and trade-offs involved in the CHC-to-CFA transformation-based approach of Theta, which had previously not been documented in the CHC context. An empirical analysis of Theta’s behavior on CHC-COMP benchmarks, identifying strengths, limitations, and sensitivity to configuration choices. A re-evaluation of CHC-COMP 2025 benchmarks under corrected tool settings, providing a more accurate picture of Theta’s actual capabilities as a Horn solver. A description of how Theta is capable of producing models for the CHC problems it solves.

- What problem does it solve, and why does it matter? The paper addresses the lack of understanding of how general-purpose software model checkers perform when applied to Horn clauses. While many CHC solvers are designed specifically for Horn reasoning, Theta originates from software verification.

- Contribution of department members: The work was carried out by the department’s authors, including the design, implementation, experimental evaluation, and analysis of the transformation-based approach and benchmark results.

3. Added Value & Impact

- What makes this work stand out?

It demonstrates that mature software model checkers can be effectively repurposed for other verification domains—in this case, Horn clauses—through well-defined transformations, rather than by building domain-specific solvers from scratch. The paper provides transparency into solver internals and configuration effects, which is particularly valuable in a competition-driven setting like CHC-COMP. The area that shows the advantages of a software verification based approach most clearly is __model generation__. Outputting correctness- and violation-witnesses has been a requirement towards model checkers competing in SV-COMP for years now, meaning the format of these witnesses and the tools' support for them is well established. On the other hand, most CHC solvers are not yet capable of producing models (analogous to correctness witnesses) for the CHC problems they solve. 2025 is the first year that CHC-COMP introduced the model generation track. We were able to utilize Theta's witness-generation algorithms to produce CHC models and thus compete in this track, even winning 2 of the categories: https://chc-comp.github.io/2025/CHC-COMP%202025%20Extended%20Report%20-%20HCVS.pdf

- Potential or observed impact:

The paper helps position Theta as a reusable verification backend beyond software model checking, encouraging similar cross-domain reuse of established tools. The CHC-COMP results demonstrate that Theta can be competitive as a Horn-solver, as we were able to rank top 3 in multiple verification categories as well as in the new model generation category. The paper also provides practical insights for CHC solver developers and competition organizers.

(1) Venue & Significance

Our paper entitled ‘Towards Faulty Claim Impact Analysis & Mitigation in Verifiable-Credential-Driven Collaborations’ was presented at the 15th International Conference on Logistics, Informatics and Service Sciences (LISS2025). While this conference focuses on logistics and service sciences and is thus relatively far from our primary research tracks, our work has notable applications in the logistics domain (especially supply chains); in addition, the 2025 conference was organized in Budapest.

(2) Summary of Contributions

Verifiable credentials (VCs) represent cryptographically signed statements made by trusted entities in a decentralized manner and following the philosophy of self-sovereign identity (SSI). These credentials are increasingly widely adopted in several domains. While standalone VCs provide value on their own, their true potential is realized when several VCs are combined into chains and form what we refer to as ‘credential systems.

VCs provide assurance about the authenticity of their issuers and the integrity of their contents. However, they do not inherently ensure the truthfulness of the included claims themselves; issuers may make false claims due to software faults, human error, or for malicious reasons. In credential systems, where interdependent VCs are used, the erroneous claims within one credential can directly or transitively affect other credentials and lead to undesired system-level effects.

The main contribution of this work is a first (to our knowledge) mapping of dependability concepts (faults, errors, failures, error propagation, mitigation techniques, etc) to credential systems (systems of interdependent verifiable credentials). We put a special focus on error propagation analysis (EPA) in credential systems. In addition, the proposed theoretical defences and mitigations are described in the context of a running example in the logistics domain.

(3) Added Value & Impact

To the best of our knowledge, there is no prior art in either analyzing interdependent verifiable credential systems from a dependability perspective, or in designing or adapting dependability mechanisms (for as fault prevention, tolerance, removal, and forecasting) and techniques (such as error propagation analysis) to the verifiable credential context.

In our paper, we laid down the foundations of future dependability research for VCs. Following up on the conference in the summer of 2025, a BSc student (Malek Alqassasfeh) has implemented a prototype system based on our ideas in the Autumn of 2025 as his thesis work.

Venue & Significance This research was first presented at the European Symposium on Artificial Neural Networks, Computational Intelligence, and Machine Learning (ESANN 2025) and subsequently expanded for the Applied Network Science journal (Springer). ESANN is a long-standing, prestigious venue (CORE B) known for advancements in machine learning models. Applied Network Science (Q1) is a leading open-access journal dedicated to the study of complex networks. This venue is particularly significant for this work as it appeared in the special collection "Bridging Network Science and AI," underscoring the research's relevance at the intersection of geometric deep learning and biological network analysis.

Summary of Contributions This work addresses a fundamental misalignment in computational biology: the use of flat, Euclidean vector spaces to model biological systems that are intrinsically hierarchical and scale-free. Personal contributions include: • Geometric Characterization: I performed a geometric analysis of multi-layer tissue-specific Protein-Protein Interaction (PPI) networks, revealing that the degree distributions of each PPI network are heavy-tailed, highly correlated across tissues, and that layer-to-layer correlation is inversely proportional to the distance between layers in the tissue hierarchy. These topological properties provide empirical evidence that the tissue-specific protein interaction space has an underlying hyperbolic geometry and can be effectively modeled within a shared embedding space. • Methodological Innovation: I proposed a hyperbolic extension to the unsupervised, multi-layer graph embedding method, OhmNet, by developing a non-Euclidean version of Node2Vec and formulating hierarchy regularization in hyperbolic space. • Empirical evaluation: I compared the proposed hyperbolic model to its Euclidean counterpart across various downstream tasks. Results demonstrate that embeddings leveraging a geometric inductive bias align better with the scale-free structure of the multi-layer network, yielding lower PPI graph distortion and superior accuracy in tissue-specific protein function prediction, while also facilitating interpretable visualizations of the latent space.

Added Value & Impact This work stands out as the first geometry-aware network embedding solution specifically designed for multi-layer PPI networks. By successfully integrating hyperbolic geometry into a hierarchical multi-layer framework, it solves the problem of "geometric mismatch" that limits traditional models. Scientific Impact: The reduction in graph distortion enables a more accurate representation of the human protein interactome, leading to a deeper understanding of biological processes by predicting novel interactions and inferring biological functions with greater accuracy. Broader Implications: In addition to proposing a specific solution, by assessing the geometry of the tissue-specific protein interaction space, this work motivates future research to incorporate hyperbolic geometry into multi-layer PPI graph embedding models. Guidelines: The study provides a publicly available open-source implementation, serving as a methodological guideline for constructing geometry-aware models in systems biology.

Abstract

Accurate system identification requires excitation signals that deliver sufficient broadband energy while maintaining controlled peak levels at the input. In this context, minimizing the crest factor (CR) of multisine signals is essential to improve frequency response function (FRF) estimation accuracy. This work proposes an optimized gradient-based algorithm that integrates the Newton–Raphson method with the Levenberg–Marquardt (LM) scheme, where closed-form gradient and Hessian expressions are derived to ensure stability and efficient convergence. A systematic procedure for selecting the LM damping coefficient is introduced, where multiple candidate values are tested during the initial iterations and the best one is retained, ensuring stable convergence and consistent performance across different multisine scenarios. The method is validated on five multisine configurations with varying harmonic counts, amplitude distributions, and frequency spacings, each repeated over 1000 realizations. Compared with Guillaume’s method, the proposed approach achieved consistent improvements, reducing the minimum CR from 1.3700 to 1.3502 (31 harmonics) and from 1.3512 to 1.3481 (100 harmonics), representing the lowest reported values in the literature. Across all cases, the improvement rate exceeded 70% of realizations, reaching 91.7% for exponential–flat spectra. Although the computation time increased by 1.2– 3.5× , the method consistently delivered superior minimum and average CR values. These results establish new benchmark values for multisine excitation design, confirming the method’s effectiveness for accurate and efficient system identification.

The paper has been published and presented at the 31st International Symposium on Model Checking Software (SPIN 2025) which is a well-established workshop in the field of software model checking. Having a clear focus on this narrow segment of formal methods, it brings together the best researchers who work on very similar problems. Even though, it is a workshop, it follows a strict peer-review process as usual in the larger conferences of the field.

The main contribution of the paper is the simplification of the state space exploration by identifying irrelevant program statements. While similar techniques that remove redundant parts of the model have long been in existence, the key differentiating characteristic of our contribution is the application of the idea for concurrent software models. The different possible thread interleavings make it difficult to detect redundant program statements. We propose a thread context-sensitive data flow analysis to have a fine-grained algorithm for determining if evaluating a program statement during the state space exploration is important or not. We also provide the integration of our proposed algorithm to existing model checking techniques to improve their scalability. Applying formal verification and model checking in real world projects is often hindered by scalability issues. Therefore, improving the performance and scalability of model checking algorithms is crucial for their adoption in industrial applications.

The algorithms presented in the paper have been implemented in the open source verification framework Theta. The framework mainly serves research purposes but it is also used in projects with industrial partners. The tool also participates in the international competition on software verification (SV-COMP) where the algorithms presented in the paper contribute to the performance of the tool.

This paper was presented at Bioimaging 2026, a well-established international conference focusing on biomedical image analysis, computer-assisted diagnosis, and translational imaging technologies. Bioimaging is an important venue in the medical imaging community because it brings together researchers from machine learning, medical physics, and clinical domains, emphasizing methods that are both technically sound and clinically relevant. The conference is selective and competitive, with a rigorous peer-review process that prioritizes methodological novelty, validation on real-world data, and potential clinical impact, making acceptance a strong indicator of research quality and relevance. The core contribution of this work is a hybrid lung segmentation framework that combines the representational power of Convolutional Neural Networks (CNNs) with the strong prior knowledge encoded in Active Shape Models (ASMs). Lung segmentation in posterior–anterior (PA) chest X-ray images is a critical preprocessing step for many computer-aided detection and diagnosis (CADe/CADx) pipelines, including pulmonary nodule detection, lesion analysis, and disease screening. While CNN-based approaches achieve high accuracy on benchmark datasets, they often suffer from poor robustness, non-local segmentation errors, and limited generalization when exposed to distribution shifts—an important limitation given the scarcity and variability of annotated medical imaging data. To address this problem, the proposed method introduces an iterative contour refinement strategy, where CNN predictions are regularized by a statistical shape model of the lungs. By integrating learned appearance cues with anatomically plausible shape constraints, the method mitigates common failure modes of purely data-driven approaches. Experimental results demonstrate that the hybrid CNN–ASM framework produces robust and anatomically consistent lung segmentations, even in challenging cases where standalone neural networks fail to generalize. This directly improves the reliability of downstream CADe/CADx systems and reduces the risk of error propagation in clinical decision-support pipelines. What makes this work stand out is its principled integration of deep learning and classical model-based techniques, showing that shape priors remain highly relevant in modern medical imaging workflows. Rather than replacing CNNs, the approach augments them with interpretable constraints, improving robustness without requiring large additional datasets. This is particularly valuable in low-resource or heterogeneous clinical settings, where training data is limited or imaging protocols vary. The impact of this research lies in its potential for broader adoption in clinical imaging pipelines, especially for large-scale screening applications where chest X-rays remain the most accessible modality worldwide. The method provides a blueprint for hybrid segmentation systems that balance accuracy, robustness, and interpretability. The work has also opened avenues for follow-up research on hybrid models for other anatomical structures, reinforcing its relevance beyond lung segmentation and contributing to the ongoing discourse on trustworthy and generalizable AI in medical imaging.

This paper, published at the IEEE International Conference on Industrial Cyber-Physical Systems (ICPS), delivers advance in model-based systems engineering (MBSE) for critical CPS by addressing the fragmentation caused by diverse high‑level languages. Its core contribution is a configurable V&V framework that unifies static (validation) and dynamic (verification) analysis through semantic libraries that encode language structure, constraints, and semantics. By shifting the burden from hand‑crafted transformation chains to reusable semantic libraries, the framework makes it feasible to support new DSLs with a modeling task rather than a full toolchain rewrite, while ensuring that results can be mapped back to the original models to support practitioner workflows. This approach directly tackles the long‑standing abstraction and interoperability gaps in MBSE, enabling stakeholders to reason about a broad family of languages with consistent semantics and verifiable properties.

The paper’s significance stems from its potential to increase the reuse and extensibility of V&V tooling in safety‑critical domains where DSL proliferation is common. The framework’s layered architecture - comprising a syntactic mapper, semantic unfolder, constraint validator, and back‑annotator - allows engineers to plug in different model checkers and backends without reimplementing semantics for each language. The feasibility demonstrated via a proof‑of‑concept built with Semantifyr, Viatra, and Theta, and applied to the OpenMBEE Space Mission model, provides concrete evidence that the approach scales beyond theory to operational practice. Open‑source artifacts (including the Gamma semantic library and the Gamma‑OXSTS serializer) are made available through the Semantifyr repository, supporting transparency, replication, and future extensions.

In terms of added value and impact, the work stands out for its emphasis on pluggable semantics as a design primitive, which promises to lower barriers to adoption in industry and academia alike. ICPS, with its strong industry‑academic cross‑pollination and rigorous peer review, provides an appropriate venue signaling both methodological quality and practical relevance. The open‑source nature of the PoC artifacts amplifies potential follow‑on work, from additional case studies (e.g., SysML v2 frontends) to broader integration with MBSE workflows, increasing citations, collaborations, and potential industry uptake in safety‑critical sectors.