In out sourced industrial projects for testing of web applications, often neither the application to be tested, nor its source code are provided to the testing team, due to confidentiality reasons, making systematic testing of these applications very challenging. However, textual descriptions of such systems are often available. So, one can consider leveraging a Large Language Model (LLM) to parse these descriptions and synthesize test generators (programs that produce test data). In our experience, LLM synthesized test generators suffer from two problems:- (1) unsound: the generators might produce invalid data and (2) incomplete: the generators typically fail to generate all expected valid inputs. To mitigate these problems, we introduce TestRefineGen a method for autonomously generating test data from textual descriptions. TestRe-fineGen begins by invoking an LLM to parse a given corpus of documents and produce multiple test gener-ators. It then uses a novel ranking approach to identify generators that can produce invalid test data, and then automatically repairs them using a counterexample-guided refinement process. Lastly, TestRefineGen per-forms a generalization procedure that offsets synthesis or refinements that leads to incompleteness, to obtain generators that produce more comprehensive valid in-puts. We evaluated the effectiveness of TestRefineGen on a manually curated set of 256 textual descriptions of test data. TestRefineGen synthesized generators that produce valid test data for 66.01 % of the descriptions. Using a combination of post-processing sanitisation and refinement it was able to successfully repair synthesized generators, which improved the success rate to 76.95 %. Further, our statistical analysis on a small subset of synthesized generators shows that TestRefineGen is able to generate test data that is well distributed across the input space. Thus, TestRefineGen can be an effective technique for autonomous test data generation for web testing in projects with confidentiality concerns.

Abstract VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in three strategies. We add an array verification technique called full-program induction, and enhance the existing techniques of loop pruning, k-path interval analysis, and disjunctive loop summarization. These changes have improved the verification of programs with arrays, and unstructured loops and unstructured control flows.

Verification of programs continues to be a challenge and no single known technique succeeds on all programs. In this paper we present VeriAbs, a reachability verifier for C programs that incorporates a portfolio of techniques implemented as four strategies, where each strategy is a set of techniques applied in a specific sequence. It selects a strategy based on the kind of loops in the program. We analysed the effectiveness of the implemented strategies on the 3831 verification tasks from the ReachSafety category of the 8th International Competition on Software Verification (SV-COMP) 2019 and found that although classic techniques - explicit state model checking and bounded model checking, succeed on a majority of the programs, a wide range of further techniques are required to analyse the rest. A screencast of the tool is available at https://youtu.be/Hzh3PPiODwk.

Loop Abstraction followed by Bounded Model Checking, or LABMC in short, is a promising recent technique for proving safety of large programs. In an experimental setup proposed last year [14], LABMC was combined with slicing and Iterative Context Extension (ICE) with the aim of achieving scalability over industrial code. In this paper, we address two major limitations of that set-up, namely (i) the inability of ICE to prune redundant code in a verification context, and (ii) the unavailability of a tool that implements the set-up. We propose an improvement over ICE called Iterative Function Level Slicing (IFLS) and incorporate it in our tool called ELABMC, to offer an efficient implementation of [14]. We substantiate our claim with two sets of experiments over industrial applications as well as academic benchmarks. Quantifying the benefits of IFLS over traditional ICE in one, our results report that IFLS leads to 34.9% increase in efficiency, 17.7% improvement in precision, and scales in 14.2% more cases. With the second experiment, we show that ELABMC outperforms state-of-the-art verification techniques in the task of identifying static analysis warnings as false alarms.