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).

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.

Smart contracts manage valuable assets, and their immutability hinders bug fixing. Therefore, pre-deployment verification and validation are critical. In fact, auditing has become mandatory in the pipeline of smart contract development. Auditors usually combine manual inspection with automated tools in their auditing work, looking for issues that may be domain dependent (i.e., pertaining to the correct implementation of requirements-which are often informal, partial, and implicit) or independent (e.g., reentrancy, overflow, etc.), To identify domain dependent issues, it is important to understand the non-trivial behavior of the implementation over sequences of calls made by callees playing different roles in the contract. In this paper, we propose a novel approach that combines predicate abstraction with modal transition systems to build abstractions that can help auditors in the smart contract validation process. The required inputs are a set of predicates provided as code and, optionally, constraints over smart contract function parameters. The output is a modal transition system that captures the contract's behavior. We report on a prototype that builds modal abstractions and an evaluation on two established benchmarks where we identified four previously unreported issues.

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.

Boundary conditions express situations under which requirements specifications conflict. They are used within a broader conflict management process to produce less idealized specifications. Several approaches have been proposed to identify boundary conditions automatically. Some introduce a prioritization criteria to reduce the number of boundary conditions presented to an engineer. However, identifying the few, relevant boundary conditions remains an open challenge. In this paper, we argue that one of the problems of the state of the art is with the definition of boundary condition itselfit is too weak. We propose a stronger definition which we refer to as Unavoidable Boundary Conditions (UBCs), which utilizes the notion of realizability in reactive synthesis. We show experimentally that UBCs non-trivially reduce the number of conditions produced by existing boundary condition identification techniques. We also relate UBCs to existing concepts in reactive synthesis used to provide feedback for unrealizable specifications (including counter-strategies and unrealizable cores). We then show that UBCs provide a targeted form of feedback for repairing unrealizable specifications.

Verification and validation of smart contracts is crucial, as these programs administer valuable assets. Indeed, there is a proliferation of companies, specialized in smart contract audits that has become a key component of the blockchain ecosystem. Current verification and validation practice is heavily reliant on the insight and experience of auditors. However, there is an increasing rich toolbox that supports their work. In this paper, we show how predicate abstraction can be leveraged to construct models that support smart contract auditing. These models provide auditors with a systematic approach to analyzing and validating the behavior of smart contracts at the function call level. By proposing predicates, auditors can generate alternative perspectives on a contract’s behavior, refine transitions to investigate specific scenarios, and incorporate transient states into the abstraction to uncover reentrancy vulnerabilities. We formally define predicate abstractions for smart contracts and introduce default predicates to support initial exploration. We also present PASCo, a tool that automatically builds an abstract finite state automaton from a set of predicates and a smart contract implementation. We evaluate PASCo on established benchmarks and with an experienced smart contract auditor. Furthermore, we compare its effectiveness in detecting reentrancy vulnerabilities (measured in terms of precision and recall) against 14 state-of-the-art Solidity vulnerability detectors.

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 the first adaptive shielding framework - to the best of our knowledge - 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 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.

We introduce a novel verification problem that exploits common code fragments between two programs. We discuss a solution based on Mimicry Monitors that anticipate if the execution of a Program Under Analysis has a counterpart in an Oracle Program without executing the latter. We discuss how such monitors can be leveraged in different software engineering tasks.

Metamorphic testing is a valuable technique that helps in dealing with the oracle problem. It involves testing software against specifications of its intended behavior given in terms of so called metamorphic relations, statements that express properties relating different software elements (e.g., different inputs, methods, etc). The effective application of metamorphic testing strongly depends on identifying suitable domain-specific metamorphic relations, a challenging task, that is typically manually performed. This paper introduces MemoRIA, a novel approach that aims at automatically identifying metamorphic relations. The technique focuses on a particular kind of metamorphic relation, which asserts equivalences between methods and method sequences. MemoRIA works by first generating an object-protocol abstraction of the software being tested, then using fuzzing to produce candidate relations from the abstraction, and finally validating the candidate relations through run-time analysis. A SAT-based analysis is used to eliminate redundant relations, resulting in a concise set of metamorphic relations for the software under test. We evaluate our technique on a benchmark consisting of 22 Java subjects taken from the literature, and compare MemoRIA with the metamorphic relation inference technique SBES. Our results show that by incorporating the object protocol abstraction information, MemoRIA is able to more effectively infer meaningful metamorphic relations, that are also more precise, compared to SBES, measured in terms of mutation analysis. Also, the SAT-based reduction allows us to significantly reduce the number of reported metamorphic relations, while in general having a small impact in the bug finding ability of the corresponding obtained relations.

For systems to respond to scenarios that were unforeseen at design time, they must be capable of safely adapting, at runtime, the assumptions they make about the environment, the goals they are expected to achieve, and the strategy that guarantees the goals are fulfilled if the assumptions hold. Such adaptation often involves the system degrading its functionality, by weakening its environment assumptions and/or the goals it aims to meet, ideally in a graceful manner. However, finding weaker assumptions that account for the unanticipated behaviour and of goals that are achievable in the new environment in a systematic and safe way remains an open challenge. In this paper, we propose a novel framework that supports assumption and, if necessary, goal degradation to allow systems to cope with runtime assumption violations. The framework, which integrates into the MORPH reference architecture, combines symbolic learning and reactive synthesis to compute implementable controllers that may be deployed safely. We describe and implement an algorithm that illustrates the working of this framework. We further demonstrate in our evaluation its effectiveness and applicability to a series of benchmarks from the literature. The results show that the algorithm successfully learns realizable specifications that accommodate previously violating environment behaviour in almost all cases. Exceptions are discussed in the evaluation.

Controller synthesis is in essence a case of model-based planning for non-deterministic environments in which plans (actually "strategies") are meant to preserve system goals indefinitely. In the case of supervisory control environments are specified as the parallel composition of state machines and valid strategies are required to be "non-blocking" (i.e., always enabling the environment to reach certain marked states) in addition to safe (i.e., keep the system within a safe zone). Recently, On-the-fly Directed Controller Synthesis techniques were proposed to avoid the exploration of the entire -and exponentially large-environment space, at the cost of non-maximal permissiveness, to either find a strategy or conclude that there is none. The incremental exploration of the plant is currently guided by a domain-independent human-designed heuristic. In this work, we propose a new method for obtaining heuristics based on Reinforcement Learning (RL). The synthesis algorithm is thus framed as an RL task with an unbounded action space and a modified version of DQN is used. With a simple and general set of features that abstracts both states and actions, we show that it is possible to learn heuristics on small versions of a problem that generalize to the larger instances, effectively doing zero-shot policy transfer. Our agents learn from scratch in a highly partially observable RL task and outperform the existing heuristic overall, in instances unseen during training.

We study directed control of discrete event system expressed as the parallel composition of interacting automata. Solutions that first compose the automata and then compute a controller may result in an exponential blow up. We present a technique that builds the composition on-the-fly guided by a novel domain-independent heuristic, which attempts to discover relevant dependencies between the intervening components. We obtain safe and non-blocking directed controllers, or directors, exploring a reduced portion of the state space. We present the first experimental results on directed control comparing on-the-fly composition with informed search against the original monolithic approach to directed control.

Temporal task planning uses formal techniques such as reactive synthesis to guarantee that a robot will succeed in its mission. This technique requires certain explicit and implicit assumptions and simplifications about the operating environment of the robot, including its sensors and capabilities. A robot executing a plan can produce a silent mission failure, where the user may believe that the mission goals were achieved when instead the assumptions were violated at runtime. This entails that mitigation and remediation opportunities are missed. Monitoring at runtime can detect complex assumption violations and identify silent failures, but such monitoring requires the ability to describe and detect sophisticated temporal properties together with quantitative and complex data. Additional challenges include (1) ensuring the correctness of the monitors and a correct interplay between the planning execution and the monitors, and (2) that monitors run under constrained environments in terms of resources. In this paper we propose a solution based on stream runtime verification, which offers a high-level declarative language to describe sophisticated monitors together with guarantees on the execution time and memory usage. We show how monitors can be combined with temporal planning not only to monitor assumptions but also to support mitigation and remediation in UAV missions. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.