Linear Temporal Logic (LTL) can be used for problem-solving when all problem constraints can be specified in this logic through the use of satisfiability checking techniques. In optimization problems such as scheduling with preferences, where constraints are primarily temporal, LTL is a desirable specification formalism. However, LTL cannot be used as a standalone formalism due to the fact that it is unable to specify soft constraints. This article introduces Optimization LTL (OLTL), an optimization-oriented extension of LTL that can specify both hard and soft constraints in optimization problems. The syntax, semantics and basic formal properties of this logic are presented, along with an encoding based on bit-vector logic and Linear Real Arithmetic (LRA). Additionally, a tool called LiTeLLab ( Li near Te mporal L ogic Lab oratory) is introduced to solve optimization problems specified by OLTL. The feasibility and scalability of using OLTL as a specification formalism is demonstrated through two case studies. These problems, with multiple optimization parameters, are specified in OLTL and LiTeLLab successfully generates optimal solutions.

ABSTRACT Introduction Requirements engineering plays a crucial role in the software development lifecycle, encompassing the elicitation, analysis, specification, and validation of requirements. Inefficiencies in any of these processes can lead to delays, budget overruns, and even project failure. This paper explores the integration of requirements reuse and recommender systems to enhance the elicitation process by leveraging historical project data and stakeholder interaction patterns. Methods The proposed methodology incorporates a hybrid approach that combines collaborative filtering and content‐based filtering to recommend relevant requirements to stakeholders. A dynamic weighting framework adjusts the contributions of these two approaches based on the availability of data. In situations with insufficient qualified data, the approach relies more heavily on content‐based filtering to address challenges such as data sparsity and the cold‐start problem. To enhance the semantic similarity between requirements, the method aggregates GloVe word vectors with domain‐specific TF‐IDF scores to identify software engineering‐specific vocabulary. Results Experimental evaluation using a benchmark dataset demonstrates that the proposed hybrid approach significantly improves the prediction accuracy of relevant requirements recommendations, compared to traditional methods. Conclusion The integration of requirements reuse with a recommender system that combines collaborative and content‐based filtering offers an effective solution to streamline the elicitation process, mitigate risks of overlooking critical requirements, and save time during the evaluation and selection of requirements. The proposed method improves the efficiency and accuracy of requirements engineering, especially in contexts with limited data availability.

Many developers rely on Large Language Models (LLMs) to facilitate software development. Nevertheless, these models have exhibited limited capabilities in the security domain. We introduce LLMSecGuard, a framework to offer enhanced code security through the synergy between static code analyzers and LLMs. LLMSecGuard is open source and aims to equip developers with code solutions that are more secure than the code initially generated by LLMs. This framework also has a benchmarking feature, aimed at providing insights into the evolving security attributes of these models.

Static program analysis development is a non-trivial and time-consuming task. We present a framework through which developers can define static program analyses in natural language. We show the application of this framework to identify cryptography misuses in Java programs, and we discuss how it facilitates static program analysis development for developers.

This paper studies how bit-vector logic (bv logic) can help improve the efficiency of verifying specifications expressed in Linear Temporal Logic (LTL). First, it exploits the notion of Bounded Satisfiability Checking to propose an improved encoding of LTL formulae into formulae of bv logic, which can be formally verified by means of Satisfiability Modulo Theories (SMT) solvers. To assess the gain in efficiency, we compare the proposed encoding, implemented in our tool$\mathbb {Z}$ot, against three well-known encodings available in the literature: the classic bounded encoding and the optimized, incremental one, as implemented in both NuSMV and nuXmv, and the encoding optimized for metric temporal logic, which was the “standard” implementation provided by$\mathbb {Z}$ot. We also compared the newly proposed solution against five additional efficient algorithms proposed by nuXmv, which is the state-of-the-art tool for verifying LTL specifications. The experiments show that the new encoding provides significant benefits with respect to existing tools. Since the first set of experiments only used Z3 as SMT solver, we also wanted to assess whether the benefits were induced by the specific solver or were more general. This is why we also embedded different SMT solvers in$\mathbb {Z}$ot. Besides Z3, we also carried out experiments with CVC4, Mathsat, Yices2, and Boolector, and compared the results against the first and second best solutions provided by either NuSMV or nuXmv. Obtained results witness that the benefits of the bv logic encoding are independent of the specific solver. Bv logic-based solutions are better than traditional ones with only a few exceptions. It is also true that there is no particular SMT solver that outperformed the others. Boolector is often the best as for memory usage, while Yices2 and Z3 are often the fastest ones.

Abstract Software developers study and reuse existing source code to understand how to properly use application programming interfaces (APIs). However, manually finding sufficient and adequate code examples for a given API is a difficult and a time‐consuming activity. Existing approaches to find or generate examples assume availability of a reasonable set of client code that uses the API. This assumption does not hold for newly released API libraries, non‐widely used APIs, nor private ones. In this work we reuse the important information that is naturally present in test code to circumvent the lack of usage examples for an API when other sources of client code are not available. We propose an approach for automatically identifying the most representative API uses within each unit test case. We then develop an approach to synthesize API usage examples by extracting relevant statements representing the usage of such APIs. We compare the output of a prototype implementation of our approach to both human‐written examples and to a state‐of‐the‐art approach. The obtained results are encouraging; the examples automatically generated with our approach are superior to the state‐of‐the‐art approach and highly similar to the manually constructed examples.

This article presents a novel technique to formally verify models of real-time systems captured through a set of heterogeneous UML diagrams. The technique is based on the following key elements: (i) a subset of Unified Modeling Language (UML) diagrams, called Coretto UML (C-UML), which allows designers to describe the components of the system and their behavior through several kinds of diagrams (e.g., state machine diagrams, sequence diagrams, activity diagrams, interaction overview diagrams), and stereotypes taken from the UML Profile for Modeling and Analysis of Real-Time and Embedded Systems; (ii) a formal semantics of C-UML diagrams, defined through formulae of the metric temporal logic Tempo Reale ImplicitO (TRIO); and (iii) a tool, called Corretto, which implements the aforementioned semantics and allows users to carry out formal verification tasks on modeled systems. We validate the feasibility of our approach through a set of different case studies, taken from both the academic and the industrial domain.

Linear Temporal Logic (LTL) has been used in computer science for decades to formally specify programs, systems, desired properties, and relevant behaviors. This paper presents a novel, efficient technique for verifying LTL specifications in a fully automated way. Our technique belongs to the category of Bounded Satisfiability Checking approaches, where LTL formulae are encoded as formulae of another decidable logic that can be solved through modern satisfiability solvers. The target logic in our approach is Bit-Vector Logic. We present our novel encoding, show its correctness, and experimentally compare it against existing encodings implemented in well-known formal verification tools.

UML (Unified Modeling Language) has been used for years in diverse domains. Its notations usually come with a reasonably well-defined syntax, but its semantics is left under-specified and open to different interpretations. This freedom hampers the formal verification of produced specifications and calls for more rigor and precision. This work aims to bridge this gap and proposes a flexible and modular formalization approach based on temporal logic. We studied the different interpretations for some of its constructs, and our framework allows one to assemble the semantics of interest by composing the selected formalizations for the different pieces. However, the formalization per-se is not enough. The verification process, in general, becomes slow and impossible -as the model grows in size. To tackle the scalability problem, this work also proposes a bit-vector-based encoding of LTL formulae. The first results witness a significant increase in the size of analyzable models, not only for our formalization of UML models, but also for numerous other models that can be reduced to bounded satisfiability checking of LTL formulae.