Costs for resolving software defects increase exponentially in late stages. Incomplete or ambiguous requirements are one of the biggest sources for defects, since stakeholders might not be able to communicate their needs or fail to share their domain specific knowledge. Combined with insufficient developer experience, teams are prone to constructing incorrect or incomplete features. To prevent this, requirements engineering has to explore knowledge sources beyond stakeholder interviews. Publicly accessible issue trackers for systems within the same application domain hold essential information on identified weaknesses, edge cases, and potential error sources, all documented by actual users. Our research aims at (1) identifying, and (2) leveraging such issues to improve an agile requirements artifact known as a “user story”. We present CrUISE-AC (Crowd and User Informed Suggestion Engine for Acceptance Criteria) as a fully automated method that investigates issues and generates non-trivial additional acceptance criteria for a given user story by employing NLP techniques and an ensemble of LLMs. CrUISE-AC was evaluated by five independent experts in two distinct business domains. Our findings suggest that issue trackers hold valuable information pertinent to requirements engineering. Our evaluation shows that 80–82 % of the generated acceptance criteria add relevant requirements to the user stories. Limitations are the dependence on accessible input issues and the fact that we do not check generated criteria for being conflict-free or non-overlapping with criteria from other user stories.

We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.

There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). In this paper, we present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program.

Abstract Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing in our termination prover AProVE and evaluated it successfully with extensive experiments.