arXiv subjects

Sebastian Uchitel

Publications and source records attributed to Sebastian Uchitel.

9 recordsLinked to original sources

arXiv2026

Agentic Generation and Evolution of Knowledge Models

Complex software systems such as autonomous vehicles, robotics increasingly interact with dynamic physical, cyber, and social environments. Reasoning about their behavior, maintaining them under continuous change, and evolving them safely require trustworthy knowledge about the system, its assumptions, and its operating context. Knowledge models (KMs) provide a practical basis for such reasoning, but they may themselves become incomplete, inconsistent, or outdated as systems evolve. This paper presents TrustModel, a vision for the agentic generation and evolution of living KMs. TrustModel comprises three agentic subsystems: Modeling, for constructing and updating KMs; Conformance, for assessing their alignment with the system and its environment; and Evolution, for generating guidance to keep KMs synchronized with emerging changes. We demonstrate how TrustModel can be instantiated for model-based testing and discuss its potential for supporting other MDE activities, such as requirements and assumption monitoring, architectural drift tracking, and change impact assessment. Overall, TrustModel positions living KMs as a foundation for dependable engineering of continuously evolving software systems.

cs.SE↗

arXiv2026

SE Journals in 2036: Looking Back at the Future We Need to Have

In 2025, SE publishing faces an existential crisis of scalability. As our communities swell globally and integrate fast-moving methodologies like LLMs, traditional peer-review practices are collapsing under the strain. The "bureaucratic anomaly" of monolithic review has become mathematically unsustainable, creating a stochastic "lottery" that punishes novelty and exhausts researchers. This paper, written from the perspective of 2036, documents potential solutions. Here, the editors of ASE, EMSE, IST, JSS, TOSEM and TSE dream a collective dream of a brighter future. In summary first we stopped fighting (The Journal Alliance). Then we fixed the process (The Lottery / Unbundling / Fixing the Benchmark Graveyard). And then we fixed the culture (Cathedrals/Bazaars).

cs.SE↗

arXiv2025

Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning

Shielding is widely used to enforce safety in reinforcement learning (RL), ensuring that an agent's actions remain compliant with formal specifications. Classical shielding approaches, however, are often static, in the sense that they assume fixed logical specifications and hand-crafted abstractions. While these static shields provide safety under nominal assumptions, they fail to adapt when environment assumptions are violated. In this paper, we develop an adaptive shielding framework based on based on Generalized Reactivity of rank 1 (GR(1)) specifications, a tractable and expressive fragment of Linear Temporal Logic (LTL) that captures both safety and liveness properties. Our method detects environment assumption violations at runtime and employs Inductive Logic Programming (ILP) to automatically repair GR(1) specifications online, in a systematic and interpretable way. This ensures that the shield evolves gracefully, ensuring liveness is achievable and minimally weakening goals only when necessary. We consider two case studies: Minepump and Atari Seaquest; showing that (i) static symbolic controllers are often severely suboptimal when optimizing for auxiliary rewards, and (ii) RL agents equipped with our adaptive shield maintain near-optimal reward and perfect logical compliance compared with static shields.

cs.AI↗

arXiv2025

Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control

We present a compositional approach to controller synthesis of discrete event system controllers with linear temporal logic (LTL) goals. We exploit the modular structure of the plant to be controlled, given as a set of labelled transition systems (LTS), to mitigate state explosion that monolithic approaches to synthesis are prone to. Maximally permissive safe controllers are iteratively built for subsets of the plant LTSs by solving weaker control problems. Observational synthesis equivalence is used to reduce the size of the controlled subset of the plant by abstracting away local events. The result of synthesis is also compositional, a set of controllers that when run in parallel ensure the LTL goal. We implement synthesis in the MTSA tool for an expressive subset of LTL, GR(1), and show it computes solutions to that can be up to 1000 times larger than those that the monolithic approach can solve.

cs.SE↗

arXiv2022

Dynamic Slicing by On-demand Re-execution

In this paper, we propose a novel approach that aims to offer an alternative to the prevalent paradigm to dynamic slicing construction. Dynamic slicing requires dynamic data and control dependencies that arise in an execution. During a single execution, memory reference information is recorded and then traversed to extract dependencies. Execute-once approaches and tools are challenged even by executions of moderate size of simple and short programs. We propose to shift practical time complexity from execution size to slice size. In particular, our approach executes the program multiple times while tracking targeted information at each execution. We present a concrete algorithm that follows an on-demand re-execution paradigm that uses a novel concept of frontier dependency to incrementally build a dynamic slice. To focus dependency tracking, the algorithm relies on static analysis. We show results of an evaluation on the SV-COMP benchmark and Antrl4 unit tests that provide evidence that on-demand re-execution can provide performance gains particularly when slice size is small and execution size is large.

cs.SE↗

arXiv2022

Focused Dynamic Slicing for Large Applications using an Abstract Memory-Model

Dynamic slicing techniques compute program dependencies to find all statements that affect the value of a variable at a program point for a specific execution. Despite their many potential uses, applicability is limited by the fact that they typically cannot scale beyond small-sized applications. We believe that at the heart of this limitation is the use of memory references to identify data-dependencies. Particularly, working with memory references hinders distinct treatment of the code-to-be-sliced (e.g., classes the user has an interest in) from the rest of the code (including libraries and frameworks). The ability to perform a coarser-grained analysis for the code that is not under focus may provide performance gains and could become one avenue toward scalability. In this paper, we propose a novel approach that completely replaces memory reference registering and processing with a memory analysis model that works with program symbols (i.e., terms). In fact, this approach enables the alternative of not instrumenting -- thus, not generating any trace -- for code that is not part of the code-to-be-sliced. We report on an implementation of an abstract dynamic slicer for C\#, \textit{DynAbs}, and an evaluation that shows how large and relevant parts of Roslyn and Powershell -- two of the largest and modern C\# applications that can be found in GitHub -- can be sliced for their test cases assertions in at most a few minutes. We also show how reducing the code-to-be-sliced focus can bring important speedups with marginal relative precision loss.

cs.SE↗

arXiv2017

Model Checker Execution Reports

Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe cones, and present the notion of execution reports, which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the execution reports produced and the information that can be extracted.

cs.SE↗

arXiv2017

Verification Coverage

Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success stories. However, widespread adoption remains unlikely in the short term and one of the remaining obstacles in that direction is the vast number of instances which software model checkers cannot fully analyze within reasonable memory and CPU bounds. The majority of verification tools fail to provide a measure of progress or any intermediate verification result when such situations occur. Inspired in the success that coverage metrics have achieved in industry, we propose to adapt the definition of coverage to the context of verification. We discuss some of the challenges in pinning down a definition that resembles the deeply rooted semantics of test coverage. Subsequently we propose a definition for a broad family of verification techniques: those based on Abstract Reachability Trees. Moreover, we discuss a general approach to computing an under-approximation of such metric and a specific heuristic to improve the performance. Finally, we conduct an empirical evaluation to assess the viability of our approach.

cs.SE↗

arXiv2015

MORPH: A Reference Architecture for Configuration and Behaviour Self-Adaptation

An architectural approach to self-adaptive systems involves runtime change of system configuration (i.e., the system's components, their bindings and operational parameters) and behaviour update (i.e., component orchestration). Thus, dynamic reconfiguration and discrete event control theory are at the heart of architectural adaptation. Although controlling configuration and behaviour at runtime has been discussed and applied to architectural adaptation, architectures for self-adaptive systems often compound these two aspects reducing the potential for adaptability. In this paper we propose a reference architecture that allows for coordinated yet transparent and independent adaptation of system configuration and behaviour.

cs.SE↗