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.
