Automated test generation is an area that has seen a lot of research and development, resulting in many test automation methods and tools for test design. However, practitioners often face challenges in adopting these tools. This is not only due to the immaturity of some tools but also because of varying perspectives, confusing terminology, and, most importantly, the lack of a clear framework to guide the selection of the most suitable approach for their needs. We propose a taxonomy that characterizes the methods for automated test generation. The taxonomy was constructed using a process that involved analyzing secondary studies on automated test generation and existing taxonomies in the scientific literature. Direct observations and iterative refinements were included, followed by validation through conceptual evaluation and practitioner feedback. The resulting dimensions characterize automated test generation and its use in software testing. The taxonomy is organized into several dimensions: software artifact (i.e., type, notation, interfaces), test generation (i.e., objectives, methods, and monitoring), test execution, and test oracle. We demonstrate the taxonomy’s use by applying it to several automated test-generation tools. This paper provides the necessary concepts and a generic process for categorizing and assessing automated test generation approaches.
Electronic voting (e-voting) requires a trusted setup to initiate an election process. This setup must be transparent to maintain the integrity of the election. A crucial aspect of this trusted setup involves generating group generators for a finite cyclic group, which are then used in cryptographic algorithms deployed within the voting system. Although computing group generators is generally not considered a difficult problem, election verifiability – where every step can be ascertained by independent third parties – excludes many of them, as they fail to provide verifiable evidence of correctness. In this work, we present a formally verified implementation of the group generator algorithm A.2.3 and the group generator verification algorithm A.2.4, specified in the National Institute of Standards and Technology (NIST), FIPS 186-4, in the Coq theorem prover. These two algorithms are highly sought-after methods to compute and verify group generator(s), respectively, because their outcomes can be established independently by third parties. Our formalisation captures all the requirements specified in algorithms A.2.3 and A.2.4 using the expressive type system of the Coq theorem prover. We evaluate the group generator algorithm within the Coq theorem prover itself to produce group generators, thereby only trusting the Coq theorem prover and its evaluation mechanism. In fact, our implementation is so efficient that it can compute the group generators used in real-world democratic elections in 30 min on a M3 laptop.
This paper presents a vision for generating formal specifications of the problems involved in the mapping of quantum algorithms to quantum networks, called the Sub-problems of Distribution (SpD). This is a significant challenge due to the importance of distributed quantum computing and the intertwined nature of SpD. Examples of SpD include teleportation minimization, qubit routing and load balancing. As such, formal specifications can help in providing a rigorous way for specifying and solving SpD. We instantiate the proposed vision in the context of Alloy, called qcAlloy, and for two of the most important SpD problems, namely teleportation minimization and load balancing. Part of the Alloy specifications that specify the constraints of SpD are reusable for any quantum circuit and any network. qcAlloy is also compositional in that it partitions the input circuit into sub-circuits, solves the SpD for each sub-circuit, and then combines the results towards generating a nearoptimal solution. qcAlloy competes, and in some cases outperforms, the state-of-the-art for minimizing the number of teleportations for the quantum circuits in the RevLib and RLSB benchmarks.
Recent verification tools aim to make formal verification more accessible for software engineers by automating most of the verification process. However, the manual work and expertise required to write verification helper code, such as loop invariants and auxiliary lemmas and assertions, remains a barrier. This paper explores the use of Large Language Models (LLMs) to automate the generation of loop invariants for programs in Dafny. We tested the approach on a curated dataset of 100 programs in Dafny involving arrays, strings, and numeric types. Using a multimodel approach that combines GPT-4o and Claude 3.5 Sonnet, correct loop invariants (passing the Dafny verifier) were generated at the first attempt for 92
To synthesize a safe and optimal controller for switched hybrid systems, one can first synthesize a shield that ensures safety, and then apply reinforcement learning within the constraints of the shield to obtain the desired controller. However, developing such a shield for switched hybrid systems typically requires a full model of the environment, which is not always available. Instead, historical data of the environment might be available. In this paper, we introduce a method for the construction of safety shields based on different scenarios captured in historical data. We show how individual shields for different scenarios can be combined to obtain a single shield that is provably safe within the bounds of the observed scenarios. We demonstrate the method using an industrial case study of a stormwater detention pond, which includes ten years of historical data of different rain events/scenarios. Our experimental results show that the shielded optimal controller ensures safety across all individual historical rain scenarios compared to the unshielded optimal controller. Additionally, we empirically show that the shield may also generalize for scenarios not covered by the historical data.
Automated test generation is an area that has seen a lot of research and development, resulting in many test automation methods and tools for test design. However, practitioners often face challenges in adopting these tools. This is not only due to the immaturity of some tools but also because of varying perspectives, confusing terminology, and, most importantly, the lack of a clear framework to guide the selection of the most suitable approach for their needs. We propose a taxonomy that characterizes the methods for automated test generation. The taxonomy was constructed using a process that involved analyzing secondary studies on automated test generation and existing taxonomies in the scientific literature. Direct observations and iterative refinements were included, followed by validation through conceptual evaluation and practitioner feedback. The resulting dimensions characterize automated test generation and its use in software testing. The taxonomy is organized into several dimensions: software artifact (i.e., type, notation, interfaces), test generation (i.e., objectives, methods, and monitoring), test execution, and test oracle. We demonstrate the taxonomy's use by applying it to several automated test-generation tools. This paper provides the necessary concepts and a generic process for categorizing and assessing automated test generation approaches.
At the heart of Product Line Engineering (PLE) lies the feature model, which describes how features can be combined to create customized variability and commonality in the development of reconfigurable cyber-physical systems. Since standardized processes are key to high-quality product development, managing their variability should align with PLE principles and regulatory standards. However, misconfigurations frequently arise due to the complexity of these standardized processes leading to potentially hazardous conditions. Therefore, containment verification of each configuration in variability management remains a complex task, that requires extensive analysis and considerable effort. We introduce a containment verification approach to determine whether a certain product configuration is consistent with the specification defined in a feature model. Our method provides a model-based architectural analysis that identifies misconfiguration against the architecture and the potential damage scenarios of their mitigations. To facilitate this task, we model the security architecture and requirements in an Eclipse-based IDE that supports all phases of feature-oriented software development for PLE. Subsequently, the proposed approach performs automated transformation of these models, using the Acceleo transformation language, into formal constraints and descriptions, in order to leverage the analytical power of model-checking techniques. The formal verification of completeness, consistency, and conflict is carried out using the NuSMV model checker. In case a counterexample is produced, a change impact analysis is performed for the identification of problems and their resolutions. We conducted a case study to evaluate the accuracy of the verification results and the inferred model transformations.
The integral presence of social networks in users' lives, has made them the main means for information dissemination. A comprehensive analysis of users' behaviors plays a pivotal role in discerning information diffusion patterns. We extract an insightful model of users' behaviors using both automata and machine learning techniques by observing users' activities within the social network. Assuming users with similar characteristics show similar behavior on a topic, we cluster the users triggering activities related to a topic based on effective behavior factors identified within a social network using the KMeans algorithm. To handle the large number of user activities and make the active automata learning technique feasible, we abstract the user of each activity by its cluster. We extract a model for users' behavior in the form of a deterministic finite automaton by employing the L* and KV algorithms with an oracle tailored by a tree organization of sequences combined with a oneclass SVM classifier. We illustrate the applicability of our approach on two datasets obtained from Twitter on COVID-19 topics. The extracted models have around 65% to 75% accuracy.
Information flow control aims at detecting the flow of sensitive information during the program execution in order to ensure the confidentiality and integrity of secret data. Static program dependency analysis calculates data and control dependencies that can be used to detect leakage of secret information. However, secret information can also be leaked through the timing channel inherent in the structure of the code, which cannot be identified using only the data and control dependencies. In this paper, we introduce the concept of Time-Sensitive Control Closure (TSCC), which offers a very general notion of control dependency. We demonstrate the application of TSCC to the fundamental semantic notion of secure information flow called noninterference. By combining TSCC with data dependencies, we develop program slicing techniques capable of detecting security leaks through both information and timing channels. To compute TSCC efficiently, we present a log-linear time algorithm to generate the influencer graph representation of programs, and a linear time algorithm to compute TSCC from the generated influencer graph. Our algorithm is implemented within the Clang/LLVM compiler infrastructure, and we conduct experiments using well-known benchmarks. The experimental evaluation validates the accuracy and performance improvements offered by the TSCC algorithm compared to existing control dependency approaches. These results demonstrate the practical utility of TSCC in enhancing the security of real-world applications.
Smart contracts are programs executed on top of a blockchain consensus protocol. Their compiled code (bytecode) is stored on the blockchain and is immutable after deployment. They are selfenforcing in the sense that any function call to a smart contract is executed by all nodes on the network, ensuring that they all reach consensus about the final state of the contract. To prevent denial-of-service attacks, such an execution is costly by design. A "gas" cost is assigned to each bytecode operation, roughly proportional to the resources required to execute it, and any user who initiates a function call to a smart contract has to pay the total gas cost of the resulting execution. On Ethereum alone, the users pay an astounding gas cost of more than 4 billion USD/year. Smart contracts are often written in high-level programming languages such as Solidity and then compiled to bytecode before being deployed on the blockchain. Thus, a natural compiler optimization problem arising in this context is to produce efficient bytecode that minimizes the total gas usage. A leading approach in this direction is superoptimization, which considers every basic block of the smart contract separately and tries to rewrite it as an equivalent block that uses as little gas as possible. The current state-of-the-art tool is syrup 2.0, which encodes gas superoptimization as Max-SMT and then relies on SMT-solvers to synthesize an equivalent contract with optimized gas usage. In this work, we make two observations: First, the performance of Max-SMT declines significantly as block sizes increase. Thus, although syrup is able to find an optimal rewriting for a small block with a dozen bytecode operations, its output on blocks with hundreds or thousands of operations, when given any realistic timeout, is far from optimal. Second, optimizations that can be applied to basic blocks are often local and compositional, i.e. they rewrite several small and disjoint parts of the block. Such locality is lost to Max-SMT solvers, mainly because it is unpredictable and there are no clear ways on how one should cut blocks of bytecode into smaller sub-blocks. To ameliorate these issues, we present a simple dynamic programming algorithm that tries every possible division of a block into sub-blocks, recursively calling syrup as a black box on each sub-block. Surprisingly, this simple idea leads to highly significant improvements in the gas usage, more than doubling the savings obtained by syrup, and reducing the gas usage of real-world smart contracts by 11.23%.
Simulation tools are essential for designing and testing car setups in modern racecar competitions: state-of-the-art full-body simulators replicate driving conditions, but they require detailed tuning (alignment) of hundreds or thousands of parameters to reduce the reality gap. This procedure is performed by comparing simulations with realworld data (Formula 1 teams collect data in the order of terabytes every race weekend), most often visually, resulting in a time-consuming operation that requires advanced expertise. Additionally, the process is not formally encoded, relies on human intuition and expertise, and thus results are highly subjective and may vary depending on who is performing the operation. In this paper, we present an automated pipeline for parameter tuning in full-body racing simulators. This pipeline replicates the manual tuning workflow, but substituting subjective visual comparisons with an objective cost function-the Residual Sum of Squares (RSS). We validate the proposed approach by comparing the quality of the alignment and the time required to achieve it between experts performing manual tuning and the proposed automated pipeline. We find that automating the process requires a similar number of simulations to be performed compared to manual tuning, but the automated pipeline is significantly faster and more consistent.
A common approach in software verification is to encode a program as a set of Constrained Horn Clauses (CHCs), which are then processed and solved automatically by a CHC solver. To streamline this verification approach for the case of programs operating on mutable linked data-structures, we have in earlier work proposed a theory of heaps, defined within the SMT-LIB framework, which enables us to represent programs as CHCs with minimal loss of structural information. By preserving high-level program information in the encoding, the theory of heaps enables CHC solvers to apply various internal techniques for handling program heap; among others, to encode the heap further using the theory of arrays, to apply shape analysis, or to translate to a heap-less program with the help of invariants. This paper explores the third option, developing transformation rules that rewrite a set of CHCs into an equisatisfiable set of CHCs with additional predicates representing heap invariants. The proposed method generalises the notion of space invariants, which were previously introduced for verifying Java programs, by lifting the entire transformation process to the CHC level. The paper defines the transformation rules, provides detailed correctness proofs, and discusses the strengths and limitations of the approach. We also outline possible extensions of the method.
Propositional dynamic logic ( ) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of is solving fixed-point equations, i.e., formulae of the form x ≡φ (x) such that x is a propositional variable and φ (x) is a formula containing x. A solution to such an equation is a formula ψ that omits x and satisfies ψ≡φ (ψ ) , where φ (ψ ) is obtained by replacing all occurrences of x with ψ in φ (x) . In this paper, we identify a novel class of formulae arranged in two dual hierarchies for which every fixed-point equation x ≡φ (x) has a solution. Moreover, we not only prove the existence of solutions for all such equations, but also provide an explicit solution ψ for each fixed-point equation.
Interactions are formal models describing asynchronous communications within a distributed system. They can be drawn in the fashion of sequence diagrams and associated with an operational semantics in the style of process algebras. In this paper, we propose an algorithm for offline runtime verification against interactions. Our algorithm deals with observability issues e.g. that some subsystems may not be observed or that some events may not be observed when the end of monitoring on different subsystems cannot be synchronized. We prove the algorithm’s correctness and assess the performance of an implementation.
This paper presents preliminary work on theories supporting partial differentiation of scalar fields, which will be based upon, and add to, the large library of mathematical theories supported by the Prototype Verification System theorem-proving environment. These theories include mathematical analysis of functions of one real-valued variable, but not, currently, theories on partial differentiation. In this paper, the issue of defining partial derivatives in the strongly typed, higher-order language of PVS is discussed, and a straightforward, pragmatic approach is proposed, introducing the formalizations of some basic concepts.
In this paper, we specialise a more general theory for testing symbolic finite state machines (SFSM) to an important sub-class of SFSMs. This specialisation allows for a significant reduction of test cases needed for proving language equivalence between an SFSM reference model and an implementation whose true behaviour is captured by another SFSM from a given fault domain.
With the increasing application of neural networks in safety-critical domains, their robustness becomes a crucial concern. In this paper, we present a multi-neuron relaxation-based verification framework kProp for ReLU neural networks with adversarial distortions in general norms. In contrast with existing verification methods tackling general distortion norms, the proposed multi-neuron relaxation method is able to capture the relations among a group of neurons, thus providing tighter convex relaxations and improving verification precision. In addition, existing methods based on linear relaxation may include infeasible inputs to the neural network for robustness verification, which further leads to verification precision loss. To address this problem, we propose a region clipping method to exclude infeasible inputs to further improve the verification precision. We implement our verification framework and evaluate its performance on open-source benchmarks. The experiments show that kProp can produce precise verification results where existing verification methods fail to produce conclusive results, and can be applied to neural networks with more than 4k neurons in general distortion norms.
Afra is an Eclipse -based tool for the modeling and model checking of Rebeca family models. Together with the standard enriched editor, easy to trace counter-example viewer, modular temporal property definition, exporting a model and its transition system to some other formats facilities are features of Afra. Rebeca family provides actor-based modeling languages which are designed to bridge the gap between formal methods and software engineering. Faithfulness to the system being modeled, and the usability of Rebeca family languages help in ease of modeling and analysis of the model, together with the synthesis of the system based on the model. In this paper, architectural decisions and design strategies we made in the development of Afra are presented. This makes Afra an extensible and reusable application for the modeling and analysis of Rebeca family models. Here, we show how different compilers can be developed for the family of languages which are the same in general language constructs but have some minor differences. Then we show how the model checking engine for these different languages is designed. Despite the fact that Afra has a layered object-oriented design and is developed in Java technology, we use C++ codes for developing its model checking for the performance purposes. This decision made the design of the application even harder.
This paper sets the basis for a compositional and structured approach to the specification of paraconsistent transitions systems, framed as an institution. The latter and theirs logics were previously introduced in [ CMB22 ] to deal with scenarios of inconsistency in which several requirements are on stake, either reinforcing or contradicting each other.
Formal verification techniques aim at formally proving the correctness of a computer program with respect to a formal specification, but the expertise and effort required for applying formal specification and verification techniques and scalability issues have limited their practical application. In recent years, the tremendous progress with SAT and SMT solvers enabled the construction of a new generation of tools that promise to make formal verification more accessible for software engineers, by automating most if not all of the verification process. The Dafny system is a prominent example of that trend. However, little evidence exists yet about its accessibility. To help fill this gap, we conducted a set of 10 case studies of developing verified implementations in Dafny of some real-world algorithms and data structures, to determine its accessibility for software engineers. We found that, on average, the amount of code written for specification and verification purposes is of the same order of magnitude as the traditional code written for implementation and testing purposes (ratio of 1.14) – an “overhead” that certainly pays off for high-integrity software. The performance of the Dafny verifier was impressive, with 2.4 proof obligations generated per line of code written, and 24 ms spent per proof obligation generated and verified, on average. However, we also found that the manual work needed in writing auxiliary verification code may be significant and difficult to predict and master. Hence, further automation and systematization of verification tasks are possible directions for future advances in the field.
