Large Language Models (LLMs) are increasingly applied to data-centric tasks in software maintenance and evolution, such as quality assurance and migration. While recent methods constrain LLM outputs using grammars or regular expressions, these syntactic techniques fail to enforce deeper semantic constraints involving numeric dependencies, conditional logic, and checksums. We present ClauseBandit, a framework that combines LLMs with Satisfiability Modulo Theories (SMT) solvers to generate structured data satisfying such constraints from natural language specifications. ClauseBandit introduces a Bayesian inference approach that selects the most plausible SMT formula using posterior probabilities derived from formula self-consistency and data likelihoods. Evaluated on 27 structured generation tasks inspired by industrial use-cases, ClauseBandit successfully selected valid SMT formulas for$\mathbf{7 4. 1 \%}$of tasks. Our approach enables LLM-based structured generation that goes beyond syntax, producing semantically valid, reusable constraint specifications from natural language.

Abstract PROTON 2.1 presents (1) a new termination checking technique that uses a fine-tuned local LLM to synthesize ranking functions, and (2) support for multiple SAT solvers for non-termination checking.

Deep Neural Networks (DNNs) are being trained and trusted for performing fairly complex tasks, even in business- and safety-critical applications. This necessitates that they be formally analyzed before deployment. Scalability of such analyses is a major bottleneck in their widespread use. There has been a lot of work on abstraction, and counterexample-guided abstraction refinement (CEGAR) of DNNs to address the scalability issue. However, these abstraction-refinement techniques explore only a subset of possible abstractions, and may miss an optimal abstraction. In particular, the refinement updates the abstract DNN based only on local information derived from the spurious counterexample in each iteration. The lack of a global view may result in a series of bad refinement choices, limiting the search to a region of sub-optimal abstractions. We propose a novel technique that parameterizes the construction of the abstract network in terms of continuous real-valued parameters. This allows us to use gradient descent to search through the space of possible abstractions, and ensures that the search never gets restricted to sub-optimal abstractions. Moreover, our parameterization can express more general abstractions than the existing techniques, enabling us to discover better abstractions than previously possible.

Abstract PROTON is a tool to check whether a given C program has a non-terminating behaviour or not. It is built around the C Bounded Model Checker (CBMC). CBMC cannot prove non-termination directly, as all non-terminating runs are unbounded. PROTON annotates the loops in a given program with assertions that check for a recurrent program state. Violation of such an assertion shows the existence of a recurrent state and thereby proves non-termination. PROTON also transforms the violating trace returned by CBMC into a non-termination witness for the program.

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 In VeriFuzz 1.4, we implemented two new techniques for checking Non-termination and Termination. VeriFuzz 1.4 won the Termination category of SV-COMP 2023.

Abstract We present VeriFuzz 1.2 with two new enhancements: (1) unroll the given program to a short depth and use BMC to produceincompletetest inputs, which are extended intocompleteinputs, and (2) if BMC fails for this short unrolling, automatically identify the reason and rerun BMC with a corresponding remedial strategy.

Unintended non-termination of programs could lead to attacks such as Denial-of-Service(DoS). Current testing techniques are not geared to detect such errors. Towards this, we present FuzzNT, a hybrid testing technique to check non-termination of C programs by combining Coverage Guided Fuzzing (CGF) and abstract interpretation based static analysis. Given a program P and the coverage test inputs generated using CGF, P is transformed into a set of specialized programs, each of which under-approximates P. Abstract interpretation is then used to check each of these smaller programs for non-termination. The key advantage of this approach for checking non-termination is that it reuses the test case corpus created during software development and maintenance. Our preliminary experimental evaluation of FuzzNT shows highly promising results.